awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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)
⊢ 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₁)
have 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₂)
Tactic: have aux₂ := Basis.equiv_apply (Pi.basisFun R n) i v₂
-- 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 : 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.{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₁)
have 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)
Tactic: rw [toLin_eq_toLin', toLin'_apply'] at aux₁
Cleared hypotheses: aux₁, aux₂
-- 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 : 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.{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₁)
have 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)
Tactic: rw [Pi.basisFun_apply] at aux₁ aux₂
Cleared hypotheses: aux₁, aux₂
-- 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 : 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)
⊢ 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₁)
have 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₂)
Tactic: rw [Pi.basisFun_apply] at aux₁ aux₂
Cleared hypotheses: aux₁, aux₂
-- 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 : CommRing R
A : Matrix m n R
⊢ A.rank = finrank R ↥(span R (range A.col))
have rw : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(span R (range A.col))
Tactic: rw [rank, Matrix.range_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 : CommRing R
A : Matrix m n R
rw : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(span R (range A.col))
⊢ A.rank = finrank R ↥(span R (range A.col))
have rw₁ : finrank R ↥(span R (range A.col)) = finrank R ↥(span R (range A.col))
Tactic: rw [rank, Matrix.range_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 : CommRing R
A : Matrix m n R
⊢ (toNat : (a : Cardinal.{max uR um}) → ℕ) A.cRank = A.rank
have rw : finrank R ↥(span R (range A.col)) = A.rank
Tactic: rw [cRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]
-- 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 : CommRing R
A : Matrix m n R
rw : finrank R ↥(span R (range A.col)) = A.rank
⊢ (toNat : (a : Cardinal.{max uR um}) → ℕ) A.cRank = A.rank
have rw₁ : A.rank = A.rank
Tactic: rw [cRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]
-- 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 : CommRing R
A : Matrix m n R
⊢ A.eRank.toNat = A.rank
have rw : finrank R ↥(span R (range A.col)) = A.rank
Tactic: rw [eRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]
-- 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 : CommRing R
A : Matrix m n R
rw : finrank R ↥(span R (range A.col)) = A.rank
⊢ A.eRank.toNat = A.rank
have rw₁ : A.rank = A.rank
Tactic: rw [eRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ (diagonal w).rank = Fintype.card.{um} { i : m // w i ≠ 0 }
have rw : finrank R ↥(LinearMap.range (diagonal w).mulVecLin) = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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 }
⊢ (diagonal w).rank = Fintype.card.{um} { i : m // w i ≠ 0 }
have 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 }
Tactic: rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank,
    LinearMap.rank_diagonal, Cardinal.toNat_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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 }
⊢ (diagonal w).rank = Fintype.card.{um} { i : m // w i ≠ 0 }
have 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 }
Tactic: rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank,
    LinearMap.rank_diagonal, Cardinal.toNat_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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 }
⊢ (diagonal w).rank = Fintype.card.{um} { i : m // w i ≠ 0 }
have 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 }
Tactic: rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank,
    LinearMap.rank_diagonal, Cardinal.toNat_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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 }
⊢ (diagonal w).rank = Fintype.card.{um} { i : m // w i ≠ 0 }
have 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 }
Tactic: rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank,
    LinearMap.rank_diagonal, Cardinal.toNat_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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 }
⊢ (diagonal w).rank = Fintype.card.{um} { i : m // w i ≠ 0 }
have rw₅ : Fintype.card.{um} { i : m // w i ≠ 0 } = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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'
have 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)
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'])
-- 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)
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 R w'
have 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)
Tactic: convert! hli'.comp Subtype.val Subtype.val_injective
-- 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)
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)
⊢ 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)
have 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
Tactic: ext ⟨j, hj⟩ k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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)
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have h : 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]
-- 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'
⊢ insert 0 (range (diagonal w)ᵀ) = insert 0 (range w')
have suffices : ∀ (a : m), diagonal w a = 0 ∨ ∃ (b : m), w b ≠ 0 ∧ diagonal w b = diagonal w a
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']
-- 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'
⊢ ∀ (a : m), diagonal w a = 0 ∨ ∃ (b : m), w b ≠ 0 ∧ diagonal w b = diagonal w a
have simp_rw : ∀ (a : m), (∀ (x : m), diagonal w x = diagonal w a → w x = 0) → diagonal w a = 0
Tactic: simp_rw [or_iff_not_imp_right, not_exists, not_and, not_imp_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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'
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have hrw : 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]
-- 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')
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have rw : Module.rank R ↥(span R (range (diagonal w)ᵀ)) = 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']
-- 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 }
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have rw₁ : Module.rank R ↥(span R (insert 0 (range (diagonal w)ᵀ))) = 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']
-- 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 }
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have rw₂ : Module.rank R ↥(span R (insert 0 (range w'))) = 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']
-- 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 }
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have rw₃ : Module.rank R ↥(span R (range w')) = 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']
-- 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 }
⊢ (diagonal w).cRank = lift.{uR, um} #{ i : m // w i ≠ 0 }
have rw₄ : #(↑(range w') : Type (max uR um)) = 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']