awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ IsPWO.{u_1} (α := α) (List.prod '' {l : List α | ∀ x ∈ l, x ∈ s})

Tactic:
(h.partiallyWellOrderedOn_sublistForall₂ (· ≤ ·)).image_of_monotone_on ?_

Premises used: Set.IsPWO, Set.PartiallyWellOrderedOn.image_of_monotone_on, LE.le, Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
refine :
  ∀ (a₁ : List α),
    Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s} a₁ →
      ∀ (a₂ : List α),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s} a₂ →
          List.SublistForall₂ (fun (x1 x2 : α) ↦ x1 ≤ x2) a₁ a₂ → a₁.prod ≤ a₂.prod
⊢ IsPWO.{u_1} (α := α) (List.prod '' {l : List α | ∀ x ∈ l, x ∈ s})

Tactic:
refine (h.partiallyWellOrderedOn_sublistForall₂ (· ≤ ·)).image_of_monotone_on ?_

Premises used: Set.PartiallyWellOrderedOn.image_of_monotone_on, LE.le, Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ ∀ (a₁ : List α),
    Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s} a₁ →
      ∀ (a₂ : List α),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s} a₂ →
          List.SublistForall₂ (fun (x1 x2 : α) ↦ x1 ≤ x2) a₁ a₂ → a₁.prod ≤ a₂.prod

Tactic:
fun l1 _ l2 hl2 h12 => h12.prod_le_prod' fun x hx => hpos x <| hl2 x hx

Premises used: List.SublistForall₂.prod_le_prod'
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ ∀ (a₁ : List α),
    Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s} a₁ →
      ∀ (a₂ : List α),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s} a₂ →
          List.SublistForall₂ (fun (x1 x2 : α) ↦ x1 ≤ x2) a₁ a₂ → a₁.prod ≤ a₂.prod

Tactic:
exact fun l1 _ l2 hl2 h12 => h12.prod_le_prod' fun x hx => hpos x <| hl2 x hx
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s : Submonoid M
h : s.MulSaturated
x y : M
⊢ x * y ∈ s ↔ x ∈ s ∧ y ∈ s

Tactic:
⟨@h _ _, and_imp.mpr mul_mem⟩

Premises used: Iff.mpr, and_imp, Iff.intro, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
⊢ MulSaturated.{u_1} (M := M) ⊤

Tactic:
fun _ _ _ ↦ ⟨trivial, trivial⟩

Premises used: trivial, Submonoid.MulSaturated, And.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s₁ s₂ : Submonoid M
h₁ : s₁.MulSaturated
h₂ : s₂.MulSaturated
⊢ (s₁ ⊓ s₂).MulSaturated

Tactic:
fun _ _ hxy ↦ ⟨⟨(h₁ hxy.1).1, (h₂ hxy.2).1⟩, (h₁ hxy.1).2, (h₂ hxy.2).2⟩

Premises used: And.right, And.left, Submonoid.MulSaturated, And.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x x_1 : M
hxy : x * x_1 ∈ InfSet.sInf f
simp_rw : ∀ (hxy : ∀ p ∈ f, x * x_1 ∈ p), (∀ p ∈ f, x ∈ p) ∧ ∀ p ∈ f, x_1 ∈ p
⊢ x ∈ InfSet.sInf f ∧ x_1 ∈ InfSet.sInf f

Tactic:
simp_rw [mem_sInf] at hxy ⊢

Premises used: Submonoid.mem_sInf
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x x_1 : M
hxy : ∀ p ∈ f, x * x_1 ∈ p
⊢ (∀ p ∈ f, x ∈ p) ∧ ∀ p ∈ f, x_1 ∈ p

Tactic:
⟨fun s hs ↦ (hf s hs <| hxy s hs).1, fun s hs ↦ (hf s hs <| hxy s hs).2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x x_1 : M
hxy : ∀ p ∈ f, x * x_1 ∈ p
⊢ (∀ p ∈ f, x ∈ p) ∧ ∀ p ∈ f, x_1 ∈ p

