-- Mathlib/Data/Matrix/Rank.lean
theorem ker_mulVecLin_transpose_mul_self (A : Matrix m n R) :
    LinearMap.ker (Aᵀ * A).mulVecLin = LinearMap.ker (mulVecLin A)

Proof state:
case h.mp
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ Aᵀ *ᵥ A *ᵥ x = 0 → A *ᵥ x = 0

Tactic:
intro h

Result:
case h.mp
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : Aᵀ *ᵥ A *ᵥ x = 0
⊢ A *ᵥ x = 0

Proof state:
case h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ Aᵀ *ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0

Tactic:
constructor

Result:
case h.mp
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ Aᵀ *ᵥ A *ᵥ x = 0 → A *ᵥ x = 0

case h.mpr
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ A *ᵥ x = 0 → Aᵀ *ᵥ A *ᵥ x = 0

Proof state:
case h.mp
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : Aᵀ *ᵥ A *ᵥ x = 0
⊢ A *ᵥ x = 0

Tactic:
replace h := congr_arg (dotProduct x) h

Result:
case h.mp
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0
⊢ A *ᵥ x = 0

Proof state:
case h.mpr
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ A *ᵥ x = 0 → Aᵀ *ᵥ A *ᵥ x = 0

Tactic:
intro h

Result:
case h.mpr
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : A *ᵥ x = 0
⊢ Aᵀ *ᵥ A *ᵥ x = 0

Proof state:
case h.mpr
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : A *ᵥ x = 0
⊢ Aᵀ *ᵥ A *ᵥ x = 0

Tactic:
rw [h, mulVec_zero]

Result:
no goals

Proof state:
case h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ x ∈ LinearMap.ker (Aᵀ * A).mulVecLin ↔ x ∈ LinearMap.ker A.mulVecLin

Tactic:
simp only [LinearMap.mem_ker, mulVecLin_apply, ← mulVec_mulVec]

Result:
case h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ Aᵀ *ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ LinearMap.ker (Aᵀ * A).mulVecLin = LinearMap.ker A.mulVecLin

Tactic:
ext x

Result:
case h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ x ∈ LinearMap.ker (Aᵀ * A).mulVecLin ↔ x ∈ LinearMap.ker A.mulVecLin

Proof state:
case h.mp
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0
⊢ A *ᵥ x = 0

Tactic:
rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h

Result:
no goals