ext — Mathlib

English

If two ListBlanks agree on every nth element, then they are equal.

Русский

Если две ListBlank совпадают по каждому элементу с индексом n, то они равны.

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)]\,{L_1 L_2 : ListBlank(\Gamma)},\ (\forall i, L_1.nth(i) = L_2.nth(i)) \rightarrow L_1 = L_2$$$

Lean4

@[ext]
theorem ext {Γ} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} : (∀ i, L₁.nth i = L₂.nth i) → L₁ = L₂ :=
  by
  refine ListBlank.induction_on L₁ fun l₁ ↦ ListBlank.induction_on L₂ fun l₂ H ↦ ?_
  wlog h : l₁.length ≤ l₂.length
  · cases le_total l₁.length l₂.length <;> [skip; symm] <;> apply this <;> try assumption
    intro
    rw [H]
  refine Quotient.sound' (Or.inl ⟨l₂.length - l₁.length, ?_⟩)
  refine List.ext_getElem ?_ fun i h h₂ ↦ Eq.symm ?_
  · simp only [Nat.add_sub_cancel' h, List.length_append, List.length_replicate]
  simp only [ListBlank.nth_mk] at H
  rcases lt_or_ge i l₁.length with h' | h'
  · simp [h', List.getElem_append h₂, ← List.getI_eq_getElem _ h, ← List.getI_eq_getElem _ h', H]
  · rw [List.getElem_append_right h', List.getElem_replicate, ← List.getI_eq_default _ h', H, List.getI_eq_getElem _ h]

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