awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
⊢ S.units.ofUnits ≤ S

Tactic:
fun _ ⟨_, hm, he⟩ => he ▸ hm.1

Premises used: _private.0.Submonoid.ofUnits_units_le.match_1, Membership.mem, Eq.rec, And.left
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Monotone.{u_1, u_1} (α := Subgroup Mˣ) ofUnits

Tactic:
fun _ _ hST _ ⟨x, hx, hy⟩ => ⟨x, hST hx, hy⟩

Premises used: Monotone, Membership.mem, And.intro, Exists.intro, Subgroup.ofUnits, _private.0.Subgroup.ofUnits_mono.match_1
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
⊢ S.ofUnits.units = S

Tactic:
Subgroup.ext (fun _ =>
  ⟨fun ⟨⟨_, hm, he⟩, _⟩ => (Units.ext he) ▸ hm, fun hm => ⟨⟨_, hm, rfl⟩, _, S.inv_mem hm, rfl⟩⟩)

Premises used: Membership.mem, Eq.rec, Units.ext, Inv.inv, Subgroup.inv_mem, And.intro, Iff.intro, Exists.intro, rfl, Subgroup.ext, _private.0.Subgroup.units_ofUnits_eq.match_1
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ GaloisConnection.{u_1, u_1} (α := Subgroup Mˣ) Subgroup.ofUnits Submonoid.units

Tactic:
ofUnits_units_gci.gc

Premises used: ofUnits_units_gci, GaloisCoinsertion.gc
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
H : Subgroup Mˣ
⊢ H.ofUnits ≤ S ↔ H ≤ S.units

Tactic:
ofUnits_units_gc _ _

Premises used: ofUnits_units_gc
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Type u_2
inst_1 : SetLike S M
inst_2 : SubmonoidClass S M
N : S
a : ↥N
ha : IsUnit a
⊢ IsUnit (↑a : M)

Tactic:
ha.map (SubmonoidClass.subtype N)

Premises used: SubmonoidClass.subtype, IsUnit.map
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
⊢ x ∈ S.units ↔ (↑x : M) ∈ S ∧ (↑x⁻¹ : M) ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.preimage
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
h₁ : (↑x : M) ∈ S
h₂ : (↑x⁻¹ : M) ∈ S
⊢ x ∈ S.units

Tactic:
⟨h₁, h₂⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
h : x ∈ S.units
⊢ (↑x : M) ∈ S

Tactic:
h.1

Premises used: Set.Mem, setOf, Set.preimage, And.left
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
h : x ∈ S.units
⊢ (↑x⁻¹ : M) ∈ S

Tactic:
h.2

Premises used: Set.Mem, setOf, And.right, Set.preimage
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : (↥S)ˣ
⊢ (↑(↑x⁻¹ : ↥S) : M) * (↑(↑x : ↥S) : M) = 1

Tactic:
DFunLike.congr_arg S.subtype x.inv_mul

Premises used: Units.inv_mul, Submonoid.subtype, DFunLike.congr_arg
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : (↥S)ˣ
⊢ (↑(↑x : ↥S) : M) * (↑(↑x⁻¹ : ↥S) : M) = 1

Tactic:
DFunLike.congr_arg S.subtype x.mul_inv

Premises used: Units.mul_inv, Submonoid.subtype, DFunLike.congr_arg
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
h : x ∈ S.units
⊢ HMul.hMul (α := ↥S) (β := ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) ((coeHom M : (a : Mˣ) → M) x⁻¹) ⋯ : ↥S)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ S) ((coeHom M : (a : Mˣ) → M) x) ⋯ : ↥S) =
    1

Tactic:
Subtype.ext x.inv_mul

Premises used: Units.inv_mul, Subtype.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
h : x ∈ S.units
⊢ HMul.hMul (α := ↥S) (β := ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) ((coeHom M : (a : Mˣ) → M) x) ⋯ : ↥S)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ S) ((coeHom M : (a : Mˣ) → M) x⁻¹) ⋯ : ↥S) =
    1

Tactic:
Subtype.ext x.mul_inv

Premises used: Units.mul_inv, Subtype.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x y : Mˣ
h₁ : x ∈ S.units
h₂ : y ∈ S.units
⊢ x * y ∈ S.units

