awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Monoid M
x : ↥(IsUnit.submonoid M)
⊢ (↑x⁻¹ : M) = (↑(IsUnit.unit ⋯)⁻¹ : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
a _b : M
h : Membership.mem (γ := Set M) {x : M | ∃ (y : ↥S), x * (↑y : M) = 1} a
h_1 : Membership.mem (γ := Set M) {x : M | ∃ (y : ↥S), x * (↑y : M) = 1} _b
a' : ↥S
ha : a * (↑a' : M) = 1
b' : ↥S
hb : _b * (↑b' : M) = 1
⊢ a * _b * (↑(b' * a') : M) = 1

Tactic:
simp only [coe_mul, ← mul_assoc, mul_assoc a, hb, mul_one, ha]

Premises used: mul_assoc, mul_one, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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
⊢ (↑z : M) ∈ S

Tactic:
z.prop

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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 = (↑z : M)
⊢ x ∈ S

Tactic:
convert! z.prop

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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)
h₆ h₇ : (↑z : M) = (↑z : M)
⊢ x = (↑z : M)

Tactic:
rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]

Premises used: mul_assoc, mul_one, one_mul
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
hx : (↑x : M) ∈ S
⊢ (↑x⁻¹ : M) ∈ S.leftInv

Tactic:
⟨⟨x, hx⟩, x.inv_val⟩

Premises used: Units.val, Set.Mem, Units.inv_val, setOf, Subtype.mk, Exists.intro
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S.leftInv.leftInv = S

Tactic:
le_antisymm S.leftInv_leftInv_le ?_

Premises used: Submonoid.leftInv_leftInv_le, le_antisymm
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
refine : S ≤ S.leftInv.leftInv
⊢ S.leftInv.leftInv = S

Tactic:
refine le_antisymm S.leftInv_leftInv_le ?_

Premises used: Submonoid.leftInv_leftInv_le, le_antisymm
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
rw : x = (↑(IsUnit.unit ⋯) : M)
⊢ x = (↑(IsUnit.unit ⋯)⁻¹⁻¹ : M)

Tactic:
rw [inv_inv (hS hx).unit]

Premises used: inv_inv, IsUnit.unit
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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)

Tactic:
have : x = ((hS hx).unit⁻¹⁻¹ : Mˣ) := by
    rw [inv_inv (hS hx).unit]
    rfl
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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)
rw : (↑(IsUnit.unit ⋯)⁻¹⁻¹ : M) ∈ S.leftInv.leftInv
⊢ x ∈ S.leftInv.leftInv

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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)
⊢ (↑(IsUnit.unit ⋯)⁻¹⁻¹ : M) ∈ S.leftInv.leftInv

Tactic:
S.leftInv.unit_mem_leftInv _ (S.unit_mem_leftInv _ hx)

Premises used: Submonoid.leftInv, Submonoid.unit_mem_leftInv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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)
⊢ (↑(IsUnit.unit ⋯)⁻¹⁻¹ : M) ∈ S.leftInv.leftInv

Tactic:
exact S.leftInv.unit_mem_leftInv _ (S.unit_mem_leftInv _ hx)

Premises used: Submonoid.leftInv, Submonoid.unit_mem_leftInv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : ↥S.leftInv
⊢ (↑x : M) * (↑(S.fromLeftInv x) : M) = 1

Tactic:
x.prop.choose_spec

Premises used: Exists.choose_spec, Subtype.prop
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
⊢ S.fromLeftInv 1 = 1

Tactic:
(one_mul _).symm.trans (Subtype.ext <| S.mul_fromLeftInv 1)

Premises used: OfNat.ofNat, Eq.symm, one_mul, Eq.trans, Subtype.ext, Submonoid.mul_fromLeftInv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : ↥S.leftInv
rw : (↑x : M) * (↑(S.fromLeftInv x) : M) = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := M) 1 1
⊢ (↑(S.fromLeftInv x) : M) * (↑x : M) = 1

Tactic:
rw [mul_comm, mul_fromLeftInv]

Premises used: mul_comm, Submonoid.mul_fromLeftInv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
⊢ S.leftInv ≤ IsUnit.submonoid M

Tactic:
fun x ⟨y, hx⟩ ↦
  ⟨⟨x, y, hx, mul_comm x y ▸ hx⟩, rfl⟩