Tactic:
exact ⟨fun s hs ↦ (hf s hs <| hxy s hs).1, fun s hs ↦ (hf s hs <| hxy s hs).2⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_2
f : ι → Submonoid M
hf : ∀ (i : ι), (f i).MulSaturated
⊢ (_root_.iInf f).MulSaturated

Tactic:
sInf <| Set.forall_mem_range.mpr hf

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Submonoid.MulSaturated.sInf
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_2
inst : CommMonoid M
s : Submonoid M
h : ∀ ⦃x y : M⦄, x * y ∈ s → x ∈ s
⊢ s.MulSaturated

Tactic:
fun x y hxy ↦ ⟨h hxy, h <| mul_comm x y ▸ hxy⟩

Premises used: Submonoid.MulSaturated, And.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_2
inst : CommMonoid M
s : Submonoid M
h : ∀ ⦃x y : M⦄, x * y ∈ s → y ∈ s
⊢ s.MulSaturated

Tactic:
of_left fun x y ↦ mul_comm x y ▸ @h y x

Premises used: Eq.rec, Submonoid.MulSaturated.of_left, mul_comm, Eq.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
x x_1 : SaturatedSubmonoid M
s₁ : Submonoid M
h₁ : s₁.MulSaturated
s₂ : Submonoid M
h₂ : s₂.MulSaturated
eq :
  { toSubmonoid := s₁, mulSaturated := h₁ : SaturatedSubmonoid M }.toSubmonoid =
    { toSubmonoid := s₂, mulSaturated := h₂ }.toSubmonoid
⊢ { toSubmonoid := s₁, mulSaturated := h₁ : SaturatedSubmonoid M } = { toSubmonoid := s₂, mulSaturated := h₂ }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s₁ s₂ : SaturatedSubmonoid M
h : s₁.toSubmonoid = s₂.toSubmonoid
⊢ s₁ = s₂

Tactic:
toSubmonoid_injective h

Premises used: SaturatedSubmonoid.toSubmonoid_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s₁ s₂ : SaturatedSubmonoid M
h : ∀ (x : M), x ∈ s₁ ↔ x ∈ s₂
⊢ s₁ = s₂

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s : SaturatedSubmonoid M
x : M
⊢ x ∈ s.toSubmonoid ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
x : M
⊢ Membership.mem (γ := SaturatedSubmonoid M) ⊤ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
a b : M
hx : Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) a
hy : Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) b
rw :
  ∀ (hx : ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), a ∈ (↑i : Set M))
    (hy : ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), b ∈ (↑i : Set M)) (i : SaturatedSubmonoid M) (j : i ∈ f),
    a * b ∈ (↑i : Set M)
⊢ Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) (a * b)

Tactic:
rw [Set.mem_iInter₂] at *

Premises used: Set.mem_iInter₂
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
a b : M
hx : ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), a ∈ (↑i : Set M)
hy : ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), b ∈ (↑i : Set M)
⊢ ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), a * b ∈ (↑i : Set M)

Tactic:
fun s hs ↦ mul_mem (hx s hs) (hy s hs)

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
a b : M
hx : ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), a ∈ (↑i : Set M)
hy : ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), b ∈ (↑i : Set M)
⊢ ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), a * b ∈ (↑i : Set M)

Tactic:
exact fun s hs ↦ mul_mem (hx s hs) (hy s hs)

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ ∀ s ∈ toSubmonoid '' f, s.MulSaturated

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
h : Eq.{u_1 + 1} (α := Set M) (⋂ s ∈ f, (↑s : Set M)) (Subsemigroup.carrier (sInf (toSubmonoid '' f)).1)
⊢ Submonoid.MulSaturated.{u_1} (M := M) { carrier := ⋂ s ∈ f, (↑s : Set M), mul_mem' := ⋯, one_mem' := ⋯ }

Tactic:
convert! Submonoid.MulSaturated.sInf (f := toSubmonoid '' f) (by simp)

Premises used: Submonoid.MulSaturated.sInf
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
h :
  ∀ (x : M),
    Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) x ↔
      Membership.mem (γ := Set M) (Subsemigroup.carrier (sInf (toSubmonoid '' f)).1) x
