awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
k : ℕ
hk : k ≤ n
⊢ card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
have zero : ∀ (hk : 0 ≤ n), card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
Tactic: induction k with
  | zero =>
      have : Unique { s : Fin 0 → V // (⊤ : Submodule K (Fin 0 →₀ K)) = ⊥ } :=
        uniqueOfSubsingleton ⟨0, Subsingleton.elim ..⟩
      simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
  | succ k ih =>
      have (s : { s : Fin k → V // LinearIndependent K s }) :
          card ((Submodule.span K (Set.range (s : Fin k → V)))ᶜ : Set (V)) =
          (q) ^ n - (q) ^ k := by
            rw [card_compl_set, Module.card_eq_pow_finrank (K := K)
            (V := ((Submodule.span K (Set.range (s : Fin k → V))) : Set (V)))]
            simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]
            rw [Module.card_eq_pow_finrank (K := K)]
      simp [card_congr (equiv_linearIndependent k), sum_congr _ _ this, ih (Nat.le_of_succ_le hk),
        mul_comm, Fin.prod_univ_succAbove _ (Fin.last k), -Set.fintypeCard_eq_ncard]
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
k : ℕ
hk : k ≤ n
zero : ∀ (hk : 0 ≤ n), card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
⊢ card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
have succ : ∀ (k : ℕ)
  (ih : ∀ (hk : k ≤ n), card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ)))
  (hk : k + 1 ≤ n),
  card.{u_2} { s : Fin (k + 1) → V // LinearIndependent K s } = ∏ i : Fin (k + 1), (q ^ n - q ^ (↑i : ℕ))
Tactic: induction k with
  | zero =>
      have : Unique { s : Fin 0 → V // (⊤ : Submodule K (Fin 0 →₀ K)) = ⊥ } :=
        uniqueOfSubsingleton ⟨0, Subsingleton.elim ..⟩
      simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
  | succ k ih =>
      have (s : { s : Fin k → V // LinearIndependent K s }) :
          card ((Submodule.span K (Set.range (s : Fin k → V)))ᶜ : Set (V)) =
          (q) ^ n - (q) ^ k := by
            rw [card_compl_set, Module.card_eq_pow_finrank (K := K)
            (V := ((Submodule.span K (Set.range (s : Fin k → V))) : Set (V)))]
            simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]
            rw [Module.card_eq_pow_finrank (K := K)]
      simp [card_congr (equiv_linearIndependent k), sum_congr _ _ this, ih (Nat.le_of_succ_le hk),
        mul_comm, Fin.prod_univ_succAbove _ (Fin.last k), -Set.fintypeCard_eq_ncard]
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ LinearIndependent 𝔽 (↑M : Matrix (Fin n) (Fin n) 𝔽).col
have apply : Fintype.card (Fin n) = Set.finrank 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col)
Tactic: apply linearIndependent_iff_card_eq_finrank_span.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ Fintype.card (Fin n) = Set.finrank 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col)
have rw : Fintype.card (Fin n) = finrank 𝔽 ↥(Submodule.span 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col))
Tactic: rw [Set.finrank, ← rank_eq_finrank_span_cols, rank_unit]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
rw : Fintype.card (Fin n) = finrank 𝔽 ↥(Submodule.span 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col))
⊢ Fintype.card (Fin n) = Set.finrank 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col)
have rw₁ : Fintype.card (Fin n) = (↑M : Matrix (Fin n) (Fin n) 𝔽).rank
Tactic: rw [Set.finrank, ← rank_eq_finrank_span_cols, rank_unit]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
rw : Fintype.card (Fin n) = finrank 𝔽 ↥(Submodule.span 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col))
rw₁ : Fintype.card (Fin n) = (↑M : Matrix (Fin n) (Fin n) 𝔽).rank
⊢ Fintype.card (Fin n) = Set.finrank 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col)
have rw₂ : Fintype.card (Fin n) = Fintype.card (Fin n)
Tactic: rw [Set.finrank, ← rank_eq_finrank_span_cols, rank_unit]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
⊢ IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
have have : ∀
  (this :
    Invertible (α := Matrix (Fin n) (Fin n) 𝔽) (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))),
  IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
Tactic: have := (Pi.basisFun 𝔽 (Fin n)).invertibleToMatrix b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
this :
  Invertible (α := Matrix (Fin n) (Fin n) 𝔽) (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))
⊢ IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
have rw : IsUnit
  (det (n := Fin n)
    (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑(basisOfPiSpaceOfLinearIndependent sorry) : (a : Fin n) → Fin n → 𝔽)))
Tactic: rw [← Basis.coePiBasisFun.toMatrix_eq_transpose,
      ← coe_basisOfPiSpaceOfLinearIndependent M.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
let let₁ let₂ : IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
⊢ IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
have let₃ : let b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent sorry;
∀
  (this :
    Invertible (α := Matrix (Fin n) (Fin n) 𝔽) (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))),
  IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
