awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * (↑z : M) = 1
h₂ : x * y = 1
h : x * 1 = (↑z : M)
h₃ : x * (y * (↑z : M)) = (↑z : M)
⊢ x = (↑z : M)
have h₄ : x * y * (↑z : M) = (↑z : M)
Tactic: rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * (↑z : M) = 1
h₂ : x * y = 1
h : x * 1 = (↑z : M)
h₃ : x * (y * (↑z : M)) = (↑z : M)
h₄ : x * y * (↑z : M) = (↑z : M)
⊢ x = (↑z : M)
have h₅ : 1 * (↑z : M) = (↑z : M)
Tactic: rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * (↑z : M) = 1
h₂ : x * y = 1
h : x * 1 = (↑z : M)
h₃ : x * (y * (↑z : M)) = (↑z : M)
h₄ : x * y * (↑z : M) = (↑z : M)
h₅ : 1 * (↑z : M) = (↑z : M)
⊢ x = (↑z : M)
have h₆ : (↑z : M) = (↑z : M)
Tactic: rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S.leftInv.leftInv = S
have refine : S ≤ S.leftInv.leftInv
Tactic: refine le_antisymm S.leftInv_leftInv_le ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = (↑(IsUnit.unit ⋯)⁻¹⁻¹ : M)
have rw : x = (↑(IsUnit.unit sorry) : M)
Tactic: rw [inv_inv (hS hx).unit]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (hypothesis)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x ∈ S.leftInv.leftInv
have this : x = (↑(IsUnit.unit sorry)⁻¹⁻¹ : M)
Tactic: have : x = ((hS hx).unit⁻¹⁻¹ : Mˣ) := by
    rw [inv_inv (hS hx).unit]
    rfl
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = (↑(IsUnit.unit ⋯)⁻¹⁻¹ : M)
⊢ x ∈ S.leftInv.leftInv
have rw : (↑(IsUnit.unit sorry)⁻¹⁻¹ : M) ∈ S.leftInv.leftInv
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : ↥S.leftInv
⊢ (↑(S.fromLeftInv x) : M) * (↑x : M) = 1
have rw : (↑x : M) * (↑(S.fromLeftInv x) : M) = 1
Tactic: rw [mul_comm, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : ↥S.leftInv
rw : (↑x : M) * (↑(S.fromLeftInv x) : M) = 1
⊢ (↑(S.fromLeftInv x) : M) * (↑x : M) = 1
have rw₁ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [mul_comm, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S.leftInv
b : M
⊢ (↑(S.fromLeftInv a) : M) = b ↔ (↑a : M) * b = 1
have rw : (↑a : M) * (↑(S.fromLeftInv a) : M) = (↑a : M) * b ↔ (↑a : M) * b = 1
Tactic: rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S.leftInv
b : M
rw : (↑a : M) * (↑(S.fromLeftInv a) : M) = (↑a : M) * b ↔ (↑a : M) * b = 1
⊢ (↑(S.fromLeftInv a) : M) = b ↔ (↑a : M) * b = 1
have rw₁ : 1 = (↑a : M) * b ↔ (↑a : M) * b = 1
Tactic: rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S.leftInv
b : M
rw : (↑a : M) * (↑(S.fromLeftInv a) : M) = (↑a : M) * b ↔ (↑a : M) * b = 1
rw₁ : 1 = (↑a : M) * b ↔ (↑a : M) * b = 1
⊢ (↑(S.fromLeftInv a) : M) = b ↔ (↑a : M) * b = 1
have rw₂ : (↑a : M) * b = 1 ↔ (↑a : M) * b = 1
Tactic: rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw₁ : (↑(y * x) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₁ : (↑(y * x) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw₂ : (↑y : M) * (↑x : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₁ : (↑(y * x) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₂ : (↑y : M) * (↑x : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw₃ : (↑y : M) * (↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₁ : (↑(y * x) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₂ : (↑y : M) * (↑x : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₃ : (↑y : M) * (↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw₄ : (↑y : M) * ((↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M))) = 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₁ : (↑(y * x) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₂ : (↑y : M) * (↑x : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₃ : (↑y : M) * (↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
rw₄ : (↑y : M) * ((↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M))) = 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw₅ : (↑y : M) * ((↑x : M) * (↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₁ : (↑(y * x) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₂ : (↑y : M) * (↑x : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₃ : (↑y : M) * (↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
rw₄ : (↑y : M) * ((↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M))) = 1
rw₅ : (↑y : M) * ((↑x : M) * (↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw₆ : (↑y : M) * (1 * (↑(S.fromLeftInv y) : M)) = 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₁ : (↑(y * x) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₂ : (↑y : M) * (↑x : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₃ : (↑y : M) * (↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
rw₄ : (↑y : M) * ((↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M))) = 1
rw₅ : (↑y : M) * ((↑x : M) * (↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
rw₆ : (↑y : M) * (1 * (↑(S.fromLeftInv y) : M)) = 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw₇ : (↑y : M) * (↑(S.fromLeftInv y) : M) = 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
rw : (↑(x * y) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₁ : (↑(y * x) : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₂ : (↑y : M) * (↑x : M) * (↑(S.fromLeftInv x * S.fromLeftInv y) : M) = 1
rw₃ : (↑y : M) * (↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
rw₄ : (↑y : M) * ((↑x : M) * ((↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M))) = 1
rw₅ : (↑y : M) * ((↑x : M) * (↑(S.fromLeftInv x) : M) * (↑(S.fromLeftInv y) : M)) = 1
rw₆ : (↑y : M) * (1 * (↑(S.fromLeftInv y) : M)) = 1
rw₇ : (↑y : M) * (↑(S.fromLeftInv y) : M) = 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)
have rw₈ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ←
        mul_assoc (x : M), mul_fromLeftInv, one_mul, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
⊢ (fun (x : ↥S) ↦ (Subtype.mk (p := fun (x : M) ↦ x ∈ S.leftInv) (↑(IsUnit.unit ⋯)⁻¹ : M) ⋯ : ↥S.leftInv))
      ((↑S.fromCommLeftInv : OneHom ↥S.leftInv ↥S).toFun x) =
    x
have a : (↑((fun (x : ↥S) ↦ (Subtype.mk (p := fun (x : M) ↦ x ∈ S.leftInv) (↑(IsUnit.unit sorry)⁻¹ : M) sorry : ↥S.leftInv))
        ((↑S.fromCommLeftInv : OneHom ↥S.leftInv ↥S).toFun x)) :
    M) =
  (↑x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ (↑S.fromCommLeftInv : OneHom ↥S.leftInv ↥S).toFun
      ((fun (x : ↥S) ↦ (Subtype.mk (p := fun (x : M) ↦ x ∈ S.leftInv) (↑(IsUnit.unit ⋯)⁻¹ : M) ⋯ : ↥S.leftInv))
        (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx)) =
    Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx
have a : (↑((↑S.fromCommLeftInv : OneHom ↥S.leftInv ↥S).toFun
        ((fun (x : ↥S) ↦ (Subtype.mk (p := fun (x : M) ↦ x ∈ S.leftInv) (↑(IsUnit.unit sorry)⁻¹ : M) sorry : ↥S.leftInv))
          (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx))) :
    M) =
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ (↑(((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x) : M) * (↑x : M) = 1
have h : x = (S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) (((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x)
Tactic: convert! S.mul_leftInvEquiv hS ((S.leftInvEquiv hS).symm x)
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ (↑x : M) * (↑(((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x) : M) = 1
have h : x = (S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) (((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x)
Tactic: convert! S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Group M
S : Submonoid M
x : ↥S.leftInv
⊢ (↑(S.fromLeftInv x) : M) = (↑x : M)⁻¹
have rw : (↑x : M) * (↑(S.fromLeftInv x) : M) = (↑x : M) * (↑x : M)⁻¹
Tactic: rw [← mul_right_inj (x : M), mul_inv_cancel, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Group M
S : Submonoid M
x : ↥S.leftInv
rw : (↑x : M) * (↑(S.fromLeftInv x) : M) = (↑x : M) * (↑x : M)⁻¹
⊢ (↑(S.fromLeftInv x) : M) = (↑x : M)⁻¹
have rw₁ : (↑x : M) * (↑(S.fromLeftInv x) : M) = 1
Tactic: rw [← mul_right_inj (x : M), mul_inv_cancel, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Group M
S : Submonoid M
x : ↥S.leftInv
rw : (↑x : M) * (↑(S.fromLeftInv x) : M) = (↑x : M) * (↑x : M)⁻¹
rw₁ : (↑x : M) * (↑(S.fromLeftInv x) : M) = 1
⊢ (↑(S.fromLeftInv x) : M) = (↑x : M)⁻¹
have rw₂ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [← mul_right_inj (x : M), mul_inv_cancel, mul_fromLeftInv]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
    (↑x : M)⁻¹
have rw : (↑x : M) * (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
  (↑x : M) * (↑x : M)⁻¹
Tactic: rw [← mul_right_inj (x : M), mul_inv_cancel, mul_leftInvEquiv_symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
rw :
  (↑x : M) *
      (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
    (↑x : M) * (↑x : M)⁻¹
⊢ (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
    (↑x : M)⁻¹
have rw₁ : (↑x : M) * (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
  1
Tactic: rw [← mul_right_inj (x : M), mul_inv_cancel, mul_leftInvEquiv_symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
rw :
  (↑x : M) *
      (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
    (↑x : M) * (↑x : M)⁻¹
rw₁ :
  (↑x : M) *
      (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
    1
⊢ (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
    (↑x : M)⁻¹
have rw₂ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [← mul_right_inj (x : M), mul_inv_cancel, mul_leftInvEquiv_symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Subsemigroup.Center (goal)
Goal:
M : Type u_1
inst : Semigroup M
z : M
⊢ Membership.mem (γ := Subsemigroup M) (center M) z ↔ ∀ (g : M), g * z = z * g
have rw : Membership.mem (γ := Subsemigroup M) (center M) z ↔ z ∈ Set.center M
Tactic: rw [← Semigroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
P Q : Sylow p G
h : (↑P : Subgroup G) = (↑Q : Subgroup G)
⊢ P = Q
have mk : ∀ (toSubgroup : Subgroup G) (isPGroup' : IsPGroup.{u_1} p ↥toSubgroup)
  (is_maximal' : ∀ {Q : Subgroup G}, IsPGroup.{u_1} p ↥Q → toSubgroup ≤ Q → Q = toSubgroup)
  (h :
    (↑{ toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := @is_maximal' : Sylow p G } : Subgroup G) =
      (↑Q : Subgroup G)),
  { toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := @is_maximal' : Sylow p G } = Q
Tactic: cases P
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
Q : Sylow p G
toSubgroup : Subgroup G
isPGroup' : IsPGroup.{u_1} p ↥toSubgroup
is_maximal' : ∀ {Q : Subgroup G}, IsPGroup.{u_1} p ↥Q → toSubgroup ≤ Q → Q = toSubgroup
h :
  (↑{ toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := @is_maximal' : Sylow p G } : Subgroup G) =
    (↑Q : Subgroup G)
⊢ { toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := @is_maximal' : Sylow p G } = Q
have mk : ∀ (toSubgroup_1 : Subgroup G) (isPGroup'_1 : IsPGroup.{u_1} p ↥toSubgroup_1)
  (is_maximal'_1 : ∀ {Q : Subgroup G}, IsPGroup.{u_1} p ↥Q → toSubgroup_1 ≤ Q → Q = toSubgroup_1)
  (h :
    (↑{ toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := @is_maximal' : Sylow p G } : Subgroup G) =
      (↑{ toSubgroup := toSubgroup_1, isPGroup' := isPGroup'_1, is_maximal' := @is_maximal'_1 : Sylow p G } :
        Subgroup G)),
  { toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := @is_maximal' : Sylow p G } =
    { toSubgroup := toSubgroup_1, isPGroup' := isPGroup'_1, is_maximal' := @is_maximal'_1 }
Tactic: cases Q
Cleared hypotheses: Q, h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup.{u_1} p ↥P
hP2 : ¬p ∣ P.index
Q : Subgroup G
hQ : IsPGroup.{u_1} p ↥Q
hPQ : P ≤ Q
⊢ Q = P
have this : P.FiniteIndex
Tactic: have : P.FiniteIndex := ⟨fun h ↦ hP2 (h ▸ (dvd_zero p))⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup.{u_1} p ↥P
hP2 : ¬p ∣ P.index
Q : Subgroup G
hQ : IsPGroup.{u_1} p ↥Q
hPQ : P ≤ Q
this : P.FiniteIndex
⊢ Q = P
have obtain : ∀ (k : ℕ) (hk : Nat.card.{u_1} (↥Q ⧸ P.normalCore.subgroupOf Q) = p ^ k), Q = P
Tactic: obtain ⟨k, hk⟩ := (hQ.to_quotient (P.normalCore.subgroupOf Q)).exists_card_eq
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup.{u_1} p ↥P
hP2 : ¬p ∣ P.index
Q : Subgroup G
hQ : IsPGroup.{u_1} p ↥Q
hPQ : P ≤ Q
this : P.FiniteIndex
k : ℕ
hk : Nat.card.{u_1} (↥Q ⧸ P.normalCore.subgroupOf Q) = p ^ k
⊢ Q = P
have h : P.index.Coprime (Nat.card.{u_1} (↥Q ⧸ P.normalCore.subgroupOf Q))
Tactic: have h := hk ▸ Nat.Prime.coprime_pow_of_not_dvd (m := k) Fact.out hP2
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p_1 : ℕ
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card.{u_1} ↥H = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ¬p ∣ H.index
have rw : ¬p ^ HAdd.hAdd (α := ℕ) (β := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣ Nat.card G
Tactic: rw [← mul_dvd_mul_iff_left (Nat.card_pos (α := H)).ne', card_mul_index, card_eq, ← pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
K : Type u_2
inst_1 : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
h : (↑P : Subgroup G) ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup.{u_2} p ↥Q
hle : comap ϕ (↑P : Subgroup G) ≤ Q
⊢ Q = comap ϕ (↑P : Subgroup G)
have rw : Q = comap ϕ (map ϕ Q)
Tactic: rw [← P.3 (hQ.map ϕ) (le_trans (ge_of_eq (map_comap_eq_self h)) (map_mono hle))]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
N : Subgroup G
P Q : Sylow p G
hP : (↑P : Subgroup G) ≤ N
hQ : (↑Q : Subgroup G) ≤ N
h : P.subtype hP = Q.subtype hQ
⊢ P = Q
have rw : ∀ (h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ) (x : G), x ∈ P ↔ x ∈ Q
Tactic: rw [SetLike.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q : Subgroup G | IsPGroup.{u_1} p ↥Q}
hc2 : IsChain (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x : ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : (↑c : Type u_1)
hg : Membership.mem (γ := Set G) ((fun (R : (↑c : Type u_1)) ↦ (↑(↑R : Subgroup G) : Set G)) S) g
⊢ ∃ (k : ℕ),
    HPow.hPow (α :=
        ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
            inv_mem' := ⋯ : Subgroup G })
        (Subtype.mk (p := fun (x : G) ↦
          Membership.mem (γ := Subgroup G)
            { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
              inv_mem' := ⋯ : Subgroup G }
            x)
          g ⋯)
        (p ^ k) =
      1
have refine : ∀ (k : ℕ) (hk : Subtype.mk (p := fun (x : G) ↦ x ∈ (↑S : Subgroup G)) g hg ^ p ^ k = 1),
  HPow.hPow (α :=
      ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := sorry, one_mem' := sorry, inv_mem' := sorry :
          Subgroup G })
      (Subtype.mk (p := fun (x : G) ↦
        Membership.mem (γ := Subgroup G)
          { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := sorry, one_mem' := sorry,
            inv_mem' := sorry : Subgroup G }
          x)
        g sorry)
      (p ^ k) =
    1
Tactic: refine Exists.imp (fun k hk => ?_) (hc1 S.2 ⟨g, hg⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q : Subgroup G | IsPGroup.{u_1} p ↥Q}
hc2 : IsChain (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x : ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : (↑c : Type u_1)
hg : Membership.mem (γ := Set G) ((fun (R : (↑c : Type u_1)) ↦ (↑(↑R : Subgroup G) : Set G)) S) g
k : ℕ
hk : Subtype.mk (p := fun (x : G) ↦ x ∈ (↑S : Subgroup G)) g hg ^ p ^ k = 1
⊢ HPow.hPow (α :=
      ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ :
          Subgroup G })
      (Subtype.mk (p := fun (x : G) ↦
        Membership.mem (γ := Subgroup G)
          { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
            inv_mem' := ⋯ : Subgroup G }
          x)
        g ⋯)
      (p ^ k) =
    1
have rwa : ∀ (hk : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ (↑S : Subgroup G)) g hg ^ p ^ k) : G) = (↑1 : G)),
  (↑(HPow.hPow (α :=
          ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := sorry, one_mem' := sorry,
              inv_mem' := sorry : Subgroup G })
          (Subtype.mk (p := fun (x : G) ↦
            Membership.mem (γ := Subgroup G)
              { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := sorry, one_mem' := sorry,
                inv_mem' := sorry : Subgroup G }
              x)
            g sorry)
          (p ^ k)) :
      G) =
    (↑1 : G)
Tactic: rwa [Subtype.ext_iff, coe_pow] at hk ⊢
Cleared hypotheses: hk