awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)) :
      (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₁ :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑(A * A⁻¹) : Matrix n n R) : (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₂ :
  Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑1 : Matrix n n R))
    LinearMap.id
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R))
    LinearMap.id
have rw₃ : Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1) LinearMap.id
Tactic: rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)) :
      (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₁ :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑(A * A⁻¹) : Matrix n n R) : (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₂ :
  Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑1 : Matrix n n R))
    LinearMap.id
rw₃ : Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1) LinearMap.id
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R))
    LinearMap.id
have rw₄ : Eq (α := (n → R) →ₗ[R] n → R) LinearMap.id LinearMap.id
Tactic: rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R))
    LinearMap.id
have rw : Eq (α := (n → R) →ₗ[R] n → R)
  ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)) :
    (n → R) →ₗ[R] n → R)
  (LinearMap.id : (n → R) →ₗ[R] n → R)
Tactic: rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)) :
      (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R))
    LinearMap.id
have rw₁ : Eq (α := (n → R) →ₗ[R] n → R)
  ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑(A⁻¹ * A) : Matrix n n R) : (n → R) →ₗ[R] n → R)
  (LinearMap.id : (n → R) →ₗ[R] n → R)
Tactic: rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)) :
      (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₁ :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑(A⁻¹ * A) : Matrix n n R) : (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R))
    LinearMap.id
have rw₂ : Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑1 : Matrix n n R))
  LinearMap.id
Tactic: rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)) :
      (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₁ :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑(A⁻¹ * A) : Matrix n n R) : (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₂ :
  Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑1 : Matrix n n R))
    LinearMap.id
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R))
    LinearMap.id
have rw₃ : Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1) LinearMap.id
Tactic: rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)) :
      (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₁ :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑(A⁻¹ * A) : Matrix n n R) : (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₂ :
  Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑1 : Matrix n n R))
    LinearMap.id
rw₃ : Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1) LinearMap.id
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R))
    LinearMap.id
have rw₄ : Eq (α := (n → R) →ₗ[R] n → R) LinearMap.id LinearMap.id
Tactic: rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (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 : SpecialLinearGroup n R
⊢ Eq.{u_1 + 1} (α := S) (det.{u_1, u} (n := n) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) (↑g : Matrix n n R)))
    1
