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

Tactic:
rw [List.length_cons] at h₁

Result:
case cons.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₂
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
h₁ : as.length + 1 = List.nil.length
h₂ :
  ∀ (i : Nat) (hi₁ : i < (a :: as).length) (hi₂ : i < List.nil.length), (a :: as).get ⟨i, hi₁⟩ = List.nil.get ⟨i, hi₂⟩
⊢ a :: as = List.nil

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), as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩

Tactic:
intro i hi₁ hi₂

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
⊢ as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩

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
⊢ as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩

Tactic:
have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'

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
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₂⟩

Proof state:
case a
α : 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
⊢ i < bs.length

Tactic:
assumption

Result:
no goals

Proof state:
case mk.mk.h.h₁
α : Type u
toList✝¹ toList✝ : List α
h₁ : { toList := toList✝¹ }.size = { toList := toList✝ }.size
h₂ :
  ∀ (i : Nat) (hi₁ : i < { toList := toList✝¹ }.size) (hi₂ : i < { toList := toList✝ }.size),
    getElem { toList := toList✝¹ } i hi₁ = getElem { toList := toList✝ } i hi₂
⊢ toList✝¹.length = toList✝.length

case mk.mk.h.h₂
α : Type u
toList✝¹ toList✝ : List α
h₁ : { toList := toList✝¹ }.size = { toList := toList✝ }.size
h₂ :
  ∀ (i : Nat) (hi₁ : i < { toList := toList✝¹ }.size) (hi₂ : i < { toList := toList✝ }.size),
    getElem { toList := toList✝¹ } i hi₁ = getElem { toList := toList✝ } i hi₂
⊢ ∀ (i : Nat) (hi₁ : i < toList✝¹.length) (hi₂ : i < toList✝.length), toList✝¹.get ⟨i, hi₁⟩ = toList✝.get ⟨i, hi₂⟩

Tactic:
assumption

Result:
case mk.mk.h.h₂
α : Type u
toList✝¹ toList✝ : List α
h₁ : { toList := toList✝¹ }.size = { toList := toList✝ }.size
h₂ :
  ∀ (i : Nat) (hi₁ : i < { toList := toList✝¹ }.size) (hi₂ : i < { toList := toList✝ }.size),
    getElem { toList := toList✝¹ } i hi₁ = getElem { toList := toList✝ } i hi₂
⊢ ∀ (i : Nat) (hi₁ : i < toList✝¹.length) (hi₂ : i < toList✝.length), toList✝¹.get ⟨i, hi₁⟩ = toList✝.get ⟨i, hi₂⟩

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

Tactic:
have hz₂ : 0 < (b::bs).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
hz₂ : 0 < (b :: bs).length
⊢ a :: as = b :: bs