English
Let a,b,c,d be ordinals. There exist a' < a, b' < b, c' < c such that d ⊞ a' ⊗ b' ⊗ c ⊞ a' ⊗ b ⊗ c' ⊞ a ⊗ b' ⊗ c' ≤ a' ⊗ b ⊗ c ⊞ a ⊗ b' ⊗ c ⊞ a ⊗ b ⊗ c' ⊞ a' ⊗ b' ⊗ c'.
Русский
Пусть a,b,c,d — ординалы. Существуют a' < a, b' < b, c' < c такие, что d ⊞ a' ⊗ b' ⊗ c ⊞ a' ⊗ b ⊗ c' ⊞ a ⊗ b' ⊗ c' ≤ a' ⊗ b ⊗ c ⊞ a ⊗ b' ⊗ c ⊞ a ⊗ b ⊗ c' ⊞ a' ⊗ b' ⊗ c'.
LaTeX
$$$d < a \otimes b \otimes c \iff \exists a' < a, \exists b' < b, \exists c' < c, \\ d \boxplus a' \otimes b' \otimes c \boxplus a' \otimes b \otimes c' \boxplus a \otimes b' \otimes c' \le a' \otimes b \otimes c \boxplus a \otimes b' \otimes c \boxplus a \otimes b \otimes c' \boxplus a' \otimes b' \otimes c' $$$
Lean4
theorem lt_nmul_iff₃ :
d < a ⨳ b ⨳ c ↔
∃ a' < a,
∃ b' < b,
∃ c' < c, d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' :=
by
refine ⟨fun h ↦ ?_, fun ⟨a', ha, b', hb, c', hc, h⟩ ↦ ?_⟩
· rcases lt_nmul_iff.1 h with ⟨e, he, c', hc, H₁⟩
rcases lt_nmul_iff.1 he with ⟨a', ha, b', hb, H₂⟩
refine ⟨a', ha, b', hb, c', hc, ?_⟩
have := nadd_le_nadd H₁ (nmul_nadd_le H₂ hc.le)
simp only [nadd_nmul, nadd_assoc] at this
rw [nadd_left_comm, nadd_left_comm d, nadd_left_comm, nadd_le_nadd_iff_left, nadd_left_comm (a ⨳ b' ⨳ c),
nadd_left_comm (a' ⨳ b ⨳ c), nadd_left_comm (a ⨳ b ⨳ c'), nadd_le_nadd_iff_left, nadd_left_comm (a ⨳ b ⨳ c'),
nadd_left_comm (a ⨳ b ⨳ c')] at this
simpa only [nadd_assoc]
· have := h.trans_lt (nmul_nadd_lt₃ ha hb hc)
repeat rw [nadd_lt_nadd_iff_right] at this
assumption
