awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
R : Type uR
inst : Field R
inst_1 : DecidableEq m
w : m → R
w' : { i : m // w i ≠ 0 } → m → R := fun (i : { i : m // w i ≠ 0 }) ↦ diagonal w (↑i : m)
h : LinearIndependent R w'
hrw : insert 0 (range (diagonal w)ᵀ) = insert 0 (range w')
rw : Module.rank R ↥(span R (range (diagonal w)ᵀ)) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₁ : Module.rank R ↥(span R (insert 0 (range (diagonal w)ᵀ))) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₂ : Module.rank R ↥(span R (insert 0 (range w'))) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₃ : Module.rank R ↥(span R (range w')) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₄ : #(↑(range w') : Type (max uR um)) = lift.{uR, um} #{ i : m // w i ≠ 0 }
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have rw₅ : #(↑(range w') : Type (max uR um)) = lift.{max um uR, um} #{ i : m // w i ≠ 0 }
Tactic: rw [cRank, ← span_insert_zero, hrw, span_insert_zero, rank_span h,
    ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
R : Type uR
inst : Field R
inst_1 : DecidableEq m
w : m → R
w' : { i : m // w i ≠ 0 } → m → R := fun (i : { i : m // w i ≠ 0 }) ↦ diagonal w (↑i : m)
h : LinearIndependent R w'
hrw : insert 0 (range (diagonal w)ᵀ) = insert 0 (range w')
rw : Module.rank R ↥(span R (range (diagonal w)ᵀ)) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₁ : Module.rank R ↥(span R (insert 0 (range (diagonal w)ᵀ))) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₂ : Module.rank R ↥(span R (insert 0 (range w'))) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₃ : Module.rank R ↥(span R (range w')) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₄ : #(↑(range w') : Type (max uR um)) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₅ : #(↑(range w') : Type (max uR um)) = lift.{max um uR, um} #{ i : m // w i ≠ 0 }
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have rw₆ : #(↑(range w') : Type (max uR um)) = lift.{um, max uR um} #(↑(range w') : Type (max uR um))
Tactic: rw [cRank, ← span_insert_zero, hrw, span_insert_zero, rank_span h,
    ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
R : Type uR
inst : Field R
inst_1 : DecidableEq m
w : m → R
w' : { i : m // w i ≠ 0 } → m → R := fun (i : { i : m // w i ≠ 0 }) ↦ diagonal w (↑i : m)
h : LinearIndependent R w'
hrw : insert 0 (range (diagonal w)ᵀ) = insert 0 (range w')
rw : Module.rank R ↥(span R (range (diagonal w)ᵀ)) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₁ : Module.rank R ↥(span R (insert 0 (range (diagonal w)ᵀ))) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₂ : Module.rank R ↥(span R (insert 0 (range w'))) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₃ : Module.rank R ↥(span R (range w')) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₄ : #(↑(range w') : Type (max uR um)) = lift.{uR, um} #{ i : m // w i ≠ 0 }
rw₅ : #(↑(range w') : Type (max uR um)) = lift.{max um uR, um} #{ i : m // w i ≠ 0 }
rw₆ : #(↑(range w') : Type (max uR um)) = lift.{um, max uR um} #(↑(range w') : Type (max uR um))
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have rw₇ : #(↑(range w') : Type (max uR um)) = #(↑(range w') : Type (max uR um))
Tactic: rw [cRank, ← span_insert_zero, hrw, span_insert_zero, rank_span h,
    ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
R : Type uR
inst : Field R
inst_1 : DecidableEq m
w : m → R
set set₁ : (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have set₂ : let w' : { i : m // w i ≠ 0 } → m → R := fun (i : { i : m // w i ≠ 0 }) ↦ diagonal w (↑i : m);
∀ (h : LinearIndependent R w'), (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
Tactic: classical
  set w' : {i // (w i) ≠ 0} → _ := fun i ↦ (diagonal w) i
  have h : LinearIndependent R w' := by
    have hli' := Pi.linearIndependent_single_of_ne_zero (R := R)
      (v := fun i : m ↦ if w i = 0 then (1 : R) else w i) (by simp [ite_eq_iff'])
    convert! hli'.comp Subtype.val Subtype.val_injective
    ext ⟨j, hj⟩ k
    simp [w', diagonal, hj, Pi.single_apply, eq_comm]
  have hrw : insert 0 (range (diagonal w)ᵀ) = insert 0 (range w') := by
    suffices ∀ a, diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a
      by simpa [subset_antisymm_iff, subset_def, w']
    simp_rw [or_iff_not_imp_right, not_exists, not_and, not_imp_not]
    simp +contextual [funext_iff, diagonal]
  rw [cRank, ← span_insert_zero, hrw, span_insert_zero, rank_span h,
    ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
R : Type uR
inst : Field R
inst_1 : DecidableEq m
w : m → R
set set₁ : (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
set₂ :
  let w' : { i : m // w i ≠ 0 } → m → R := fun (i : { i : m // w i ≠ 0 }) ↦ diagonal w (↑i : m);
  ∀ (h : LinearIndependent R w'), (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have set₃ : let w' : { i : m // w i ≠ 0 } → m → R := fun (i : { i : m // w i ≠ 0 }) ↦ diagonal w (↑i : m);
∀ (h : LinearIndependent R w') (hrw : insert 0 (range (diagonal w)ᵀ) = insert 0 (range w')),
  (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
Tactic: classical
  set w' : {i // (w i) ≠ 0} → _ := fun i ↦ (diagonal w) i
  have h : LinearIndependent R w' := by
    have hli' := Pi.linearIndependent_single_of_ne_zero (R := R)
      (v := fun i : m ↦ if w i = 0 then (1 : R) else w i) (by simp [ite_eq_iff'])
    convert! hli'.comp Subtype.val Subtype.val_injective
    ext ⟨j, hj⟩ k
    simp [w', diagonal, hj, Pi.single_apply, eq_comm]
  have hrw : insert 0 (range (diagonal w)ᵀ) = insert 0 (range w') := by
    suffices ∀ a, diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a
      by simpa [subset_antisymm_iff, subset_def, w']
    simp_rw [or_iff_not_imp_right, not_exists, not_and, not_imp_not]
    simp +contextual [funext_iff, diagonal]
  rw [cRank, ← span_insert_zero, hrw, span_insert_zero, rank_span h,
    ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ Eq (α := Submodule R (n → R)) (LinearMap.ker (Aᴴ * A).mulVecLin) (LinearMap.ker A.mulVecLin)
have h : ∀ (x : n → R),
  Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker (Aᴴ * A).mulVecLin) x ↔
    Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker A.mulVecLin) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
have refine : Eq (α := ℕ)
  ((fun (x : ℕ) ↦ x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin)))
  ((fun (x : ℕ) ↦ x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range A.mulVecLin)))
Tactic: refine add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
have trans : finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
  finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᴴ * A).mulVecLin)
Tactic: trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ * A)) }
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
trans :
  finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᴴ * A).mulVecLin)
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
have trans₁ : finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᴴ * A).mulVecLin) =
  finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
Tactic: trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ * A)) }
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᴴ * A).mulVecLin)
have rw : finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
  finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
Tactic: rw [ker_mulVecLin_conjTranspose_mul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
⊢ Eq (α := Submodule R (n → R)) (LinearMap.ker (Aᵀ * A).mulVecLin) (LinearMap.ker A.mulVecLin)
have h : ∀ (x : n → R),
  Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker (Aᵀ * A).mulVecLin) x ↔
    Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker A.mulVecLin) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
⊢ Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker (Aᵀ * A).mulVecLin) x ↔
    Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker A.mulVecLin) x
have h : Aᵀ *ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
Tactic: simp only [LinearMap.mem_ker, mulVecLin_apply, ← mulVec_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
⊢ Aᵀ *ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
have h : Aᵀ *ᵥ A *ᵥ x = 0 → A *ᵥ x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : Aᵀ *ᵥ A *ᵥ x = 0 → A *ᵥ x = 0
⊢ Aᵀ *ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
have h₁ : A *ᵥ x = 0 → Aᵀ *ᵥ A *ᵥ x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : Aᵀ *ᵥ A *ᵥ x = 0
⊢ A *ᵥ x = 0
have h₁ : x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0
Tactic: replace h := congr_arg (dotProduct x) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0
⊢ A *ᵥ x = 0
have h₁ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = x ⬝ᵥ 0), A *ᵥ x = 0
Tactic: rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0
h₁ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = x ⬝ᵥ 0), A *ᵥ x = 0
⊢ A *ᵥ x = 0
have h₂ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
Tactic: rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0
h₁ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = x ⬝ᵥ 0), A *ᵥ x = 0
h₂ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
⊢ A *ᵥ x = 0
have h₃ : ∀ (h : A *ᵥ x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
Tactic: rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0
h₁ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = x ⬝ᵥ 0), A *ᵥ x = 0
h₂ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
h₃ : ∀ (h : A *ᵥ x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
⊢ A *ᵥ x = 0
have h₄ : ∀ (h : A *ᵥ x = 0), A *ᵥ x = 0
Tactic: rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : A *ᵥ x = 0
⊢ Aᵀ *ᵥ A *ᵥ x = 0
have h₁ : Aᵀ *ᵥ 0 = 0
Tactic: rw [h, mulVec_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : A *ᵥ x = 0
h₁ : Aᵀ *ᵥ 0 = 0
⊢ Aᵀ *ᵥ A *ᵥ x = 0
have h₂ : Eq (α := n → R) 0 0
Tactic: rw [h, mulVec_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
have refine : Eq (α := ℕ)
  ((fun (x : ℕ) ↦ x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin)))
  ((fun (x : ℕ) ↦ x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range A.mulVecLin)))
Tactic: refine add_left_injective (finrank R <| LinearMap.ker A.mulVecLin) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
have trans : finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
  finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin)
Tactic: trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) }
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
trans :
  finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin)
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
have trans₁ : finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin) =
  finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
Tactic: trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) }
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin)
have rw : finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
  finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
Tactic: rw [ker_mulVecLin_transpose_mul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Fintype m
A : Matrix m n R
⊢ Aᵀ.rank = A.rank
have rw : finrank R
    ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
        ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
            (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
          Aᵀ)) =
  A.rank
Tactic: rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₁ : finrank R
    ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
        ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
  A.rank
Tactic: rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₂ : finrank R
    ↥(LinearMap.range (M := Dual R (m → R))
        (LinearMap.dualMap
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
  A.rank
Tactic: rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₂ :
  finrank R
      ↥(LinearMap.range (M := Dual R (m → R))
          (LinearMap.dualMap
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₃ : finrank R
    ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
        ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
  A.rank
Tactic: rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₂ :
  finrank R
      ↥(LinearMap.range (M := Dual R (m → R))
          (LinearMap.dualMap
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₃ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₄ : finrank R
    ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
        ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
  A.rank
Tactic: rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]