-- 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.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
⊢ ((↑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:
have aux₁ := toLin_self (Pi.basisFun R n) (Pi.basisFun R m) A i

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₁ : ((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
⊢ ((↑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₁ : ((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
⊢ ((↑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:
have aux₂ := Basis.equiv_apply (Pi.basisFun R n) i v₂

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₁ : ((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

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)
range_e₂ : LinearMap.range e₂ = ⊤
⊢ Submodule.map (↑e₁) (LinearMap.range A.mulVecLin) = LinearMap.range ((toLin v₂ v₁) A)

Tactic:
rw [← LinearMap.range_comp, ← LinearMap.range_comp_of_range_eq_top (toLin v₂ v₁ A) range_e₂]

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₂ = ⊤
⊢ LinearMap.range (↑e₁ ∘ₗ A.mulVecLin) = LinearMap.range ((toLin v₂ v₁) A ∘ₗ ↑e₂)

Proof state:
case intro.e_f.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
⊢ (↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun i => R) i =
    ((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single R (fun i => R) i

Tactic:
apply LinearMap.ext_ring

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
⊢ ((↑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:
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₂
⊢ A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))

Tactic:
cases nonempty_fintype m

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
⊢ A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))