Tactic:
mul_mem h₁ h₂

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
h : x ∈ S.units
⊢ x⁻¹ ∈ S.units

Tactic:
inv_mem h

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x : Mˣ
⊢ x⁻¹ ∈ S.units ↔ x ∈ S.units

Tactic:
inv_mem_iff

Premises used: Set.Mem, inv_mem_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq.{u_1 + 1} (α := Subgroup Mˣ) (units ⊤) ⊤

Tactic:
ofUnits_units_gc.u_top

Premises used: ofUnits_units_gc, GaloisConnection.u_top
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S T : Submonoid M
⊢ (S ⊓ T).units = S.units ⊓ T.units

Tactic:
ofUnits_units_gc.u_inf

Premises used: ofUnits_units_gc, GaloisConnection.u_inf
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
s : Set (Submonoid M)
⊢ (sInf s).units = ⨅ S ∈ s, S.units

Tactic:
ofUnits_units_gc.u_sInf

Premises used: ofUnits_units_gc, GaloisConnection.u_sInf
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
ι : Sort u_2
f : ι → Submonoid M
⊢ (iInf f).units = ⨅ (i : ι), (f i).units

Tactic:
ofUnits_units_gc.u_iInf

Premises used: GaloisConnection.u_iInf, ofUnits_units_gc
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
ι : Sort u_2
κ : ι → Sort u_3
f : (i : ι) → κ i → Submonoid M
⊢ Eq.{u_1 + 1} (α := Subgroup Mˣ) (units (⨅ (i : ι), ⨅ (j : κ i), f i j)) (⨅ (i : ι), ⨅ (j : κ i), (f i j).units)

Tactic:
ofUnits_units_gc.u_iInf₂

Premises used: ofUnits_units_gc, GaloisConnection.u_iInf₂
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq.{u_1 + 1} (α := Subgroup Mˣ) (units ⊥) ⊥

Tactic:
ofUnits_units_gci.u_bot

Premises used: ofUnits_units_gci, GaloisCoinsertion.u_bot
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := Submonoid M) units

Tactic:
ofUnits_units_gci.u_surjective

Premises used: ofUnits_units_gci, GaloisCoinsertion.u_surjective
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Function.LeftInverse.{u_1 + 1, u_1 + 1} (α := Subgroup Mˣ) units Subgroup.ofUnits

Tactic:
ofUnits_units_gci.leftInverse_u_l

Premises used: ofUnits_units_gci, GaloisCoinsertion.leftInverse_u_l
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Submonoid M
⊢ Subsingleton.{u_1 + 1} (↥S)ˣ

Tactic:
.units_of_isUnit fun _a ha ↦ Subtype.ext (ha.map S.subtype).eq_one

Premises used: Subsingleton.units_of_isUnit, Submonoid.subtype, IsUnit.map, IsUnit.eq_one, Subtype.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
⊢ x ∈ S.ofUnits ↔ ∃ y ∈ S, (↑y : M) = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
y : Mˣ
h₁ : y ∈ S
h₂ : (↑y : M) = x
⊢ x ∈ S.ofUnits

Tactic:
⟨_, h₁, h₂⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
h : x ∈ S.ofUnits
⊢ ∃ y ∈ S, (↑y : M) = x

Tactic:
h

Premises used: Set.Mem, setOf, Set.image
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
y : Mˣ
hy : (↑y : M) ∈ S.ofUnits
⊢ y ∈ S

Tactic:
match hy with
  | ⟨_, hm, he⟩ => (Units.ext he) ▸ hm

Premises used: Membership.mem, Eq.rec, _private.0.Subgroup.mem_of_mem_val_ofUnits.match_1, Units.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
hx : x ∈ S.ofUnits
⊢ IsUnit x

Tactic:
match hx with
  | ⟨_, _, h⟩ => ⟨_, h⟩

Premises used: IsUnit, _private.0.Subgroup.isUnit_of_mem_ofUnits.match_1, Exists.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : Mˣ
h : (↑x : M) ∈ S.ofUnits
⊢ S.unit_of_mem_ofUnits h = x

