-- 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:
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
⊢ a :: as = b :: bs

Tactic:
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

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₂⟩
⊢ a :: as = b :: bs

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₂⟩
⊢ a :: as = b :: bs

Tactic:
have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ

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
⊢ a :: as = b :: bs

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₂⟩
⊢ 0 < as.length + 1

Tactic:
apply Nat.zero_lt_succ

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
⊢ a :: as = b :: bs

Tactic:
have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection 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
⊢ a :: as = b :: bs

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 b : List α
h₁ : a.length = b.length
h₂ : ∀ (i : Nat) (hi₁ : i < a.length) (hi₂ : i < b.length), a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩
⊢ a = b

Tactic:
induction a generalizing b with
| nil =>
  cases b with
  | nil       => rfl
  | cons b bs => rw [List.length_cons] at h₁; injection h₁
| cons a as ih =>
  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
⊢ 0 < (b :: bs).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
⊢ 0 < bs.length + 1