Theorem: Vector.ext' (Saturn/Vector.lean)

State before:
α : Type
n : ℕ
v1 v2 : Vector α n
⊢ get' v1 = get' v2 → v1 = v2
Tactic:
intro h
State after:
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
⊢ v1 = v2

State before:
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
⊢ v1 = v2
Tactic:
apply Vector.ext
State after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
⊢ ∀ (m : Fin n), get v1 m = get v2 m

State before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
⊢ ∀ (m : Fin n), get v1 m = get v2 m
Tactic:
intro ⟨i, iw⟩
State after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
⊢ get v1 { val := i, isLt := iw } = get v2 { val := i, isLt := iw }

State before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
⊢ get v1 { val := i, isLt := iw } = get v2 { val := i, isLt := iw }
Tactic:
show get' v1 i iw = get' v2 i iw
State after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
⊢ get' v1 i iw = get' v2 i iw

State before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
⊢ get' v1 i iw = get' v2 i iw
Tactic:
let lem := congrFun h i
State after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
lem : get' v1 i = get' v2 i := congrFun h i
⊢ get' v1 i iw = get' v2 i iw

State before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
lem : get' v1 i = get' v2 i := congrFun h i
⊢ get' v1 i iw = get' v2 i iw
Tactic:
let lem' := (congrFun lem iw)
State after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
lem : get' v1 i = get' v2 i := congrFun h i
lem' : get' v1 i iw = get' v2 i iw := congrFun lem iw
⊢ get' v1 i iw = get' v2 i iw

State before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
lem : get' v1 i = get' v2 i := congrFun h i
lem' : get' v1 i iw = get' v2 i iw := congrFun lem iw
⊢ get' v1 i iw = get' v2 i iw
Tactic:
exact lem'
State after:
no goals