⊢ Eq.{u_1 + 1} (α := Set M) (⋂ s ∈ f, (↑s : Set M)) (Subsemigroup.carrier (sInf (toSubmonoid '' f)).1)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
x : M
⊢ Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) x ↔
    Membership.mem (γ := Set M) (Subsemigroup.carrier (sInf (toSubmonoid '' f)).1) x

Tactic:
simp [Submonoid.mem_sInf]

Premises used: Submonoid.mem_sInf
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
x : M
⊢ x ∈ sInf f ↔ ∀ s ∈ f, x ∈ s

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
⊢ GaloisConnection saturation fun (x : SaturatedSubmonoid M) ↦ x.toSubmonoid

Tactic:
fun _ _ ↦
  ⟨fun ih _ hx ↦ ih <| SaturatedSubmonoid.mem_sInf.mpr fun _ ht ↦ ht hx,
  fun ih _ hx ↦ SaturatedSubmonoid.mem_sInf.mp hx _ ih⟩

Premises used: Iff.mpr, SaturatedSubmonoid.mem_sInf, Iff.intro, Iff.mp, GaloisConnection
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s : Submonoid M
hs : s.saturation.toSubmonoid ≤ s
⊢ s.saturation.MulSaturated

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
a : Submonoid M
b : SaturatedSubmonoid M
⊢ a.saturation ≤ b ↔ a ≤ b.toSubmonoid

Tactic:
gc_saturation ..

Premises used: Set.Mem, Submonoid.gc_saturation
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
a : Submonoid M
⊢ a ≤ a.saturation.toSubmonoid

Tactic:
(gc_saturation M).le_u_l a

Premises used: GaloisConnection.le_u_l, Submonoid.gc_saturation
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
b : SaturatedSubmonoid M
⊢ b.saturation = b

Tactic:
(giSaturation M).l_u_eq b

Premises used: GaloisInsertion.l_u_eq, Submonoid.giSaturation
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s : Submonoid M
p : (x : M) → x ∈ s.saturation → Prop
mem : ∀ (x : M) (hx : x ∈ s), p x ⋯
mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯
of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯
x : M
hx : x ∈ s.saturation
let : p x hx
⊢ p x hx

Tactic:
let s' : SaturatedSubmonoid M :=
  { carrier := { x | ∃ hx, p x hx }
    one_mem' := ⟨_ , mem 1 <| one_mem s⟩
    mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
    mulSaturated := fun x y ⟨_, hpxy⟩ ↦ ⟨⟨_, (of_mul _ _ _ hpxy).1⟩, ⟨_, (of_mul _ _ _ hpxy).2⟩⟩ }
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s : Submonoid M
p : (x : M) → x ∈ s.saturation → Prop
mem : ∀ (x : M) (hx : x ∈ s), p x ⋯
mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯
of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯
x : M
hx : x ∈ s.saturation
s' : SaturatedSubmonoid M :=
  { carrier := {x : M | ∃ (hx : x ∈ s.saturation), p x hx}, mul_mem' := ⋯, one_mem' := ⋯, mulSaturated := ⋯ }
⊢ p x hx

Tactic:
SaturatedSubmonoid.mem_sInf.mp hx s' (fun _ h ↦ ⟨_, mem _ h⟩) |>.2

Premises used: SaturatedSubmonoid.mem_sInf, Submonoid.le_toSubmonoid_saturation, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s : Submonoid M
p : (x : M) → x ∈ s.saturation → Prop
mem : ∀ (x : M) (hx : x ∈ s), p x ⋯
mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯
of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯
x : M
hx : x ∈ s.saturation
s' : SaturatedSubmonoid M :=
  { carrier := {x : M | ∃ (hx : x ∈ s.saturation), p x hx}, mul_mem' := ⋯, one_mem' := ⋯, mulSaturated := ⋯ }
⊢ p x hx

Tactic:
exact SaturatedSubmonoid.mem_sInf.mp hx s' (fun _ h ↦ ⟨_, mem _ h⟩) |>.2

Premises used: SaturatedSubmonoid.mem_sInf, Submonoid.le_toSubmonoid_saturation, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ (y : M), x * y ∈ s