Tactic:
Units.ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
h : x ∈ S.ofUnits
⊢ (↑(S.unit_of_mem_ofUnits h) : M) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
h : x ∈ S.ofUnits
⊢ S.unit_of_mem_ofUnits h ∈ S

Tactic:
S.mem_of_mem_val_ofUnits h

Premises used: Subgroup.mem_of_mem_val_ofUnits
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
h₁ : IsUnit x
h₂ : x ∈ S.ofUnits
⊢ h₁.unit = S.unit_of_mem_ofUnits h₂

Tactic:
Units.ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
h₁ : IsUnit x
h₂ : x ∈ S.ofUnits
⊢ h₁.unit ∈ S

Tactic:
S.unit_eq_unit_of_mem_ofUnits h₁ h₂ ▸ (S.unit_of_mem_ofUnits_spec_mem)

Premises used: Eq.rec, Subgroup.unit_eq_unit_of_mem_ofUnits, Subgroup.unit_of_mem_ofUnits_spec_mem, Eq.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
h₁ : IsUnit x
h₂ : h₁.unit ∈ S
⊢ x ∈ S.ofUnits

Tactic:
S.mem_ofUnits h₂ h₁.unit_spec

Premises used: Subgroup.mem_ofUnits, IsUnit.unit_spec
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S : Subgroup Mˣ
x : M
⊢ x ∈ S.ofUnits ↔ ∃ (h : IsUnit x), h.unit ∈ S

Tactic:
⟨fun h => ⟨S.isUnit_of_mem_ofUnits h, S.unit_mem_of_mem_ofUnits h⟩,
  fun ⟨hm, he⟩ => S.mem_ofUnits_of_isUnit_of_unit_mem hm he⟩

Premises used: _private.0.Subgroup.mem_ofUnits_iff_exists_isUnit.match_1, Membership.mem, Subgroup.mem_ofUnits_of_isUnit_of_unit_mem, Subgroup.unit_mem_of_mem_ofUnits, Iff.intro, Exists.intro, Subgroup.ofUnits, Subgroup.isUnit_of_mem_ofUnits
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq.{u_1 + 1} (α := Submonoid M) (ofUnits ⊥) ⊥

Tactic:
ofUnits_units_gc.l_bot

Premises used: ofUnits_units_gc, GaloisConnection.l_bot
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S T : Subgroup Mˣ
⊢ (S ⊔ T).ofUnits = S.ofUnits ⊔ T.ofUnits

Tactic:
ofUnits_units_gc.l_sup

Premises used: ofUnits_units_gc, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
s : Set (Subgroup Mˣ)
⊢ (sSup s).ofUnits = ⨆ S ∈ s, S.ofUnits

Tactic:
ofUnits_units_gc.l_sSup

Premises used: GaloisConnection.l_sSup, ofUnits_units_gc
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
ι : Sort u_2
f : ι → Subgroup Mˣ
⊢ (iSup f).ofUnits = ⨆ (i : ι), (f i).ofUnits

Tactic:
ofUnits_units_gc.l_iSup

Premises used: ofUnits_units_gc, GaloisConnection.l_iSup
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
ι : Sort u_2
κ : ι → Sort u_3
f : (i : ι) → κ i → Subgroup Mˣ
⊢ Eq.{u_1 + 1} (α := Submonoid M) (ofUnits (⨆ (i : ι), ⨆ (j : κ i), f i j)) (⨆ (i : ι), ⨆ (j : κ i), (f i j).ofUnits)

Tactic:
ofUnits_units_gc.l_iSup₂

Premises used: GaloisConnection.l_iSup₂, ofUnits_units_gc
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Subgroup Mˣ) ofUnits

Tactic:
ofUnits_units_gci.l_injective

Premises used: GaloisCoinsertion.l_injective, ofUnits_units_gci
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S T : Subgroup Mˣ
⊢ (S.ofUnits ⊔ T.ofUnits).units = S ⊔ T

Tactic:
ofUnits_units_gci.u_sup_l _ _

Premises used: ofUnits_units_gci, GaloisCoinsertion.u_sup_l
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S T : Subgroup Mˣ
⊢ (S.ofUnits ⊓ T.ofUnits).units = S ⊓ T

Tactic:
ofUnits_units_gci.u_inf_l _ _