Premises used: _private.0.Submonoid.leftInv_le_isUnit.match_1, Membership.mem, IsUnit.submonoid, Eq.rec, Units.mk, Exists.intro, mul_comm, Subtype.val, rfl
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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
rw₂ rw₃ : (↑a : M) * b = 1 ↔ (↑a : M) * b = 1
⊢ (↑(S.fromLeftInv a) : M) = b ↔ (↑a : M) * b = 1

Tactic:
rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]

Premises used: eq_comm, IsUnit.mul_right_inj, Subtype.prop, Submonoid.leftInv_le_isUnit, Submonoid.mul_fromLeftInv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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
rw₈ rw₉ : Eq.{u_1 + 1} (α := M) 1 1
⊢ (↑(S.fromLeftInv (x * y)) : M) = (↑(S.fromLeftInv x * S.fromLeftInv y) : M)

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]

Premises used: mul_assoc, Submonoid.fromLeftInv_eq_iff, mul_comm, Subtype.val, one_mul, Submonoid.coe_mul, Submonoid.mul_fromLeftInv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ (↑(IsUnit.unit ⋯)⁻¹ : M) * (↑x : M) = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
a :
  (↑((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)) :
      M) =
    (↑x : M)
⊢ (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

Tactic:
ext
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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)) :
      M) =
    (↑x : M)

Tactic:
simp [← Units.mul_eq_one_iff_inv_eq]

Premises used: Units.mul_eq_one_iff_inv_eq
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
a :
  (↑((↑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))) :
      M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) : M)
⊢ (↑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

Tactic:
ext
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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))) :
      M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) : M)

Tactic:
simp [fromLeftInv_eq_iff]

