nmul_nadd — Mathlib

English

Multiplication distributes over natural addition: a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c.

Русский

Произведение распределяется по натуральному сложению: a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c.

LaTeX

$$$\\forall a,b,c \\in \\mathrm{Ordinal},\\ a \\nabla (b \\# c) = a \\nabla b \\# a \\nabla c$$$

Lean4

theorem nmul_nadd (a b c : Ordinal) : a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c :=
  by
  refine le_antisymm (nmul_le_iff.2 fun a' ha d hd => ?_) (nadd_le_iff.2 ⟨fun d hd => ?_, fun d hd => ?_⟩)
  · rw [nmul_nadd]
    rcases lt_nadd_iff.1 hd with (⟨b', hb, hd⟩ | ⟨c', hc, hd⟩)
    · have := nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha hb) (nmul_nadd_le ha.le hd)
      rw [nmul_nadd, nmul_nadd] at this
      simp only [nadd_assoc] at this
      rwa [nadd_left_comm, nadd_left_comm _ (a ⨳ b'), nadd_left_comm (a ⨳ b), nadd_lt_nadd_iff_left,
        nadd_left_comm (a' ⨳ b), nadd_left_comm (a ⨳ b), nadd_lt_nadd_iff_left, ← nadd_assoc, ← nadd_assoc] at this
    · have := nadd_lt_nadd_of_le_of_lt (nmul_nadd_le ha.le hd) (nmul_nadd_lt ha hc)
      rw [nmul_nadd, nmul_nadd] at this
      simp only [nadd_assoc] at this
      rwa [nadd_left_comm, nadd_comm (a ⨳ c), nadd_left_comm (a' ⨳ d), nadd_left_comm (a ⨳ c'), nadd_left_comm (a ⨳ b),
        nadd_lt_nadd_iff_left, nadd_comm (a' ⨳ c), nadd_left_comm (a ⨳ d), nadd_left_comm (a' ⨳ b),
        nadd_left_comm (a ⨳ b), nadd_lt_nadd_iff_left, nadd_comm (a ⨳ d), nadd_comm (a' ⨳ d), ← nadd_assoc, ←
        nadd_assoc] at this
  · rcases lt_nmul_iff.1 hd with ⟨a', ha, b', hb, hd⟩
    have := nadd_lt_nadd_of_le_of_lt hd (nmul_nadd_lt ha (nadd_lt_nadd_right hb c))
    rw [nmul_nadd, nmul_nadd, nmul_nadd a'] at this
    simp only [nadd_assoc] at this
    rwa [nadd_left_comm (a' ⨳ b'), nadd_left_comm, nadd_lt_nadd_iff_left, nadd_left_comm, nadd_left_comm _ (a' ⨳ b'),
      nadd_left_comm (a ⨳ b'), nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ c), nadd_left_comm, nadd_lt_nadd_iff_left,
      nadd_left_comm, nadd_comm _ (a' ⨳ c), nadd_lt_nadd_iff_left] at this
  · rcases lt_nmul_iff.1 hd with ⟨a', ha, c', hc, hd⟩
    have := nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha (nadd_lt_nadd_left hc b)) hd
    rw [nmul_nadd, nmul_nadd, nmul_nadd a'] at this
    simp only [nadd_assoc] at this
    rwa [nadd_left_comm _ (a' ⨳ b), nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ c'), nadd_left_comm _ (a' ⨳ c),
      nadd_lt_nadd_iff_left, nadd_left_comm, nadd_comm (a' ⨳ c'), nadd_left_comm _ (a ⨳ c'), nadd_lt_nadd_iff_left,
      nadd_comm _ (a' ⨳ c'), nadd_comm _ (a' ⨳ c'), nadd_left_comm, nadd_lt_nadd_iff_left] at this
termination_by (a, b, c)

Похожие утверждения