Tactic:
⟨fun h ↦ ?_, fun ⟨y, hxy⟩ ↦ (s.saturation.2 <| le_toSubmonoid_saturation hxy).1⟩

Premises used: SaturatedSubmonoid.mulSaturated, Membership.mem, _private.0.Submonoid.mem_saturation_iff.match_1, Submonoid.le_toSubmonoid_saturation, And.left, Iff.intro, Submonoid.saturation
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
refine : ∀ (h : x ∈ s.saturation), ∃ (y : M), x * y ∈ s
⊢ x ∈ s.saturation ↔ ∃ (y : M), x * y ∈ s

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨y, hxy⟩ ↦ (s.saturation.2 <| le_toSubmonoid_saturation hxy).1⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x_1 : M
hx : x_1 ∈ s
⊢ x_1 * 1 ∈ s

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x_1 : M
hx : x_1 ∈ s
⊢ ∃ (y : M), x_1 * y ∈ s

Tactic:
exact ⟨1, by simpa⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x_1 y : M
hx : x_1 ∈ s.saturation
hy : y ∈ s.saturation
ih₁ : ∃ (y : M), x_1 * y ∈ s
ih₂ : ∃ (y_1 : M), y * y_1 ∈ s
y₁ : M
h₁ : x_1 * y₁ ∈ s
y₂ : M
h₂ : y * y₂ ∈ s
rw : x_1 * y₁ * (y * y₂) ∈ s
⊢ x_1 * y * (y₁ * y₂) ∈ s