have rw : Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (↑g : Matrix n n R).det : S) (1 : S)
Tactic: rw [← f.map_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x : SpecialLinearGroup n R
h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) ⊥ x
have rw : x = 1
Tactic: rw [mem_bot, Subsingleton.elim x 1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x : SpecialLinearGroup n R
h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x
rw : x = 1
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) ⊥ x
have rw₁ : Eq (α := SpecialLinearGroup n R) 1 1
Tactic: rw [mem_bot, Subsingleton.elim x 1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
hA : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
i : n
⊢ (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)
have obtain : ∀ (r : R) (hr : (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)),
  (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)
Tactic: obtain ⟨r : R, hr : scalar n r = A⟩ := mem_range_scalar_of_commute_transvectionStruct fun t ↦
    Subtype.ext_iff.mp <| Subgroup.mem_center_iff.mp hA ⟨t.toMatrix, by simp⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
have inl : ∀ (hn : IsEmpty n),
  Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
Tactic: rcases isEmpty_or_nonempty n with hn | ⟨⟨i⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
inl :
  ∀ (hn : IsEmpty n),
    Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
      ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
have inr : ∀ (i : n),
  Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
Tactic: rcases isEmpty_or_nonempty n with hn | ⟨⟨i⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
have inr : ∀ (h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A),
  (↑A : Matrix n n R) i i ^ Fintype.card n = 1
Tactic: refine ⟨fun h ↦ ⟨A i i, ?_, ?_⟩, fun ⟨r, _, hr⟩ ↦ Subgroup.mem_center_iff.mpr fun B ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
inr :
  ∀ (h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A),
    (↑A : Matrix n n R) i i ^ Fintype.card n = 1
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
have inr₁ : ∀ (h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A),
  (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)
Tactic: refine ⟨fun h ↦ ⟨A i i, ?_, ?_⟩, fun ⟨r, _, hr⟩ ↦ Subgroup.mem_center_iff.mpr fun B ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
inr :
  ∀ (h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A),
    (↑A : Matrix n n R) i i ^ Fintype.card n = 1
inr₁ :
  ∀ (h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A),
    (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
have inr₂ : (∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)) →
  ∀ (r : R),
    r ^ Fintype.card n = 1 →
      ∀ (hr : (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)) (B : SpecialLinearGroup n R), B * A = A * B
Tactic: refine ⟨fun h ↦ ⟨A i i, ?_, ?_⟩, fun ⟨r, _, hr⟩ ↦ Subgroup.mem_center_iff.mpr fun B ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (hypothesis)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
⊢ (↑A : Matrix n n R) i i ^ Fintype.card n = 1
have this : Eq.{v + 1} (α := R) (det.{v, u} (n := n) ((scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i))) 1
Tactic: have : det ((scalar n) (A i i)) = 1 := (scalar_eq_self_of_mem_center h i).symm ▸ A.property
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
h : ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
r : R
left : r ^ Fintype.card n = 1
hr : (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
B : SpecialLinearGroup n R
⊢ B * A = A * B
have inr : (↑(B * A) : Matrix n n R) = (↑(A * B) : Matrix n n R)
Tactic: suffices ↑ₘ(B * A) = ↑ₘ(A * B) from Subtype.val_injective this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (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
i : n
A : ↥(center (SpecialLinearGroup n R))
this : Nonempty n
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i ^ Fintype.card n = 1
have obtain : ∀ (r : R) (hr : r ^ Fintype.card n = 1)
  (hr' : (scalar n : (a : R) → Matrix n n R) r = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)),
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i ^ Fintype.card n = 1
Tactic: obtain ⟨r, hr, hr'⟩ := mem_center_iff.mp A.property
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (hypothesis)
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
i : n
A : ↥(center (SpecialLinearGroup n R))
this : Nonempty n
r : R
hr : r ^ Fintype.card n = 1
hr' : (scalar n : (a : R) → Matrix n n R) r = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i ^ Fintype.card n = 1
have hr'₁ : (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i = r
Tactic: replace hr' : A.val i i = r := by simp only [← hr', scalar_apply, diagonal_apply_eq]
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (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
i : n
A : ↥(center (SpecialLinearGroup n R))
⊢ (fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
        (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
            Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
            (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
          ↥(center (SpecialLinearGroup n R))))
      ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
          (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
            ↥(rootsOfUnity (Fintype.card n) R)))
        A) =
    A
have refine : (↑(↑((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
              (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                  Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                  (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) sorry) sorry :
                ↥(center (SpecialLinearGroup n R))))
            ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
                (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) sorry :
                  ↥(rootsOfUnity (Fintype.card n) R)))
              A)) :
        SpecialLinearGroup n R) :
    Matrix n n R) =
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
Tactic: refine SetCoe.ext <| SetCoe.ext ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (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
i : n
A : ↥(center (SpecialLinearGroup n R))
⊢ (↑(↑((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
                (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                    Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
                  ↥(center (SpecialLinearGroup n R))))
              ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
                  (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
                    ↥(rootsOfUnity (Fintype.card n) R)))
                A)) :
          SpecialLinearGroup n R) :
      Matrix n n R) =
    (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
have obtain : ∀ (r : R),
  r ^ Fintype.card n = 1 →
    ∀ (hr : (scalar n : (a : R) → Matrix n n R) r = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)),
      (↑(↑((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
                    (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                        Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                        (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) sorry)
                        sorry :
                      ↥(center (SpecialLinearGroup n R))))
                  ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
                      (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) sorry :
                        ↥(rootsOfUnity (Fintype.card n) R)))
                    A)) :
              SpecialLinearGroup n R) :
          Matrix n n R) =
        (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
Tactic: obtain ⟨r, _, hr⟩ := mem_center_iff.mp A.property
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (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
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
⊢ (fun (A : ↥(center (SpecialLinearGroup n R))) ↦
        (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
          ↥(rootsOfUnity (Fintype.card n) R)))
      ((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
          (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
              Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
              (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
            ↥(center (SpecialLinearGroup n R))))
        a) =
    a
have obtain : ∀ (a inv : R) (val_inv : a * inv = 1) (inv_val : inv * a = 1)
  (ha :
    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R)
      { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }),
  (fun (A : ↥(center (SpecialLinearGroup n R))) ↦
        (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) sorry :
          ↥(rootsOfUnity (Fintype.card n) R)))
      ((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
          (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
              Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
              (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) sorry) sorry :
            ↥(center (SpecialLinearGroup n R))))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R) x)
          { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val } ha)) =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R) x)
      { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } ha
Tactic: obtain ⟨⟨a, _⟩, ha⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (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
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ rootsOfUnity.mkOfPowEq ((↑(↑(A * B) : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ =
    HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
      (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
      (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
have dsimp : rootsOfUnity.mkOfPowEq
    (((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i) sorry =
  HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
    (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) sorry)
    (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (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
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ rootsOfUnity.mkOfPowEq
      (((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i) ⋯ =
    HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
      (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
      (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
have a : (↑(↑(rootsOfUnity.mkOfPowEq
            (((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i)
            sorry) :
        Rˣ) :
    R) =
  (↑(↑(HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
            (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) sorry)
            (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) sorry)) :
        Rˣ) :
    R)
Tactic: ext