awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this_1 : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
this :
  Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
            (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
          g) :
      Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
            ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
              ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i)
⊢ Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      (Matrix.diagonal fun (x : Module.Free.ChooseBasisIndex R V) ↦ r)
      (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
              (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
            g) :
        Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) ↔
    (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have simp : Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (Matrix.diagonal fun (x : Module.Free.ChooseBasisIndex R V) ↦ r)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      (((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
              (((↑g : V ≃ₗ[R] V) : (a : V) → V) ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j : V)) :
            Finsupp.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i) ↔
  (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
⊢ Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      (Matrix.diagonal fun (x : Module.Free.ChooseBasisIndex R V) ↦ r)
      (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
              (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
            g) :
        Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) ↔
    (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have inr : Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
  (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
          (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
        g) :
    Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
  ((Matrix.of :
      (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
        Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    fun (i j : Module.Free.ChooseBasisIndex R V) ↦
    ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
          ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
            ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
        (a : Module.Free.ChooseBasisIndex R V) → R)
      i)
Tactic: suffices ((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) =
    Matrix.of fun i j ↦ (b.repr (g (b j))) i by
    simp only [this]
    rw [← (LinearMap.toMatrix b b).injective.eq_iff]
    simp only [← Matrix.ext_iff, Matrix.of_apply]
    apply forall₂_congr
    intro i j
    simp [Matrix.diagonal, LinearMap.toMatrix_apply,
      Finsupp.single, Pi.single_apply, Iff.symm eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
⊢ Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
            (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
          g) :
      Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
            ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
              ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i)
have inr : ∀ (i j : Module.Free.ChooseBasisIndex R V),
  Eq.{u_1 + 1} (α := R)
    ((↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
                (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
              g) :
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        i j :
      R)
    ((Matrix.of :
          (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
            Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        (fun (i j : Module.Free.ChooseBasisIndex R V) ↦
          ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
                ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
                  ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
              (a : Module.Free.ChooseBasisIndex R V) → R)
            i)
        i j :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : SpecialLinearGroup R V
hg : Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g
x : V
H : (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) =
  HSMul.hSMul (β := V →ₗ[R] V)
    (⋯.choose (p := fun (r : R) ↦
      r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
    LinearMap.id :=
  ⋯
⊢ ((↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x =
    ⋯.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) •
      x
have H₁ : ∀ (x : V),
  Eq (α := V) (((↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
    ((HSMul.hSMul (β := V →ₗ[R] V)
            (sorry.choose (p := fun (r : R) ↦
              r ^ Module.finrank R V = 1 ∧
                (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
            LinearMap.id :
          (a : V) → V)
        x :
      V)
Tactic: rw [LinearMap.ext_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (LinearMap.equivOfIsUnitDet ⋯) : Rˣ) (1 : Rˣ)
have simp : (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
Tactic: simp only [← Units.val_inj, LinearEquiv.coe_det, LinearMap.coe_equivOfIsUnitDet,
      LinearMap.det_smul, LinearMap.det_id, mul_one, Units.val_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
have this : (↑(↑r : Rˣ) : R) ^ max (Module.finrank R V) 1 = 1
Tactic: have := (mem_rootsOfUnity' _ _).mp r.prop
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : (↑(↑r : Rˣ) : R) ^ max (Module.finrank R V) 1 = 1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
have inl : ∀ (h : max (Module.finrank R V) 1 = Module.finrank R V) (h' : 1 ≤ Module.finrank R V),
  (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
Tactic: rcases max_cases (Module.finrank R V) 1 with ⟨h, h'⟩ |  ⟨h, h'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : (↑(↑r : Rˣ) : R) ^ max (Module.finrank R V) 1 = 1
inl :
  ∀ (h : max (Module.finrank R V) 1 = Module.finrank R V) (h' : 1 ≤ Module.finrank R V),
    (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
have inr : ∀ (h : max (Module.finrank R V) 1 = 1) (h' : Module.finrank R V < 1), (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
Tactic: rcases max_cases (Module.finrank R V) 1 with ⟨h, h'⟩ |  ⟨h, h'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : (↑(↑r : Rˣ) : R) ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
have this₁ : (↑(↑r : Rˣ) : R) = 1
Tactic: simp_rw [h, pow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V))
    (Subtype.mk (p := fun (u : V ≃ₗ[R] V) ↦
      Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ)) (LinearMap.equivOfIsUnitDet ⋯)
      ⋯)
have simp : ∃ (r_1 : R),
  r_1 ^ Module.finrank R V = 1 ∧
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id = HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id
Tactic: simp only [mem_center_iff, LinearMap.coe_equivOfIsUnitDet]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ ∃ (r_1 : R),
    r_1 ^ Module.finrank R V = 1 ∧
      HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id = HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id
have h : (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1 ∧
  HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id =
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id
Tactic: use r.val
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1 ∧
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id =
      HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id
have h : (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
Tactic: simp only [and_true]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
have h : ∀ (r : Rˣ) (hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r),
  (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1
Tactic: let ⟨r, hr⟩ := r
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1
have pos : ∀ (hV : Module.finrank R V = 0),
  (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1
Tactic: by_cases hV : Module.finrank R V = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
pos :
  ∀ (hV : Module.finrank R V = 0),
    (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
              Rˣ) :
          R) ^
        Module.finrank R V =
      1
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1
have neg : ∀ (hV : ¬Module.finrank R V = 0),
  (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1
Tactic: by_cases hV : Module.finrank R V = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
hV : ¬Module.finrank R V = 0
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1
have hV₁ : 1 ≤ Module.finrank R V
Tactic: rw [← ne_eq, ← Nat.one_le_iff_ne_zero] at hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
r_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
hV : 1 ≤ Module.finrank R V
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1
have hr₁ : (↑r : R) ^ Module.finrank R V = 1
Tactic: rw [mem_rootsOfUnity', max_eq_left hV] at hr
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : Nontrivial V
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
have hV₁ : 0 < Module.finrank R V
Tactic: rw [← Module.finrank_pos_iff_of_free (R := R)] at hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 0 < Module.finrank R V
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
have hV₁ : 1 ≤ Module.finrank R V
Tactic: replace hV : 1 ≤ Module.finrank R V := hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
have hr : sorry.choose (p := fun (r : R) ↦
      r ^ Module.finrank R V = 1 ∧
        (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) ^
    Module.finrank R V =
  1
Tactic: have hr := (mem_center_iff.mp g.prop).choose_spec.1
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R :=
  ⋯.choose (p := fun (r : R) ↦
    r ^ Module.finrank R V = 1 ∧
      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)
hr : r ^ Module.finrank R V = 1
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
have hr₁ : r ^ max (Module.finrank R V) 1 = 1
Tactic: rw [← Nat.max_eq_left hV] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R :=
  ⋯.choose (p := fun (r : R) ↦
    r ^ Module.finrank R V = 1 ∧
      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ IsUnit r
have rw : IsUnit.{u_1} (M := R) 1
Tactic: rw [← isUnit_pow_iff _, hr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R :=
  ⋯.choose (p := fun (r : R) ↦
    r ^ Module.finrank R V = 1 ∧
      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)
hr : r ^ max (Module.finrank R V) 1 = 1
rw : IsUnit.{u_1} (M := R) 1
⊢ IsUnit r
have rw₁ : max (Module.finrank R V) 1 ≠ 0
Tactic: rw [← isUnit_pow_iff _, hr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R :=
  ⋯.choose (p := fun (r : R) ↦
    r ^ Module.finrank R V = 1 ∧
      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ max (Module.finrank R V) 1 ≠ 0
have rw : Module.finrank R V ≠ 0
Tactic: rw [Nat.max_eq_left hV]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R :=
  ⋯.choose (p := fun (r : R) ↦
    r ^ Module.finrank R V = 1 ∧
      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
have this : IsUnit r
Tactic: have : IsUnit r := by
          rw [← isUnit_pow_iff _, hr]
          · exact isUnit_one
          rw [Nat.max_eq_left hV]
          exact Nat.ne_zero_of_lt hV