-- 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 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✝ }

Tactic:
apply congrArg

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

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₂
⊢ ∀ (i : Nat) (hi₁ : i < toList✝¹.length) (hi₂ : i < toList✝.length), toList✝¹.get ⟨i, hi₁⟩ = toList✝.get ⟨i, hi₂⟩

Tactic:
assumption

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 < as.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
⊢ i < as.length

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

Tactic:
have hi₂' : i+1 < (b::bs).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
hi₂' : i + 1 < (b :: 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
⊢ i + 1 < (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
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

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
⊢ as.length = bs.length

Tactic:
rw [List.length_cons, List.length_cons] at h₁

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

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

Tactic:
apply Nat.zero_lt_succ

Result:
no goals