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

State before:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
⊢ Function.Injective (a :> f)
Tactic:
have : ∀ i, f i ≠ a := fun i => (ha i).symm
State after:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
⊢ Function.Injective (a :> f)

State before:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
⊢ Function.Injective (a :> f)
Tactic:
intro i j
State after:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i j : Fin n.succ
⊢ (a :> f) i = (a :> f) j → i = j

State before:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i j : Fin n.succ
⊢ (a :> f) i = (a :> f) j → i = j
Tactic:
cases i using Fin.cases <;> cases j using Fin.cases <;> simp[*]
State after:
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
⊢ f i✝¹ = f i✝ → i✝¹ = i✝

State before:
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
⊢ f i✝¹ = f i✝ → i✝¹ = i✝
Tactic:
intro hf
State after:
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
hf : f i✝¹ = f i✝
⊢ i✝¹ = i✝

State before:
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
hf : f i✝¹ = f i✝
⊢ i✝¹ = i✝
Tactic:
exact h hf
State after:
no goals