-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem ext (a b : Array α)
    (h₁ : a.size = b.size)
    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
    : a = b

Proof state:
α : Type u
a✝ b✝ : Array α
h₁✝ : a✝.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a✝.size) (hi₂ : i < b✝.size), getElem a✝ i hi₁ = getElem b✝ i hi₂
a : α
as : List α
ih :
  ∀ (b : List α),
    as.length = b.length →
      (∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < b.length), as.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) → as = b
b : α
bs : List α
h₁ : as.length + 1 = bs.length + 1
h₂ :
  ∀ (i : Nat) (hi₁ : i < (a :: as).length) (hi₂ : i < (b :: bs).length), (a :: as).get ⟨i, hi₁⟩ = (b :: bs).get ⟨i, hi₂⟩
hz₁ : 0 < (a :: as).length
hz₂ : 0 < (b :: bs).length
headEq : a = b
⊢ as.length = bs.length

Tactic:
injection h₁

Result:
no goals

Proof state:
case cons
α : Type u
a✝ b✝ : Array α
h₁✝ : a✝.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a✝.size) (hi₂ : i < b✝.size), getElem a✝ i hi₁ = getElem b✝ i hi₂
a : α
as : List α
ih :
  ∀ (b : List α),
    as.length = b.length →
      (∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < b.length), as.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) → as = b
b : List α
h₁ : (a :: as).length = b.length
h₂ : ∀ (i : Nat) (hi₁ : i < (a :: as).length) (hi₂ : i < b.length), (a :: as).get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩
⊢ a :: as = b

Tactic:
cases b with
| nil => rw [List.length_cons] at h₁; injection h₁
| cons b bs =>
  have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
  have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
  have headEq : a = b := h₂ 0 hz₁ hz₂
  have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
  have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
    intro i hi₁ hi₂
    have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
    have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
    have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
    apply this
  have tailEq : as = bs := ih bs h₁' h₂'
  rw [headEq, tailEq]

Result:
no goals

Proof state:
α : Type u
a✝ b✝ : Array α
h₁✝ : a✝.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a✝.size) (hi₂ : i < b✝.size), getElem a✝ i hi₁ = getElem b✝ i hi₂
a : α
as : List α
ih :
  ∀ (b : List α),
    as.length = b.length →
      (∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < b.length), as.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) → as = b
b : α
bs : List α
h₁ : (a :: as).length = (b :: bs).length
h₂ :
  ∀ (i : Nat) (hi₁ : i < (a :: as).length) (hi₂ : i < (b :: bs).length), (a :: as).get ⟨i, hi₁⟩ = (b :: bs).get ⟨i, hi₂⟩
hz₁ : 0 < (a :: as).length
hz₂ : 0 < (b :: bs).length
headEq : a = b
h₁' : as.length = bs.length
i : Nat
hi₁ : i < as.length
hi₂ : i < bs.length
hi₁' : i + 1 < (a :: as).length
hi₂' : i + 1 < (b :: bs).length
this : (a :: as).get ⟨i + 1, hi₁'⟩ = (b :: bs).get ⟨i + 1, hi₂'⟩
⊢ as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩

Tactic:
apply this

Result:
no goals

Proof state:
case cons.cons
α : Type u
a✝ b✝ : Array α
h₁✝ : a✝.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a✝.size) (hi₂ : i < b✝.size), getElem a✝ i hi₁ = getElem b✝ i hi₂
a : α
as : List α
ih :
  ∀ (b : List α),
    as.length = b.length →
      (∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < b.length), as.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) → as = b
b : α
bs : List α
h₁ : (a :: as).length = (b :: bs).length
h₂ :
  ∀ (i : Nat) (hi₁ : i < (a :: as).length) (hi₂ : i < (b :: bs).length), (a :: as).get ⟨i, hi₁⟩ = (b :: bs).get ⟨i, hi₂⟩
hz₁ : 0 < (a :: as).length
hz₂ : 0 < (b :: bs).length
headEq : a = b
h₁' : as.length = bs.length
h₂' : ∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < bs.length), as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩
⊢ a :: as = b :: bs

Tactic:
have tailEq : as = bs := ih bs h₁' h₂'

