Theorem: Matrix.vecCons_ext (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
⊢ a₁ :> s₁ = a₂ :> s₂ → a₁ = a₂ ∧ s₁ = s₂
Tactic:
intros h
State after:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ a₁ = a₂ ∧ s₁ = s₂

State before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
constructor
State after:
case left
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ a₁ = a₂

case right
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ s₁ = s₂

State before:
case left
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ a₁ = a₂
Tactic:
exact congrFun h 0
State after:
no goals

State before:
case right
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ s₁ = s₂
Tactic:
exact funext (fun i => by simpa using congrFun h (Fin.castSucc i + 1))
State after:
no goals

State before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
i : Fin n
⊢ s₁ i = s₂ i
Tactic:
simpa using congrFun h (Fin.castSucc i + 1)
State after:
no goals

State before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
⊢ a₁ = a₂ ∧ s₁ = s₂ → a₁ :> s₁ = a₂ :> s₂
Tactic:
intros h
State after:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ = a₂ ∧ s₁ = s₂
⊢ a₁ :> s₁ = a₂ :> s₂

State before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ = a₂ ∧ s₁ = s₂
⊢ a₁ :> s₁ = a₂ :> s₂
Tactic:
simp[h]
State after:
no goals