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

Tactic:
have headEq : a = b := h₂ 0 hz₁ hz₂

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

Tactic:
apply Nat.succ_lt_succ

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

Proof state:
case mk.mk.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✝¹ = toList✝

Tactic:
apply extAux

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

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

Tactic:
injection h₁

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

Tactic:
have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption

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

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

Tactic:
cases b

Result:
case mk.mk
α : 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 := toList✝¹ } = { toList := toList✝ }

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

Tactic:
cases a

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

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 = 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

Tactic:
injection h₁

Result:
no goals