-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem card_le_of_injective'' {α : Type v} {β : Type v} (f : (α →₀ R) →ₗ[R] β →₀ R)
    (i : Injective f) : #α ≤ #β

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
⊢ #α ≤ #β

Tactic:
let b : Basis β R (β →₀ R) := ⟨1⟩

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ #α ≤ #β

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ Injective ⇑(linearCombination R fun i => f (single i 1))

Tactic:
have : (linearCombination R fun i ↦ f (Finsupp.single i 1)) = f := by ext a b; simp

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
this : (linearCombination R fun i => f (single i 1)) = f
⊢ Injective ⇑(linearCombination R fun i => f (single i 1))

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
this : (linearCombination R fun i => f (single i 1)) = f
⊢ Injective ⇑(linearCombination R fun i => f (single i 1))

Tactic:
exact this.symm ▸ i

Result:
no goals

Proof state:
case h.h.h
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b✝ : Basis β R (β →₀ R) := { repr := 1 }
a : α
b : β
⊢ (((linearCombination R fun i => f (single i 1)) ∘ₗ lsingle a) 1) b = ((f ∘ₗ lsingle a) 1) b

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ #α ≤ #β

Tactic:
apply linearIndependent_le_basis b (fun (i : α) ↦ f (Finsupp.single i 1))

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ LinearIndependent R fun i => f (single i 1)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ LinearIndependent R fun i => f (single i 1)

Tactic:
rw [LinearIndependent]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ Injective ⇑(linearCombination R fun i => f (single i 1))

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ (linearCombination R fun i => f (single i 1)) = f

Tactic:
ext a b

Result:
case h.h.h
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b✝ : Basis β R (β →₀ R) := { repr := 1 }
a : α
b : β
⊢ (((linearCombination R fun i => f (single i 1)) ∘ₗ lsingle a) 1) b = ((f ∘ₗ lsingle a) 1) b