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

State before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
⊢ a₁ ::> s₁ = a₂ ::> s₂ → a₁ = a₂ ∧ s₁ = s₂
Tactic:
intros h
State after:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ a₁ = a₂ ∧ s₁ = s₂

State before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
constructor
State after:
case left
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ a₁ = a₂

case right
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ s₁ = s₂

State before:
case left
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ a₁ = a₂
Tactic:
exact congrFun h 0
State after:
no goals

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

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

State before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
⊢ a₁ = a₂ ∧ s₁ = s₂ → a₁ ::> s₁ = a₂ ::> s₂
Tactic:
intros h
State after:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ = a₂ ∧ s₁ = s₂
⊢ a₁ ::> s₁ = a₂ ::> s₂

State before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ = a₂ ∧ s₁ = s₂
⊢ a₁ ::> s₁ = a₂ ::> s₂
Tactic:
simp[h]
State after:
no goals