-- Mathlib/Data/Matrix/Rank.lean
theorem rank_eq_finrank_range_toLin [Finite m] [DecidableEq n] {M₁ M₂ : Type*} [AddCommGroup M₁]
    [AddCommGroup M₂] [Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Basis m R M₁)
    (v₂ : Basis n R M₂) : A.rank = finrank R (LinearMap.range (toLin v₂ v₁ A))

Proof state:
case intro
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
⊢ A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))

Tactic:
let e₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl _)

Result:
case intro
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
⊢ A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))

Proof state:
case intro
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
⊢ A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))

Tactic:
have range_e₂ : LinearMap.range e₂ = ⊤ := by
  rw [LinearMap.range_eq_top]
  exact e₂.surjective

Result:
case intro
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
⊢ A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
⊢ Function.Surjective ⇑e₂

Tactic:
exact e₂.surjective

Result:
no goals

Proof state:
case intro.e_f.h.h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
aux₁ : ((toLin (Pi.basisFun R n) (Pi.basisFun R m)) A) ((Pi.basisFun R n) i) = ∑ j : m, A j i • (Pi.basisFun R m) j
aux₂ : ∀ (e : n ≃ n), ((Pi.basisFun R n).equiv v₂ e) ((Pi.basisFun R n) i) = v₂ (e i)
⊢ ((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun i => R) i) 1 =
    (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single R (fun i => R) i) 1

Tactic:
rw [toLin_eq_toLin', toLin'_apply'] at aux₁

Result:
case intro.e_f.h.h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
aux₁ : A.mulVecLin ((Pi.basisFun R n) i) = ∑ j : m, A j i • (Pi.basisFun R m) j
aux₂ : ∀ (e : n ≃ n), ((Pi.basisFun R n).equiv v₂ e) ((Pi.basisFun R n) i) = v₂ (e i)
⊢ ((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun i => R) i) 1 =
    (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single R (fun i => R) i) 1

Proof state:
case intro.e_f.h.h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
aux₁ : A.mulVecLin (Pi.single i 1) = ∑ j : m, A j i • (Pi.basisFun R m) j
aux₂ : ∀ (e : n ≃ n), ((Pi.basisFun R n).equiv v₂ e) (Pi.single i 1) = v₂ (e i)
⊢ ((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun i => R) i) 1 =
    (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single R (fun i => R) i) 1

Tactic:
simp only [e₁, e₂, LinearMap.comp_apply, LinearEquiv.coe_coe, Equiv.refl_apply,
  aux₁, aux₂, LinearMap.coe_single, toLin_self, map_sum, LinearEquiv.map_smul, Basis.equiv_apply]

Result:
no goals

Proof state:
case intro
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
⊢ A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))

Tactic:
let e₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl _)

Result:
case intro
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
⊢ A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))