Premises used: ofUnits_units_gci, GaloisCoinsertion.u_inf_l
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Function.RightInverse.{u_1 + 1, u_1 + 1} (α := Submonoid M) ofUnits Submonoid.units

Tactic:
ofUnits_units_gci.leftInverse_u_l

Premises used: ofUnits_units_gci, Function.RightInverse, GaloisCoinsertion.leftInverse_u_l
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ StrictMono.{u_1, u_1} (α := Subgroup Mˣ) ofUnits

Tactic:
ofUnits_units_gci.strictMono_l

Premises used: ofUnits_units_gci, GaloisCoinsertion.strictMono_l
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
S T : Subgroup Mˣ
⊢ S.ofUnits ≤ T.ofUnits ↔ S ≤ T

Tactic:
ofUnits_units_gci.l_le_l_iff

Premises used: GaloisCoinsertion.l_le_l_iff, ofUnits_units_gci
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : Gˣ
simp_rw : (↑x : G) ∈ H.toSubmonoid ∧ (↑x⁻¹ : G) ∈ H.toSubmonoid ↔ (↑x : G) ∈ H
simp_rw₁ : (↑x : G) ∈ H ∧ (↑x⁻¹ : G) ∈ H ↔ (↑x : G) ∈ H
simp_rw₂ : (↑x : G) ∈ H ∧ (↑x : G)⁻¹ ∈ H ↔ (↑x : G) ∈ H
simp_rw₃ : (↑x : G) ∈ H ∧ (↑x : G) ∈ H ↔ (↑x : G) ∈ H
⊢ x ∈ H.units ↔ (↑x : G) ∈ H

Tactic:
simp_rw [Submonoid.mem_units_iff, mem_toSubmonoid, val_inv_eq_inv_val, inv_mem_iff, and_self]

Premises used: and_self, Units.val_inv_eq_inv_val, inv_mem_iff, Submonoid.mem_units_iff, Subgroup.mem_toSubmonoid
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gˣ
x : G
simp_rw : (∃ y ∈ H, (↑y : G) = x) ↔ Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
simp_rw₁ :
  (∃ (x_1 : G),
      Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x_1 : Gˣ) ∧ (↑((toUnits : (a : G) → Gˣ) x_1) : G) = x) ↔
    Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
simp_rw₂ :
  (∃ (x_1 : G), Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x_1 : Gˣ) ∧ x_1 = x) ↔
    Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
⊢ x ∈ H.ofUnits ↔ Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)

Tactic:
simp_rw [mem_ofUnits_iff, toUnits.surjective.exists, val_toUnits_apply, exists_eq_right]

Premises used: Function.Surjective.exists, Subgroup.mem_ofUnits_iff, val_toUnits_apply, exists_eq_right, MulEquiv.surjective, toUnits
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : G
simp_rw : (↑((toUnits : (a : G) → Gˣ) x) : G) ∈ H ↔ x ∈ H
⊢ Membership.mem (α := Gˣ) H.units ((toUnits : (a : G) → Gˣ) x : Gˣ) ↔ x ∈ H

Tactic:
simp_rw [mem_units_iff_val_mem, val_toUnits_apply]

Premises used: val_toUnits_apply, Subgroup.mem_units_iff_val_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gˣ
x : Gˣ
simp_rw : Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) (↑x : G) : Gˣ) ↔ x ∈ H
⊢ (↑x : G) ∈ H.ofUnits ↔ x ∈ H

Tactic:
simp_rw [mem_ofUnits_iff_toUnits_mem, toUnits_val_apply]

Premises used: Subgroup.mem_ofUnits_iff_toUnits_mem, toUnits_val_apply
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
s : Set (Subsemigroup M)
a b : M
hx : Membership.mem (γ := Set M) (⋂ t ∈ s, (↑t : Set M)) a
hy : Membership.mem (γ := Set M) (⋂ t ∈ s, (↑t : Set M)) b
i : Subsemigroup M
h : i ∈ s
⊢ a ∈ i

Tactic:
apply Set.mem_iInter₂.1 hx i h

