awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : 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₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
i : n
⊢ Eq (α := m → R)
    ((((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A : (n → R) →ₗ[R] m → R) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) i : n → R) :
      m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)

Tactic:
have aux₁ := toLin_self (Pi.basisFun R n) (Pi.basisFun R m) A i
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : 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₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
i : n
aux₁ :
  Eq (α := m → R)
    ((((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A : (n → R) →ₗ[R] m → R) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) i : n → R) :
      m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
⊢ ∀ (e : n ≃ n),
    Eq.{u_2 + 1} (α := M₂)
      ((Basis.equiv (Pi.basisFun R n) v₂ e : (a : n → R) → M₂) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : M₂)
      ((v₂ : (a : n) → M₂) ((e : (a : n) → n) i : n) : M₂)

Tactic:
have aux₂ := Basis.equiv_apply (Pi.basisFun R n) i v₂
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : 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₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
i : n
aux₁ :
  Eq (α := m → R)
    ((((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A : (n → R) →ₗ[R] m → R) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) i : n → R) :
      m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
aux₂ :
  ∀ (e : n ≃ n),
    Eq.{u_2 + 1} (α := M₂)
      ((Basis.equiv (Pi.basisFun R n) v₂ e : (a : n → R) → M₂) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : M₂)
      ((v₂ : (a : n) → M₂) ((e : (a : n) → n) i : n) : M₂)
⊢ Eq (α := m → R) ((A.mulVecLin : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)

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

Premises used: Matrix.toLin'_apply', Matrix.toLin_eq_toLin'
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : 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₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
i : n
aux₁ :
  Eq (α := m → R)
    ((((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A : (n → R) →ₗ[R] m → R) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) i : n → R) :
      m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
aux₂ :
  ∀ (e : n ≃ n),
    Eq.{u_2 + 1} (α := M₂)
      ((Basis.equiv (Pi.basisFun R n) v₂ e : (a : n → R) → M₂) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : M₂)
      ((v₂ : (a : n) → M₂) ((e : (a : n) → n) i : n) : M₂)
aux₃ :
  Eq (α := m → R) ((A.mulVecLin : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
⊢ ∀ (e : n ≃ n),
    Eq.{u_2 + 1} (α := M₂)
      ((Basis.equiv (Pi.basisFun R n) v₂ e : (a : n → R) → M₂) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : M₂)
      ((v₂ : (a : n) → M₂) ((e : (a : n) → n) i : n) : M₂)

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

Premises used: Matrix.toLin'_apply', Matrix.toLin_eq_toLin'
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : 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₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
i : n
aux₁ :
  Eq (α := m → R) ((A.mulVecLin : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
aux₂ :
  ∀ (e : n ≃ n),
    Eq.{u_2 + 1} (α := M₂)
      ((Basis.equiv (Pi.basisFun R n) v₂ e : (a : n → R) → M₂) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : M₂)
      ((v₂ : (a : n) → M₂) ((e : (a : n) → n) i : n) : M₂)
⊢ Eq (α := m → R) ((A.mulVecLin : (a : n → R) → m → R) (Pi.single (M := fun (j : n) ↦ R) i 1) : m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)

Tactic:
rw [Pi.basisFun_apply] at aux₁ aux₂

Premises used: Pi.basisFun_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : 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₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
i : n
aux₁ :
  Eq (α := m → R) ((A.mulVecLin : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
aux₂ :
  ∀ (e : n ≃ n),
    Eq.{u_2 + 1} (α := M₂)
      ((Basis.equiv (Pi.basisFun R n) v₂ e : (a : n → R) → M₂) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : M₂)
      ((v₂ : (a : n) → M₂) ((e : (a : n) → n) i : n) : M₂)
aux₃ :
  Eq (α := m → R) ((A.mulVecLin : (a : n → R) → m → R) (Pi.single (M := fun (j : n) ↦ R) i 1) : m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
⊢ ∀ (e : n ≃ n),
    Eq.{u_2 + 1} (α := M₂)
      ((Basis.equiv (Pi.basisFun R n) v₂ e : (a : n → R) → M₂) (Pi.single (M := fun (j : n) ↦ R) i 1) : M₂)
      ((v₂ : (a : n) → M₂) ((e : (a : n) → n) i : n) : M₂)

Tactic:
rw [Pi.basisFun_apply] at aux₁ aux₂

Premises used: Pi.basisFun_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : 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₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
i : n
aux₁ :
  Eq (α := m → R) ((A.mulVecLin : (a : n → R) → m → R) (Pi.single (M := fun (j : n) ↦ R) i 1) : m → R)
    (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
aux₂ :
  ∀ (e : n ≃ n),
    Eq.{u_2 + 1} (α := M₂)
      ((Basis.equiv (Pi.basisFun R n) v₂ e : (a : n → R) → M₂) (Pi.single (M := fun (j : n) ↦ R) i 1) : M₂)
      ((v₂ : (a : n) → M₂) ((e : (a : n) → n) i : n) : M₂)
⊢ Eq.{u_1 + 1} (α := M₁)
    ((((↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : (a : R) → M₁) 1 : M₁)
    ((((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂)) ∘ₗ
            LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → M₁)
        1 :
      M₁)

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

Premises used: Equiv.refl_apply, Module.Basis.equiv_apply, LinearMap.comp_apply, Matrix.toLin_self, map_sum, LinearMap.coe_single, LinearEquiv.coe_coe, map_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : Nontrivial R
A : Matrix m n R
⊢ A.rank ≤ Fintype.card m

Tactic:
(Submodule.finrank_le _).trans (finrank_pi R).le

Premises used: Matrix.rank, Eq.le, Module.finrank_pi, Submodule.finrank_le, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : Nontrivial R
A : Matrix m n R
⊢ A.rank ≤ Fintype.card m

Tactic:
exact (Submodule.finrank_le _).trans (finrank_pi R).le

Premises used: Eq.le, Module.finrank_pi, Submodule.finrank_le, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
m n : ℕ
A : Matrix (Fin m) (Fin n) R
⊢ A.rank ≤ m

Tactic:
A.rank_le_card_height.trans <| (Fintype.card_fin m).le

Premises used: Fintype.card_fin, Eq.le, Matrix.rank_le_card_height, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
A : Matrix m n R
rw : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(span R (range A.col))
rw₁ rw₂ : finrank R ↥(span R (range A.col)) = finrank R ↥(span R (range A.col))
⊢ A.rank = finrank R ↥(span R (range A.col))

Tactic:
rw [rank, Matrix.range_mulVecLin]

Premises used: Matrix.rank, Matrix.range_mulVecLin
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
A : Matrix m n R
rw : finrank R ↥(span R (range A.col)) = A.rank
rw₁ rw₂ : A.rank = A.rank
⊢ (toNat : (a : Cardinal.{max uR um}) → ℕ) A.cRank = A.rank

Tactic:
rw [cRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]

Premises used: Matrix.cRank_toNat_eq_finrank, Matrix.rank_eq_finrank_span_cols
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
A : Matrix m n R
rw : finrank R ↥(span R (range A.col)) = A.rank
rw₁ rw₂ : A.rank = A.rank
⊢ A.eRank.toNat = A.rank

Tactic:
rw [eRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]

Premises used: Matrix.eRank_toNat_eq_finrank, Matrix.rank_eq_finrank_span_cols
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
R : Type uR
inst : Field R
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : DecidableEq R
w : m → R
rw : finrank R ↥(LinearMap.range (diagonal w).mulVecLin) = Fintype.card.{um} { i : m // w i ≠ 0 }
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := m → R) (τ₁₂ := RingHom.id R)
          ((toLin' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (diagonal w))) =
    Fintype.card.{um} { i : m // w i ≠ 0 }
rw₂ :
  (toNat : (a : Cardinal.{max uR um}) → ℕ)
      (Module.rank R
        ↥(LinearMap.range (R := R) (M := m → R) (τ₁₂ := RingHom.id R)
            ((toLin' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (diagonal w)))) =
    Fintype.card.{um} { i : m // w i ≠ 0 }
rw₃ :
  (toNat : (a : Cardinal.{max uR um}) → ℕ)
      (LinearMap.rank (K := R) (V := m → R) (V' := m → R)
        ((toLin' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (diagonal w))) =
    Fintype.card.{um} { i : m // w i ≠ 0 }
rw₄ :
  (toNat : (a : Cardinal.{max uR um}) → ℕ) (↑(Fintype.card.{um} { i : m // w i ≠ 0 }) : Cardinal.{max uR um}) =
    Fintype.card.{um} { i : m // w i ≠ 0 }
rw₅ rw₆ : Fintype.card.{um} { i : m // w i ≠ 0 } = Fintype.card.{um} { i : m // w i ≠ 0 }
⊢ (diagonal w).rank = Fintype.card.{um} { i : m // w i ≠ 0 }

Tactic:
rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank,
    LinearMap.rank_diagonal, Cardinal.toNat_natCast]

Premises used: LinearMap.rank_diagonal, Matrix.rank, Matrix.toLin'_apply', LinearMap.rank, Cardinal.toNat_natCast, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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)
⊢ ∀ (i : m), Ne.{uR + 1} (α := R) ((fun (i : m) ↦ if w i = 0 then 1 else w i) i) 0

Tactic:
simp [ite_eq_iff']

Premises used: ite_eq_iff'
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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)
⊢ LinearIndependent R (M := (j : m) → R) fun (i : m) ↦
    Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i)

Tactic:
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'])
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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)
hli' :
  LinearIndependent R (M := (j : m) → R) fun (i : m) ↦
    Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i)
⊢ LinearIndependent (ι := { i : m // w i ≠ 0 }) R (M := (j : m) → R)
    ((fun (i : m) ↦ Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i)) ∘
      Subtype.val (p := fun (i : m) ↦ w i ≠ 0))

Tactic:
hli'.comp Subtype.val Subtype.val_injective

Premises used: Subtype.val_injective, Subtype.val, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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)
hli' :
  LinearIndependent R (M := (j : m) → R) fun (i : m) ↦
    Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i)
h :
  w' =
    (fun (i : m) ↦ Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i)) ∘
      Subtype.val (p := fun (i : m) ↦ w i ≠ 0)
⊢ LinearIndependent R w'

Tactic:
convert! hli'.comp Subtype.val Subtype.val_injective

Premises used: Subtype.val_injective, Subtype.val, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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)
hli' :
  LinearIndependent R (M := (j : m) → R) fun (i : m) ↦
    Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i)
h :
  ∀ (j : m) (hj : w j ≠ 0) (k : m),
    w' (Subtype.mk (p := fun (i : m) ↦ w i ≠ 0) j hj) k =
      Function.comp (α := { i : m // w i ≠ 0 })
        (fun (i : m) ↦ Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i))
        (Subtype.val (p := fun (i : m) ↦ w i ≠ 0)) (Subtype.mk (p := fun (i : m) ↦ w i ≠ 0) j hj) k
⊢ w' =
    (fun (i : m) ↦ Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i)) ∘
      Subtype.val (p := fun (i : m) ↦ w i ≠ 0)

Tactic:
ext ⟨j, hj⟩ k
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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)
hli' :
  LinearIndependent R (M := (j : m) → R) fun (i : m) ↦
    Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i)
j : m
hj : w j ≠ 0
k : m
⊢ w' (Subtype.mk (p := fun (i : m) ↦ w i ≠ 0) j hj) k =
    Function.comp (α := { i : m // w i ≠ 0 })
      (fun (i : m) ↦ Pi.single (M := fun (i : m) ↦ R) i ((fun (i : m) ↦ if w i = 0 then 1 else w i) i))
      (Subtype.val (p := fun (i : m) ↦ w i ≠ 0)) (Subtype.mk (p := fun (i : m) ↦ w i ≠ 0) j hj) k

Tactic:
simp [w', diagonal, hj, Pi.single_apply, eq_comm]

Premises used: Pi.single_apply, eq_comm, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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)
⊢ LinearIndependent R w'

Tactic:
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]
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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'
this : ∀ (a : m), diagonal w a = 0 ∨ ∃ (b : m), w b ≠ 0 ∧ diagonal w b = diagonal w a
⊢ insert 0 (range (diagonal w)ᵀ) = insert 0 (range w')

Tactic:
simpa [subset_antisymm_iff, subset_def, w']

Premises used: Set.subset_def, subset_antisymm_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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'
suffices : ∀ (a : m), diagonal w a = 0 ∨ ∃ (b : m), w b ≠ 0 ∧ diagonal w b = diagonal w a
⊢ insert 0 (range (diagonal w)ᵀ) = insert 0 (range w')

Tactic:
suffices ∀ a, diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a
      by simpa [subset_antisymm_iff, subset_def, w']
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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'
simp_rw : ∀ (a : m), (∀ (x : m), diagonal w x = diagonal w a → w x = 0) → diagonal w a = 0
⊢ ∀ (a : m), diagonal w a = 0 ∨ ∃ (b : m), w b ≠ 0 ∧ diagonal w b = diagonal w a

Tactic:
simp_rw [or_iff_not_imp_right, not_exists, not_and, not_imp_not]

Premises used: Classical.or_iff_not_imp_right, not_exists, not_and, not_imp_not
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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'
⊢ ∀ (a : m), (∀ (x : m), diagonal w x = diagonal w a → w x = 0) → diagonal w a = 0

Tactic:
simp +contextual [funext_iff, diagonal]

Premises used: funext_iff, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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'
⊢ insert 0 (range (diagonal w)ᵀ) = insert 0 (range w')

Tactic:
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]
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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))
rw₇ rw₈ : #(↑(range w') : Type (max uR um)) = #(↑(range w') : Type (max uR um))
⊢ (diagonal w).cRank = lift.{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']

Premises used: Cardinal.mk_range_eq_of_injective, Cardinal.lift_id', LinearIndependent.injective, Matrix.cRank, Cardinal.lift_umax, rank_span, Submodule.span_insert_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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 }
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 }
⊢ (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']

Premises used: Cardinal.lift_id', Matrix.cRank, Cardinal.lift_umax, Matrix.diagonal, Submodule.span_insert_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
R : Type uR
inst : Field R
inst_1 : DecidableEq m
w : m → R
⊢ (diagonal w).eRank = encard.{um} (α := m) {i : m | w i ≠ 0}

Tactic:
simp [eRank, cRank_diagonal, toENat_cardinalMk_subtype]

Premises used: Set.toENat_cardinalMk_subtype, Matrix.eRank, Matrix.cRank_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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
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
⊢ Eq (α := Submodule R (n → R)) (LinearMap.ker (Aᴴ * A).mulVecLin) (LinearMap.ker A.mulVecLin)

Tactic:
ext x