truncate_eq_of_agree — Mathlib

English

If x : CofixA F n, y : CofixA F (n+1) agree, then truncate y = x.

Русский

Если x ∈ CofixA F n, y ∈ CofixA F (n+1) согласованы, то truncate y = x.

LaTeX

$$$\operatorname{truncate\_eq\_of\_agree} \ x \ y \ h : \text{Agree } x y \Rightarrow \operatorname{truncate} y = x.$$$

Lean4

theorem truncate_eq_of_agree {n : ℕ} (x : CofixA F n) (y : CofixA F (succ n)) (h : Agree x y) : truncate y = x :=
  by
  induction n <;> cases x <;> cases y
  · rfl
  · -- cases' h with _ _ _ _ _ h₀ h₁

    cases h
    simp only [truncate, Function.comp_def]
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): used to be `ext y`

    rename_i n_ih a f y h₁
    suffices (fun x => truncate (y x)) = f by simp [this]
    funext y
    apply n_ih
    apply h₁

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