Premises used: Submonoid.fromLeftInv_eq_iff
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ S.fromLeftInv (((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x) = x

Tactic:
(S.leftInvEquiv hS).right_inv x

Premises used: Submonoid.fromLeftInv, Equiv.right_inv, MulEquiv.toEquiv, Classical.choose, Submonoid.leftInvEquiv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
⊢ ((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) (S.fromLeftInv x) = x

Tactic:
(S.leftInvEquiv hS).left_inv x

Premises used: MulEquiv.toEquiv, Submonoid.leftInvEquiv, Equiv.left_inv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
⊢ (↑((S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) x) : M) * (↑x : M) = 1

Tactic:
simpa only [leftInvEquiv_apply, fromCommLeftInv] using fromLeftInv_mul S x

Premises used: Submonoid.leftInvEquiv_apply, Submonoid.fromCommLeftInv, Submonoid.fromLeftInv_mul
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
⊢ (↑x : M) * (↑((S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) x) : M) = 1

Tactic:
simp only [leftInvEquiv_apply, fromCommLeftInv, mul_fromLeftInv]

Premises used: Submonoid.leftInvEquiv_apply, Submonoid.fromCommLeftInv, Submonoid.mul_fromLeftInv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ HMul.hMul (α := M) (↑(((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x) : M)
      (↑((S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) (((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x)) : M) =
    1

Tactic:
S.mul_leftInvEquiv hS ((S.leftInvEquiv hS).symm x)

Premises used: Submonoid.mul_leftInvEquiv, Submonoid.leftInvEquiv, MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
h : x = (S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) (((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x)
⊢ (↑(((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x) : M) * (↑x : M) = 1

Tactic:
convert! S.mul_leftInvEquiv hS ((S.leftInvEquiv hS).symm x)

Premises used: Submonoid.mul_leftInvEquiv, Submonoid.leftInvEquiv, MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ x = (S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) (((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ HMul.hMul (α := M)
      (↑((S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) (((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x)) : M)
      (↑(((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x) : M) =
    1

Tactic:
S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)

Premises used: Submonoid.leftInvEquiv_mul, Submonoid.leftInvEquiv, MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
h : x = (S.leftInvEquiv hS : (a : ↥S.leftInv) → ↥S) (((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x)
⊢ (↑x : M) * (↑(((S.leftInvEquiv hS).symm : (a : ↥S) → ↥S.leftInv) x) : M) = 1

Tactic:
convert! S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)

Premises used: Submonoid.leftInvEquiv_mul, Submonoid.leftInvEquiv, MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : Group M
S : Submonoid M
⊢ S.leftInv = S⁻¹

Tactic:
Submonoid.ext fun _ ↦
    ⟨fun h ↦ Submonoid.mem_inv.mpr ((inv_eq_of_mul_eq_one_right h.choose_spec).symm ▸
      h.choose.prop),
      fun h ↦ ⟨⟨_, h⟩, mul_inv_cancel _⟩⟩

Premises used: Iff.mpr, Exists.choose_spec, Submonoid.mem_inv, Eq.rec, Submonoid.ext, Subtype.mk, Inv.inv, Subtype.prop, Iff.intro, Exists.intro, inv_eq_of_mul_eq_one_right, mul_inv_cancel, Exists.choose, Eq.symm
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := M) 1 1
⊢ (↑(S.fromLeftInv x) : M) = (↑x : M)⁻¹

Tactic:
rw [← mul_right_inj (x : M), mul_inv_cancel, mul_fromLeftInv]

Premises used: mul_right_inj, mul_inv_cancel, Subtype.val, Submonoid.mul_fromLeftInv
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := M) 1 1
⊢ (↑(((MulEquiv.symm (leftInvEquiv.{u_1} (M := M) S hS) : ↥S ≃* ↥S.leftInv) : (a : ↥S) → ↥S.leftInv) x) : M) =
    (↑x : M)⁻¹

Tactic:
rw [← mul_right_inj (x : M), mul_inv_cancel, mul_leftInvEquiv_symm]

Premises used: mul_right_inj, mul_inv_cancel, Subtype.val, Submonoid.mul_leftInvEquiv_symm
-- Module: Mathlib.GroupTheory.Subsemigroup.Center
Goal:
M : Type u_1
inst : Semigroup M
z : M
rw : Membership.mem (γ := Subsemigroup M) (center M) z ↔ z ∈ Set.center M
⊢ Membership.mem (γ := Subsemigroup M) (center M) z ↔ ∀ (g : M), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Premises used: Semigroup.mem_center_iff
-- Module: Mathlib.GroupTheory.Subsemigroup.Center
Goal:
M : Type u_1
inst : Semigroup M
z : M
⊢ Membership.mem (γ := Subsemigroup M) (center M) z ↔ z ∈ Set.center M

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.center
-- Module: Mathlib.GroupTheory.Subsemigroup.Center
Goal:
M : Type u_1
inst : Semigroup M
z : M
⊢ Membership.mem (γ := Subsemigroup M) (center M) z ↔ z ∈ Set.center M

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Subsemigroup.Center
Goal:
M : Type u_1
inst : CommSemigroup M
⊢ Eq (α := Subsemigroup M) (center M) ⊤

Tactic:
SetLike.coe_injective (Set.center_eq_univ M)

Premises used: Set.center_eq_univ, SetLike.coe_injective
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
⊢ (↑(centralizer S) : Set M) = S.centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, rfl
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
z : M
⊢ Membership.mem (γ := Subsemigroup M) (centralizer S) z ↔ ∀ g ∈ S, g * z = z * g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.centralizer
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
inst : Semigroup M
S : Set M
⊢ LE.le (α := Subsemigroup M) (center M) (centralizer S)

Tactic:
S.center_subset_centralizer

Premises used: Set.Mem, setOf, Set.center, Set.centralizer, Set.Subset, Set.center_subset_centralizer
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
S T : Set M
inst : Semigroup M
h : S ⊆ T
⊢ LE.le (α := Subsemigroup M) (centralizer T) (centralizer S)

Tactic:
Set.centralizer_subset h

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
⊢ Eq (α := Subsemigroup M) (centralizer s) ⊤ ↔ s ⊆ (↑(center M) : Set M)

Tactic:
SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

Premises used: Set.centralizer_eq_top_iff_subset, SetLike.ext'_iff, Iff.trans
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
inst : Semigroup M
⊢ Eq (α := Subsemigroup M) (centralizer Set.univ) (center M)

Tactic:
SetLike.ext' (Set.centralizer_univ M)

Premises used: SetLike.ext', Set.centralizer_univ
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
⊢ LE.le (α := Subsemigroup M) (closure s) (centralizer (↑(centralizer s) : Set M))

Tactic:
closure_le.mpr Set.subset_centralizer_centralizer

Premises used: Iff.mpr, Subsemigroup.closure_le, Set.subset_centralizer_centralizer
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a
⊢ IsMulCommutative.{u_1} ↥(closure s)

Tactic:
have := closure_le_centralizer_centralizer s
  .of_setLike_mul_comm fun _ h₁ _ h₂ ↦
    Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂)

Premises used: Subsemigroup.closure_le_centralizer_centralizer, IsMulCommutative.of_setLike_mul_comm, Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.GroupTheory.Subsemigroup.Centralizer
Goal:
M : Type u_1
S_1 T : Set M
inst : Semigroup M
S : Type u_2
inst_1 : SetLike S M
inst_2 : MulMemClass S M
s : S
inst_3 : IsMulCommutative.{u_1} ↥s
⊢ IsMulCommutative.{u_1} ↥(closure (↑s : Set M))

Tactic:
isMulCommutative_closure _ fun _ h₁ _ h₂ => setLike_mul_comm h₁ h₂

Premises used: setLike_mul_comm, Subsemigroup.isMulCommutative_closure
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P Q : Sylow p G
h : (↑P : Subgroup G) = (↑Q : Subgroup G)
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
⊢ P = Q

Tactic:
cases P
-- Module: Mathlib.GroupTheory.Sylow
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)
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 }
⊢ { toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := @is_maximal' : Sylow p G } = Q

Tactic:
cases Q
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
toSubgroup : Subgroup G
isPGroup' : IsPGroup.{u_1} p ↥toSubgroup
is_maximal' : ∀ {Q : Subgroup G}, IsPGroup.{u_1} p ↥Q → toSubgroup ≤ Q → Q = toSubgroup
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:
congr
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
⊢ (↑(↑P : Subgroup G) : Set G) = (↑P : Set G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Sylow
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
⊢ P.FiniteIndex

Tactic:
have : P.FiniteIndex := ⟨fun h ↦ hP2 (h ▸ (dvd_zero p))⟩
-- Module: Mathlib.GroupTheory.Sylow
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
obtain : ∀ (k : ℕ) (hk : Nat.card.{u_1} (↥Q ⧸ P.normalCore.subgroupOf Q) = p ^ k), Q = P
⊢ Q = P

Tactic:
obtain ⟨k, hk⟩ := (hQ.to_quotient (P.normalCore.subgroupOf Q)).exists_card_eq

Premises used: Subgroup.subgroupOf, IsPGroup.to_quotient, IsPGroup.exists_card_eq, Subgroup.normalCore
-- Module: Mathlib.GroupTheory.Sylow
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
⊢ 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
-- Module: Mathlib.GroupTheory.Sylow
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
h : P.index.Coprime (Nat.card.{u_1} (↥Q ⧸ P.normalCore.subgroupOf Q))
⊢ Q = P

Tactic:
le_antisymm (Subgroup.relIndex_eq_one.mp
        (Nat.eq_one_of_dvd_coprimes h (Subgroup.relIndex_dvd_index_of_le hPQ)
        (Subgroup.relIndex_dvd_of_le_left Q P.normalCore_le))) hPQ

Premises used: Subgroup.relIndex_dvd_index_of_le, Nat.eq_one_of_dvd_coprimes, Subgroup.relIndex_dvd_of_le_left, le_antisymm, Subgroup.relIndex_eq_one, Iff.mp, Subgroup.normalCore_le
-- Module: Mathlib.GroupTheory.Sylow
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
h : P.index.Coprime (Nat.card.{u_1} (↥Q ⧸ P.normalCore.subgroupOf Q))
⊢ Q = P

Tactic:
exact le_antisymm (Subgroup.relIndex_eq_one.mp
        (Nat.eq_one_of_dvd_coprimes h (Subgroup.relIndex_dvd_index_of_le hPQ)
        (Subgroup.relIndex_dvd_of_le_left Q P.normalCore_le))) hPQ

Premises used: Subgroup.relIndex_dvd_index_of_le, Nat.eq_one_of_dvd_coprimes, Subgroup.relIndex_dvd_of_le_left, le_antisymm, Subgroup.relIndex_eq_one, Iff.mp, Subgroup.normalCore_le