Tactic: classical
    let b := basisOfPiSpaceOfLinearIndependent M.2
    have := (Pi.basisFun 𝔽 (Fin n)).invertibleToMatrix b
    rw [← Basis.coePiBasisFun.toMatrix_eq_transpose,
      ← coe_basisOfPiSpaceOfLinearIndependent M.2]
    exact isUnit_det_of_invertible _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
let let₁ let₂ : IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
let₃ :
  let b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯;
  ∀
    (this :
      Invertible (α := Matrix (Fin n) (Fin n) 𝔽)
        (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))),
    IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
⊢ IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
have let₄ : let b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent sorry;
∀
  (this :
    Invertible (α := Matrix (Fin n) (Fin n) 𝔽) (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))),
  IsUnit
    (det (n := Fin n)
      (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑(basisOfPiSpaceOfLinearIndependent sorry) : (a : Fin n) → Fin n → 𝔽)))
Tactic: classical
    let b := basisOfPiSpaceOfLinearIndependent M.2
    have := (Pi.basisFun 𝔽 (Fin n)).invertibleToMatrix b
    rw [← Basis.coePiBasisFun.toMatrix_eq_transpose,
      ← coe_basisOfPiSpaceOfLinearIndependent M.2]
    exact isUnit_det_of_invertible _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