Tactic:
rw [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x_1 y : M
hx : x_1 ∈ s.saturation
hy : y ∈ s.saturation
ih₁ : ∃ (y : M), x_1 * y ∈ s
ih₂ : ∃ (y_1 : M), y * y_1 ∈ s
y₁ : M
h₁ : x_1 * y₁ ∈ s
y₂ : M
h₂ : y * y₂ ∈ s
⊢ x_1 * y₁ * (y * y₂) ∈ s

Tactic:
mul_mem h₁ h₂

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x_1 y : M
hx : x_1 ∈ s.saturation
hy : y ∈ s.saturation
ih₁ : ∃ (y : M), x_1 * y ∈ s
ih₂ : ∃ (y_1 : M), y * y_1 ∈ s
y₁ : M
h₁ : x_1 * y₁ ∈ s
y₂ : M
h₂ : y * y₂ ∈ s
⊢ x_1 * y₁ * (y * y₂) ∈ s

Tactic:
exact mul_mem h₁ h₂

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x_1 y : M
hx : x_1 ∈ s.saturation
hy : y ∈ s.saturation
ih₁ : ∃ (y : M), x_1 * y ∈ s
ih₂ : ∃ (y_1 : M), y * y_1 ∈ s
⊢ ∃ (y_1 : M), x_1 * y * y_1 ∈ s

Tactic:
exact ih₁.elim fun y₁ h₁ ↦ ih₂.elim fun y₂ h₂ ↦
      ⟨y₁ * y₂, by rw [mul_mul_mul_comm]; exact mul_mem h₁ h₂⟩

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy : x₁ * x₂ ∈ s.saturation
ih : ∃ (y : M), x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
rwa rwa₁ rwa₂ rwa₃ : x₁ * x₂ * y ∈ s
⊢ x₁ * (x₂ * y) ∈ s

Tactic:
rwa [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy : x₁ * x₂ ∈ s.saturation
ih : ∃ (y : M), x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
rwa : x₁ * (x₂ * y) ∈ s
rwa₁ rwa₂ rwa₃ rwa₄ : x₁ * x₂ * y ∈ s
⊢ x₂ * (x₁ * y) ∈ s

Tactic:
rwa [mul_left_comm, ← mul_assoc]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy : x₁ * x₂ ∈ s.saturation
ih : ∃ (y : M), x₁ * x₂ * y ∈ s
⊢ (∃ (y : M), x₁ * y ∈ s) ∧ ∃ (y : M), x₂ * y ∈ s

Tactic:
exact ih.elim fun y h ↦ ⟨⟨x₂ * y, by rwa [← mul_assoc]⟩,
      ⟨x₁ * y, by rwa [mul_left_comm, ← mul_assoc]⟩⟩

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
h : x ∈ s.saturation
mem : ∀ (x : M) (hx : x ∈ s), ∃ (y : M), x * y ∈ s
mul :
  ∀ (x y : M),
    x ∈ s.saturation →
      y ∈ s.saturation → ∀ (ih₁ : ∃ (y : M), x * y ∈ s) (ih₂ : ∃ (y_1 : M), y * y_1 ∈ s), ∃ (y_1 : M), x * y * y_1 ∈ s
of_mul :
  ∀ (x₁ x₂ : M),
    x₁ * x₂ ∈ s.saturation → ∀ (ih : ∃ (y : M), x₁ * x₂ * y ∈ s), (∃ (y : M), x₁ * y ∈ s) ∧ ∃ (y : M), x₂ * y ∈ s
⊢ ∃ (y : M), x * y ∈ s

Tactic:
induction h using saturation_induction with
  | mem _ hx => exact ⟨1, by simpa⟩
  | mul _ _ _ _ ih₁ ih₂ =>
    exact ih₁.elim fun y₁ h₁ ↦ ih₂.elim fun y₂ h₂ ↦
      ⟨y₁ * y₂, by rw [mul_mul_mul_comm]; exact mul_mem h₁ h₂⟩
  | of_mul x₁ x₂ _ ih =>
    exact ih.elim fun y h ↦ ⟨⟨x₂ * y, by rwa [← mul_assoc]⟩,
      ⟨x₁ * y, by rwa [mul_left_comm, ← mul_assoc]⟩⟩

Premises used: Submonoid.mul
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
simp_rw : (∃ (y : M), x * y ∈ s) ↔ ∃ (y : M), y * x ∈ s
⊢ x ∈ s.saturation ↔ ∃ (y : M), y * x ∈ s

Tactic:
simp_rw [mem_saturation_iff, mul_comm x]

Premises used: mul_comm, Submonoid.mem_saturation_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
simp_rw : x ∈ s.saturation ↔ ∃ m ∈ s, ∃ (c : M), m = x * c
simp_rw₁ : x ∈ s.saturation ↔ ∃ (c : M), x * c ∈ s ∧ True
simp_rw₂ : x ∈ s.saturation ↔ ∃ (c : M), x * c ∈ s
⊢ x ∈ s.saturation ↔ ∃ m ∈ s, x ∣ m

Tactic:
simp_rw [dvd_def, existsAndEq, and_true, mem_saturation_iff]

Premises used: dvd_def, and_true, ExistsAndEq.existsAndEq, Submonoid.mem_saturation_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq.{u_1 + 1} (α := SaturatedSubmonoid M) ⊥ (Submonoid.saturation ⊥)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s₁ s₂ : SaturatedSubmonoid M
⊢ s₁ ⊔ s₂ = (s₁.toSubmonoid ⊔ s₂.toSubmonoid).saturation

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ sSup f = (sSup (toSubmonoid '' f)).saturation

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_2
f : ι → SaturatedSubmonoid M
⊢ iSup f = Submonoid.saturation (⨆ (i : ι), (f i).toSubmonoid)

Tactic:
(Submonoid.giSaturation M).l_iSup_u f |>.symm

Premises used: Eq.symm, GaloisInsertion.l_iSup_u, Submonoid.giSaturation
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : CommMonoid M
x : M
simp_rw : Membership.mem (γ := SaturatedSubmonoid M) (Submonoid.saturation ⊥) x ↔ IsUnit x
simp_rw₁ : (∃ (y : M), Membership.mem (γ := Submonoid M) ⊥ (x * y)) ↔ IsUnit x
simp_rw₂ : (∃ (y : M), x * y = 1) ↔ IsUnit x
⊢ Membership.mem (γ := SaturatedSubmonoid M) ⊥ x ↔ IsUnit x

Tactic:
simp_rw [bot_def, Submonoid.mem_saturation_iff, Submonoid.mem_bot, isUnit_iff_exists_inv]

Premises used: isUnit_iff_exists_inv, Submonoid.mem_bot, SaturatedSubmonoid.bot_def, Submonoid.mem_saturation_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq.{u_1 + 1} (α := SaturatedSubmonoid M) (saturation ⊥) ⊥

Tactic:
(gc_saturation M).l_bot

Premises used: GaloisConnection.l_bot, Submonoid.gc_saturation
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq.{u_1 + 1} (α := SaturatedSubmonoid M) (saturation ⊤) ⊤

Tactic:
(giSaturation M).l_top

Premises used: Submonoid.giSaturation, GaloisInsertion.l_top
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
s₁ s₂ : Submonoid M
⊢ (s₁ ⊔ s₂).saturation = s₁.saturation ⊔ s₂.saturation

Tactic:
(gc_saturation M).l_sup

Premises used: GaloisConnection.l_sup, Submonoid.gc_saturation
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (Submonoid M)
⊢ (sSup f).saturation = ⨆ s ∈ f, s.saturation

Tactic:
(gc_saturation M).l_sSup

Premises used: GaloisConnection.l_sSup, Submonoid.gc_saturation
-- Module: Mathlib.Algebra.Group.Submonoid.Saturation
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_2
f : ι → Submonoid M
⊢ (iSup f).saturation = ⨆ (i : ι), (f i).saturation

Tactic:
(gc_saturation M).l_iSup

Premises used: GaloisConnection.l_iSup, Submonoid.gc_saturation
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
⊢ ∀ {x : G}, x ∈ (M ⊓ M⁻¹).carrier → x⁻¹ ∈ (M ⊓ M⁻¹).carrier

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
x : G
⊢ x ∈ M.mulSupport ↔ x ∈ M ∧ x⁻¹ ∈ M

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.preimage
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
⊢ M.mulSupport.toSubmonoid = M ⊓ M⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
x : Subgroup G
x_1 : Submonoid G
h : x.toSubmonoid ≤ x_1
x_2 : G
⊢ x_2 ∈ x → x_2 ∈ x_1.mulSupport

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
h : ∀ x ∈ M, x⁻¹ ∈ M → x = 1
⊢ M.IsMulPointed

Tactic:
h

Premises used: Submonoid.IsMulPointed
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
hM : M.IsMulPointed
x : G
hx₁ : x ∈ M
hx₂ : x⁻¹ ∈ M
⊢ x = 1

Tactic:
hM _ hx₁ hx₂
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
⊢ M.IsMulPointed → M.mulSupport = ⊥

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
h : M.mulSupport = ⊥
x : G
⊢ (x ∈ M.mulSupport) = Membership.mem (γ := Subgroup G) ⊥ x

Tactic:
apply_fun (x ∈ ·) at h

Premises used: Membership.mem
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
x : G
h : (x ∈ M.mulSupport) = Membership.mem (γ := Subgroup G) ⊥ x
⊢ x ∈ M → x⁻¹ ∈ M → x = 1

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
h : ∀ (a : G), a ∈ M ∨ a⁻¹ ∈ M
⊢ M.IsMulSpanning

Tactic:
h

Premises used: Submonoid.IsMulSpanning
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
hM : M.IsMulSpanning
a : G
⊢ a ∈ M ∨ a⁻¹ ∈ M

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M N : Submonoid G
hM : M.IsMulSpanning
h : M ≤ N
⊢ N.IsMulSpanning

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : M ≤ N
⊢ ∀ ⦃x : G⦄, x ∈ M → x ∈ N

Tactic:
rw [SetLike.le_def] at h ⊢

Premises used: SetLike.le_def
-- Module: Mathlib.Algebra.Group.Submonoid.Support
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : ∀ ⦃x : G⦄, x ∈ M → x ∈ N
⊢ ∀ ⦃x : G⦄, x ∈ N → x ∈ M

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Submonoid.Units
Goal:
M : Type u_1
inst : Monoid M
⊢ Monotone.{u_1, u_1} (α := Submonoid M) units

Tactic:
fun _ _ hST _ ⟨h₁, h₂⟩ => ⟨hST h₁, hST h₂⟩

Premises used: Submonoid.units, Monotone, Membership.mem, _private.0.Submonoid.units_mono.match_1, And.intro