repr_add — Mathlib

English

For any o1,o2 with NF, repr(o1 + o2) = repr(o1) + repr(o2).

Русский

Для любых o1, o2 с NF выполняется repr(o1 + o2) = repr(o1) + repr(o2).

LaTeX

$$$\forall o_1,o_2\; [o_1.NF][o_2.NF],\; repr(o_1 + o_2) = repr(o_1) + repr(o_2)$$$

Lean4

@[simp]
theorem repr_add : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ + o₂) = repr o₁ + repr o₂
  | 0, o, _, _ => by simp
  | oadd e n a, o, h₁, h₂ => by
    haveI := h₁.snd; have h' := repr_add a o
    conv_lhs at h' => simp [HAdd.hAdd, Add.add]
    have nf := ONote.add_nf a o
    conv at nf => simp [HAdd.hAdd, Add.add]
    conv in _ + o => simp [HAdd.hAdd, Add.add]
    rcases h : add a o with - | ⟨e', n', a'⟩ <;> simp only [add, addAux, h'.symm, h, add_assoc, repr] at nf h₁ ⊢
    have := h₁.fst; haveI := nf.fst; have ee := cmp_compares e e'
    cases he : cmp e e' <;>
      simp only [he, Ordering.compares_gt, Ordering.compares_lt, Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe,
        Nat.cast_add] at ee ⊢
    · rw [← add_assoc, @add_absorp _ (repr e') (ω ^ repr e' * (n' : ℕ))]
      · have := (h₁.below_of_lt ee).repr_lt
        unfold repr at this
        cases he' : e' <;> simp only [he', zero_def, opow_zero, repr, gt_iff_lt] at this ⊢ <;>
          exact lt_of_le_of_lt (le_add_right _ _) this
      · simpa using (mul_le_mul_iff_right₀ <| opow_pos (repr e') omega0_pos).2 (Nat.cast_le.2 n'.pos)
    · rw [ee, ← add_assoc, ← mul_add]

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