⊢ Nat.card.{u_1} (GL (Fin n) 𝔽) = ∏ i : Fin n, (q ^ n - q ^ (↑i : ℕ))
have rw : n ≤ finrank 𝔽 (Fin n → 𝔽)
Tactic: rw [Nat.card_congr (equiv_GL_linearindependent n), card_linearIndependent,
    Module.finrank_fintype_fun_eq_card, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
⊢ (↑A : Matrix n n R).det * (↑A⁻¹ : Matrix n n R).det = 1
have rw : ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)).det = 1
Tactic: rw [← det_mul, A.mul_inv, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
rw : ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)).det = 1
⊢ (↑A : Matrix n n R).det * (↑A⁻¹ : Matrix n n R).det = 1
have rw₁ : Eq.{v + 1} (α := R) (Matrix.det.{v, u} (n := n) 1) 1
Tactic: rw [← det_mul, A.mul_inv, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
rw : ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)).det = 1
rw₁ : Eq.{v + 1} (α := R) (Matrix.det.{v, u} (n := n) 1) 1
⊢ (↑A : Matrix n n R).det * (↑A⁻¹ : Matrix n n R).det = 1
have rw₂ : Eq.{v + 1} (α := R) 1 1
Tactic: rw [← det_mul, A.mul_inv, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
⊢ (↑A⁻¹ : Matrix n n R).det * (↑A : Matrix n n R).det = 1
have rw : ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)).det = 1
Tactic: rw [← det_mul, A.inv_mul, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
rw : ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)).det = 1
⊢ (↑A⁻¹ : Matrix n n R).det * (↑A : Matrix n n R).det = 1
have rw₁ : Eq.{v + 1} (α := R) (Matrix.det.{v, u} (n := n) 1) 1
Tactic: rw [← det_mul, A.inv_mul, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
rw : ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)).det = 1
rw₁ : Eq.{v + 1} (α := R) (Matrix.det.{v, u} (n := n) 1) 1
⊢ (↑A⁻¹ : Matrix n n R).det * (↑A : Matrix n n R).det = 1
have rw₂ : Eq.{v + 1} (α := R) 1 1
Tactic: rw [← det_mul, A.inv_mul, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
u : Rˣ
⊢ (det : (a : GL n R) → Rˣ) ((scalar n : (a : Rˣ) → GL n R) u) = u ^ Fintype.card n
have huv : (↑((det : (a : GL n R) → Rˣ) ((scalar n : (a : Rˣ) → GL n R) u)) : R) = (↑(u ^ Fintype.card n) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ Eq.{u_1 + 1} (α := Sˣ) ((det : (a : GL n S) → Sˣ) ((map f : (a : GL n R) → GL n S) g) : Sˣ)
    (((Units.map (↑f : R →* S) : MonoidHom.{v, u_1} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ((det : (a : GL n R) → Rˣ) g) : Sˣ)
have huv : Eq.{u_1 + 1} (α := S) (↑((det : (a : GL n S) → Sˣ) ((map f : (a : GL n R) → GL n S) g)) : S)
  (↑(((Units.map (↑f : R →* S) : MonoidHom.{v, u_1} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ((det : (a : GL n R) → Rˣ) g)) : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ Eq.{u_1 + 1} (α := S) (↑((det : (a : GL n S) → Sˣ) ((map f : (a : GL n R) → GL n S) g)) : S)
    (↑(((Units.map (↑f : R →* S) : MonoidHom.{v, u_1} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ((det : (a : GL n R) → Rˣ) g)) : S)
have huv : Eq.{u_1 + 1} (α := S)
  (Matrix.det.{u_1, u} (n := n)
      (((↑f.mapMatrix : Matrix n n R →* Matrix n n S) : (a : Matrix n n R) → Matrix n n S) (↑g : Matrix n n R)) :
    S)
  ((f : (a : R) → S) (↑g : Matrix n n R).det : S)
Tactic: simp only [map,
    Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ HMul.hMul (α := Matrix n n S) ((↑g : Matrix n n R).map (⇑f : (a : R) → S))
      ((↑g : Matrix n n R)⁻¹.map (⇑f : (a : R) → S)) =
    1
have rw : Eq (α := Matrix n n S) (((↑g : Matrix n n R) * (↑g : Matrix n n R)⁻¹).map (⇑f : (a : R) → S)) 1
Tactic: rw [← Matrix.map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ HMul.hMul (α := Matrix n n S) ((↑g : Matrix n n R)⁻¹.map (⇑f : (a : R) → S))
      ((↑g : Matrix n n R).map (⇑f : (a : R) → S)) =
    1
have rw : Eq (α := Matrix n n S) (((↑g : Matrix n n R)⁻¹ * (↑g : Matrix n n R)).map (⇑f : (a : R) → S)) 1
Tactic: rw [← Matrix.map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
g : SpecialLinearGroup n R
⊢ Eq (α := GL n T)
    ((GeneralLinearGroup.map (algebraMap S T) : (a : GL n S) → GL n T)
        ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g) :
      GL n T)
    ((mapGL T : (a : SpecialLinearGroup n R) → GL n T) g : GL n T)
have huv : ∀ (i j : n),
  Eq.{u_2 + 1} (α := T)
    ((↑((GeneralLinearGroup.map (algebraMap S T) : (a : GL n S) → GL n T)
            ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g)) :
        Matrix n n T)
      i j)
    ((↑((mapGL T : (a : SpecialLinearGroup n R) → GL n T) g) : Matrix n n T) i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (goal)
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ Membership.mem (γ := Subgroup (GL n R)) (GLPos n R) (-(↑g : GL n R))
have rw : 0 < (↑(↑g : GL n R) : Matrix n n R).det
Tactic: rw [mem_glpos, GeneralLinearGroup.val_det_apply, Units.val_neg, det_neg,
        (Fact.out (p := Even <| Fintype.card n)).neg_one_pow, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic
have simp_rw : (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
      Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
    ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).discr = 0 ↔
  m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
Tactic: simp_rw [IsParabolic, discr_conj, Set.mem_range, ← Matrix.coe_units_inv,
    Units.eq_mul_inv_iff_mul_eq, scalar_apply, ← smul_eq_diagonal_mul, smul_eq_mul_diagonal,
    Units.mul_right_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
simp_rw :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic
have simp_rw₁ : (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
      Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
    m.discr = 0 ↔
  m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
Tactic: simp_rw [IsParabolic, discr_conj, Set.mem_range, ← Matrix.coe_units_inv,
    Units.eq_mul_inv_iff_mul_eq, scalar_apply, ← smul_eq_diagonal_mul, smul_eq_mul_diagonal,
    Units.mul_right_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
simp_rw :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
simp_rw₁ :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      m.discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic
have simp_rw₂ : (¬∃ (y : R),
        (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y =
          (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹) ∧
    m.discr = 0 ↔
  (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
Tactic: simp_rw [IsParabolic, discr_conj, Set.mem_range, ← Matrix.coe_units_inv,
    Units.eq_mul_inv_iff_mul_eq, scalar_apply, ← smul_eq_diagonal_mul, smul_eq_mul_diagonal,
    Units.mul_right_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
simp_rw :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
simp_rw₁ :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      m.discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
simp_rw₂ :
  (¬∃ (y : R),
          (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y =
            (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹) ∧
      m.discr = 0 ↔
    (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic
have simp_rw₃ : (¬∃ (y : R),
        (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y =
          (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g⁻¹ : Matrix (Fin 2) (Fin 2) R)) ∧
    m.discr = 0 ↔
  (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
Tactic: simp_rw [IsParabolic, discr_conj, Set.mem_range, ← Matrix.coe_units_inv,
    Units.eq_mul_inv_iff_mul_eq, scalar_apply, ← smul_eq_diagonal_mul, smul_eq_mul_diagonal,
    Units.mul_right_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
simp_rw :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
simp_rw₁ :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      m.discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
simp_rw₂ :
  (¬∃ (y : R),
          (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y =
            (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹) ∧
      m.discr = 0 ↔
    (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
simp_rw₃ :
  (¬∃ (y : R),
          (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y =
            (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g⁻¹ : Matrix (Fin 2) (Fin 2) R)) ∧
      m.discr = 0 ↔
    (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic
have simp_rw₄ : (¬∃ (y : R),
        HMul.hMul (α := Matrix (Fin 2) (Fin 2) R)
            ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y : Matrix (Fin 2) (Fin 2) R)
            (↑g : Matrix (Fin 2) (Fin 2) R) =
          (↑g : Matrix (Fin 2) (Fin 2) R) * m) ∧
    m.discr = 0 ↔
  (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
Tactic: simp_rw [IsParabolic, discr_conj, Set.mem_range, ← Matrix.coe_units_inv,
    Units.eq_mul_inv_iff_mul_eq, scalar_apply, ← smul_eq_diagonal_mul, smul_eq_mul_diagonal,
    Units.mul_right_inj]