Result:
case cons.cons
α : Type u
a✝ b✝ : Array α
h₁✝ : a✝.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a✝.size) (hi₂ : i < b✝.size), getElem a✝ i hi₁ = getElem b✝ i hi₂
a : α
as : List α
ih :
  ∀ (b : List α),
    as.length = b.length →
      (∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < b.length), as.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) → as = b
b : α
bs : List α
h₁ : (a :: as).length = (b :: bs).length
h₂ :
  ∀ (i : Nat) (hi₁ : i < (a :: as).length) (hi₂ : i < (b :: bs).length), (a :: as).get ⟨i, hi₁⟩ = (b :: bs).get ⟨i, hi₂⟩
hz₁ : 0 < (a :: as).length
hz₂ : 0 < (b :: bs).length
headEq : a = b
h₁' : as.length = bs.length
h₂' : ∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < bs.length), as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩
tailEq : as = bs
⊢ a :: as = b :: bs

Proof state:
case nil.nil
α : Type u
a b : Array α
h₁✝ : a.size = b.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), getElem a i hi₁ = getElem b i hi₂
h₁ : List.nil.length = List.nil.length
h₂ : ∀ (i : Nat) (hi₁ hi₂ : i < List.nil.length), List.nil.get ⟨i, hi₁⟩ = List.nil.get ⟨i, hi₂⟩
⊢ List.nil = List.nil

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a✝ b✝ : Array α
h₁✝ : a✝.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a✝.size) (hi₂ : i < b✝.size), getElem a✝ i hi₁ = getElem b✝ i hi₂
a : α
as : List α
ih :
  ∀ (b : List α),
    as.length = b.length →
      (∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < b.length), as.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) → as = b
b : α
bs : List α
h₁ : (a :: as).length = (b :: bs).length
h₂ :
  ∀ (i : Nat) (hi₁ : i < (a :: as).length) (hi₂ : i < (b :: bs).length), (a :: as).get ⟨i, hi₁⟩ = (b :: bs).get ⟨i, hi₂⟩
hz₁ : 0 < (a :: as).length
hz₂ : 0 < (b :: bs).length
headEq : a = b
h₁' : as.length = bs.length
i : Nat
hi₁ : i < as.length
hi₂ : i < bs.length
⊢ i + 1 < (a :: as).length

Tactic:
rw [List.length_cons]

Result:
α : Type u
a✝ b✝ : Array α
h₁✝ : a✝.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a✝.size) (hi₂ : i < b✝.size), getElem a✝ i hi₁ = getElem b✝ i hi₂
a : α
as : List α
ih :
  ∀ (b : List α),
    as.length = b.length →
      (∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < b.length), as.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) → as = b
b : α
bs : List α
h₁ : (a :: as).length = (b :: bs).length
h₂ :
  ∀ (i : Nat) (hi₁ : i < (a :: as).length) (hi₂ : i < (b :: bs).length), (a :: as).get ⟨i, hi₁⟩ = (b :: bs).get ⟨i, hi₂⟩
hz₁ : 0 < (a :: as).length
hz₂ : 0 < (b :: bs).length
headEq : a = b
h₁' : as.length = bs.length
i : Nat
hi₁ : i < as.length
hi₂ : i < bs.length
⊢ i + 1 < as.length + 1

Proof state:
case nil.cons
α : Type u
a b✝ : Array α
h₁✝ : a.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b✝.size), getElem a i hi₁ = getElem b✝ i hi₂
b : α
bs : List α
h₁ : List.nil.length = (b :: bs).length
h₂ :
  ∀ (i : Nat) (hi₁ : i < List.nil.length) (hi₂ : i < (b :: bs).length), List.nil.get ⟨i, hi₁⟩ = (b :: bs).get ⟨i, hi₂⟩
⊢ List.nil = b :: bs

Tactic:
rw [List.length_cons] at h₁

Result:
case nil.cons
α : Type u
a b✝ : Array α
h₁✝ : a.size = b✝.size
h₂✝ : ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b✝.size), getElem a i hi₁ = getElem b✝ i hi₂
b : α
bs : List α
h₁ : List.nil.length = bs.length + 1
h₂ :
  ∀ (i : Nat) (hi₁ : i < List.nil.length) (hi₂ : i < (b :: bs).length), List.nil.get ⟨i, hi₁⟩ = (b :: bs).get ⟨i, hi₂⟩
⊢ List.nil = b :: bs