Premises used: Set.mem_iInter₂, Iff.mp
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
s : Set (Subsemigroup M)
a b : M
hx : Membership.mem (γ := Set M) (⋂ t ∈ s, (↑t : Set M)) a
hy : Membership.mem (γ := Set M) (⋂ t ∈ s, (↑t : Set M)) b
i : Subsemigroup M
h : i ∈ s
⊢ b ∈ i

Tactic:
apply Set.mem_iInter₂.1 hy i h

Premises used: Set.mem_iInter₂, Iff.mp
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
S : Set (Subsemigroup M)
⊢ (↑(sInf S) : Set M) = ⋂ s ∈ S, (↑s : Set M)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
S : Set (Subsemigroup M)
x : M
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
x : M
⊢ Membership.mem (γ := Subsemigroup M) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, Subsemigroup.mem_sInf
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
⊢ (↑(⨅ (i : ι), S i) : Set M) = ⋂ (i : ι), (↑(S i) : Set M)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Premises used: iInf, Subsemigroup.coe_sInf, Set.biInter_range
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
x : M
⊢ Membership.mem (γ := Subsemigroup M) (closure s) x ↔ ∀ (S : Subsemigroup M), s ⊆ (↑S : Set M) → x ∈ S

Tactic:
mem_sInf

Premises used: Set.Mem, setOf, Subsemigroup.mem_sInf
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
⊢ s ⊆ (↑(closure s) : Set M)

Tactic:
fun _ hx => mem_closure.2 fun _ hS => hS hx

Premises used: Iff.mpr, Set.Subset, Subsemigroup.mem_closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
x : M
hx : x ∈ s
⊢ Membership.mem (γ := Subsemigroup M) (closure s) x

Tactic:
subset_closure hx

Premises used: Subsemigroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
P : M
hP : P ∉ closure s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: Subsemigroup.subset_closure, Not
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
S : Subsemigroup M
⊢ closure s ≤ S ↔ s ⊆ (↑S : Set M)

Tactic:
⟨Subset.trans subset_closure, fun h => sInf_le h⟩

Premises used: Set.Subset.trans, Subsemigroup.subset_closure, sInf_le, Iff.intro
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s t : Set M
h : s ⊆ t
⊢ LE.le (α := Subsemigroup M) (closure s) (closure t)

Tactic:
closure_le.2 <| Subset.trans h subset_closure

Premises used: Iff.mpr, Set.Subset.trans, Subsemigroup.closure_le, Subsemigroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
S : Subsemigroup M
h₁ : s ⊆ (↑S : Set M)
h₂ : S ≤ closure s
⊢ closure s = S

Tactic:
le_antisymm (closure_le.2 h₁) h₂

Premises used: Iff.mpr, Subsemigroup.closure_le, le_antisymm
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
p : (x : M) → Membership.mem (γ := Subsemigroup M) (closure s) x → Prop
mem : ∀ (x : M) (h : x ∈ s), p x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : M
hx : Membership.mem (γ := Subsemigroup M) (closure s) x
⊢ p x hx

Tactic:
let S : Subsemigroup M :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩ }
  closure_le (S := S) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, HMul.hMul, Subsemigroup.mk, setOf, Membership.mem, Exists, id, Subsemigroup.closure_le, _private.0.Subsemigroup.closure_induction.match_1, Subsemigroup.subset_closure, Exists.intro, Exists.elim, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x_1 : M
h : x_1 ∈ s
⊢ p z x_1 ⋯ ⋯

Tactic:
mem _ _ hz h
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x_1 : M
h : x_1 ∈ s
⊢ p z x_1 ⋯ ⋯

Tactic:
exact mem _ _ hz h
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x_1 y_1 : M
hx : Membership.mem (γ := Subsemigroup M) (closure s) x_1
hy : Membership.mem (γ := Subsemigroup M) (closure s) y_1
h₁ : p z x_1 ⋯ hx
h₂ : p z y_1 ⋯ hy
⊢ p z (x_1 * y_1) ⋯ ⋯

Tactic:
mul_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x_1 y_1 : M
hx : Membership.mem (γ := Subsemigroup M) (closure s) x_1
hy : Membership.mem (γ := Subsemigroup M) (closure s) y_1
h₁ : p z x_1 ⋯ hx
h₂ : p z y_1 ⋯ hy
⊢ p z (x_1 * y_1) ⋯ ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