awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u_1} ↥(⨆ (i : ι), S i)

Tactic:
.of_setLike_mul_comm ?_

Premises used: IsMulCommutative.of_setLike_mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
refine :
  ∀ (a : M),
    Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) a →
      ∀ (b : M), Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) b → a * b = b * a
⊢ IsMulCommutative.{u_1} ↥(⨆ (i : ι), S i)

Tactic:
refine .of_setLike_mul_comm ?_
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
simp_rw : ∀ (a : M) (x : ι) (h : a ∈ S x) (b : M) (x : ι) (h : b ∈ S x), a * b = b * a
⊢ ∀ (a : M),
    Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) a →
      ∀ (b : M), Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) b → a * b = b * a

Tactic:
simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]

Premises used: Submonoid.coe_iSup_of_directed, Set.mem_iUnion, forall_exists_index, SetLike.mem_coe
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
obtain : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), a * b = b * a
⊢ a * b = b * a

Tactic:
obtain ⟨k, hik, hjk⟩ := dir i j
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ a * b = b * a

Tactic:
setLike_mul_comm (hik ha) (hjk hb)

Premises used: setLike_mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ a * b = b * a

Tactic:
exact setLike_mul_comm (hik ha) (hjk hb)

Premises used: setLike_mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : MulOneClass M
ι : Type u_4
inst_1 : Nonempty ι
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
S : OrderHom.{u_4, u_1} ι (Submonoid M)
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥((S : (a : ι) → Submonoid M) i : Submonoid M)
⊢ IsMulCommutative.{u_1} ↥(⨆ (i : ι), (S : (a : ι) → Submonoid M) i)

Tactic:
Submonoid.isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, Submonoid.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
⊢ S ≤ S ⊔ T

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
⊢ S ≤ S ⊔ T

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
x y : M
hx : x ∈ S
hy : y ∈ T
⊢ x * y ∈ S ⊔ T

Tactic:
(S ⊔ T).mul_mem (mem_sup_left hx) (mem_sup_right hy)

Premises used: Submonoid.mul_mem, Submonoid.mem_sup_left, Max.max, Submonoid.mem_sup_right
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S

Tactic:
le_iSup _ _

Premises used: le_iSup
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S

Tactic:
exact le_iSup _ _

Premises used: le_iSup
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ s ≤ sSup S

Tactic:
le_sSup hs

Premises used: le_sSup
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ s ≤ sSup S

Tactic:
exact le_sSup hs

Premises used: le_sSup
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
⊢ Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x

Tactic:
rw [iSup_eq_closure] at hx

Premises used: Submonoid.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
hx₁ : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
⊢ ∀ (i : ι), ∀ x ∈ S i, motive x

Tactic:
rw [iSup_eq_closure] at hx

Premises used: Submonoid.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
hx₁ : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
mem₁ : ∀ (i : ι), ∀ x ∈ S i, motive x
⊢ motive 1

Tactic:
rw [iSup_eq_closure] at hx

Premises used: Submonoid.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
hx₁ : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
mem₁ : ∀ (i : ι), ∀ x ∈ S i, motive x
one₁ : motive 1
⊢ ∀ (x y : M), motive x → motive y → motive (x * y)

Tactic:
rw [iSup_eq_closure] at hx

Premises used: Submonoid.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
⊢ motive x

Tactic:
closure_induction (fun x hx => ?_) one (fun _ _ _ _ ↦ mul _ _) hx

Premises used: Submonoid.closure_induction
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
refine : ∀ (x : M) (hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x), motive x
⊢ motive x

Tactic:
refine closure_induction (fun x hx => ?_) one (fun _ _ _ _ ↦ mul _ _) hx
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x_1 : M
hx_1 : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x
obtain : ∀ (i : ι) (hi : x ∈ (↑(S i) : Set M)), motive x
⊢ motive x

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x_1 : M
hx_1 : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x
i : ι
hi : x ∈ (↑(S i) : Set M)
⊢ motive x

Tactic:
mem _ _ hi
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x_1 : M
hx_1 : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x
i : ι
hi : x ∈ (↑(S i) : Set M)
⊢ motive x

Tactic:
exact mem _ _ hi
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
⊢ motive x hx

Tactic:
Exists.elim (?_ : ∃ Hx, motive x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) => hc

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
refine : ∃ (Hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x), motive x Hx
⊢ motive x hx

Tactic:
refine Exists.elim (?_ : ∃ Hx, motive x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) => hc

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
⊢ ∃ (Hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x), motive x Hx

Tactic:
@iSup_induction _ _ ι S (fun m => ∃ hm, motive m hm) _ hx (fun i x hx => ?_) ?_
      fun x y => ?_

Premises used: Submonoid.iSup_induction
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
refine_1 :
  ∀ (i : ι) (x : M) (hx : x ∈ S i),
    (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) x
refine_2 : ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) 1), motive 1 hm
refine_3 :
  ∀ (x y : M),
    (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) x →
      (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) y →
        (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) (x * y)
⊢ ∃ (Hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x), motive x Hx

Tactic:
refine @iSup_induction _ _ ι S (fun m => ∃ hm, motive m hm) _ hx (fun i x hx => ?_) ?_
      fun x y => ?_

Premises used: Submonoid.iSup_induction
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x_1 : M
hx_1 : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x_1
i : ι
x : M
hx : x ∈ S i
⊢ (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) x

Tactic:
⟨_, mem _ _ hx⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x_1 : M
hx_1 : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x_1
i : ι
x : M
hx : x ∈ S i
⊢ (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) x

Tactic:
exact ⟨_, mem _ _ hx⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
⊢ (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) 1

Tactic:
⟨_, one⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
⊢ (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) 1

Tactic:
exact ⟨_, one⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x_1 : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x_1
x y : M
w : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
Cx : motive x w
w_1 : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y
Cy : motive y w_1
⊢ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) (x * y)), motive (x * y) hm

Tactic:
⟨_, mul _ _ _ _ Cx Cy⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x_1 : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x_1
x y : M
w : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
Cx : motive x w
w_1 : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y
Cy : motive y w_1
⊢ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) (x * y)), motive (x * y) hm

Tactic:
exact ⟨_, mul _ _ _ _ Cx Cy⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
α : Type u_4
⊢ Eq.{u_4 + 1} (α := Submonoid (FreeMonoid α)) (closure (Set.range of)) ⊤

Tactic:
eq_top_iff.2 fun x _ =>
    FreeMonoid.recOn x (one_mem _) fun _x _xs hxs =>
      mul_mem (subset_closure <| Set.mem_range_self _) hxs

Premises used: Iff.mpr, eq_top_iff, FreeMonoid.recOn
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x : M
⊢ Eq (α := Submonoid M) (closure {x})
    (mrange (F := Multiplicative ℕ →* M) ((powersHom M : (a : M) → Multiplicative ℕ →* M) x : Multiplicative ℕ →* M))

Tactic:
closure_eq_of_le (Set.singleton_subset_iff.2 ⟨Multiplicative.ofAdd 1, pow_one x⟩) fun _ ⟨_, hn⟩ =>
    hn ▸ pow_mem (subset_closure <| Set.mem_singleton _) _

Premises used: Iff.mpr, Set.mem_singleton, Set.singleton_subset_iff, _private.0.Submonoid.closure_singleton_eq.match_1, Membership.mem, Eq.rec, Submonoid.closure_eq_of_le, pow_one, Submonoid.closure, Exists.intro, pow_mem, Multiplicative.toAdd, Multiplicative.ofAdd, Singleton.singleton, OfNat.ofNat, Submonoid.subset_closure, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x y : M
rw :
  (∃ (x_1 : Multiplicative ℕ),
      (((powersHom M : (a : M) → Multiplicative ℕ →* M) x : Multiplicative ℕ →* M) : (a : Multiplicative ℕ) → M) x_1 =
        y) ↔
    ∃ (n : ℕ), x ^ n = y
⊢ Membership.mem (γ := Submonoid M) (closure {x}) y ↔ ∃ (n : ℕ), x ^ n = y

Tactic:
rw [closure_singleton_eq, mem_mrange]

Premises used: Submonoid.closure_singleton_eq, MonoidHom.mem_mrange
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x y : M
⊢ (∃ (x_1 : Multiplicative ℕ),
      (((powersHom M : (a : M) → Multiplicative ℕ →* M) x : Multiplicative ℕ →* M) : (a : Multiplicative ℕ) → M) x_1 =
        y) ↔
    ∃ (n : ℕ), x ^ n = y

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
y : M
⊢ Membership.mem (γ := Submonoid M) (closure {y}) y

Tactic:
mem_closure_singleton.2 ⟨1, pow_one y⟩

Premises used: Iff.mpr, Submonoid.mem_closure_singleton, pow_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq (α := Submonoid M) (closure {1}) ⊥

Tactic:
simp [eq_bot_iff_forall, mem_closure_singleton]

Premises used: Submonoid.eq_bot_iff_forall, Submonoid.mem_closure_singleton
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x : Fintype ↥⊥
⊢ card.{u_1} ↥⊥ = 1

Tactic:
card_eq_one_iff.2
    ⟨⟨(1 : M), Set.mem_singleton 1⟩, fun ⟨_y, hy⟩ => Subtype.ext <| mem_bot.1 hy⟩

Premises used: Iff.mpr, Set.mem_singleton, Submonoid.mem_bot, Subtype.mk, Exists.intro, Iff.mp, OfNat.ofNat, Eq, Fintype.card_eq_one_iff, _private.0.Submonoid.card_bot.match_1, Subtype.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
inst_1 : Fintype ↥S
h : card.{u_1} ↥S ≤ 1
⊢ S = ⊥

Tactic:
let _ := card_le_one_iff_subsingleton.mp h
  eq_bot_of_subsingleton S

Premises used: Submonoid.eq_bot_of_subsingleton, Iff.mp, Fintype.card_le_one_iff_subsingleton
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
inst_1 : Fintype ↥S
h : card.{u_1} ↥S = 1
⊢ S = ⊥

Tactic:
S.eq_bot_of_card_le (le_of_eq h)

Premises used: Submonoid.eq_bot_of_card_le, le_of_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
inst_1 : Fintype ↥S
h : card.{u_1} ↥S ≤ 1
x : M
hx : x ∈ S
⊢ x = 1

Tactic:
simpa [Subtype.ext_iff] using card_le_one_iff.1 h ⟨x, hx⟩ 1

Premises used: Fintype.card_le_one_iff, Subtype.ext_iff, Subtype.mk, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
inst_1 : Fintype ↥S
h : S = ⊥
⊢ card.{u_1} ↥S ≤ 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Fintype ↥⊥
⊢ card.{u_1} ↥⊥ = 1

Tactic:
card_bot

Premises used: Submonoid.card_bot
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Fintype ↥⊥
⊢ card.{u_1} ↥⊥ = 1

Tactic:
exact card_bot

Premises used: Submonoid.card_bot
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
α : Type u_4
f : α → M
rw :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) ⊤)
    (closure (Set.range f))
rw₁ :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      (closure (Set.range FreeMonoid.of)))
    (closure (Set.range f))
rw₂ :
  Eq (α := Submonoid M)
    (closure
      (Set.image.{u_4, u_1} (α := FreeMonoid α)
        (⇑((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) :
          (a : FreeMonoid α) → M)
        (Set.range FreeMonoid.of)))
    (closure (Set.range f))
rw₃ :
  Eq (α := Submonoid M)
    (closure
      (Set.range.{u_1, u_4 + 1} (ι := α)
        ((⇑((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) :
            (a : FreeMonoid α) → M) ∘
          FreeMonoid.of)))
    (closure (Set.range f))
rw₄ rw₅ : Eq (α := Submonoid M) (closure (Set.range f)) (closure (Set.range f))
⊢ Eq (α := Submonoid M)
    (mrange (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M))
    (closure (Set.range f))

Tactic:
rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]

Premises used: Set.range_comp, MonoidHom.mrange_eq_map, FreeMonoid.lift_comp_of, FreeMonoid.closure_range_of, MonoidHom.map_mclosure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
rw :
  Eq (α := Submonoid M) (closure s)
    (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
rw₁ rw₂ : Eq (α := Submonoid M) (closure s) (closure s)
⊢ Eq (α := Submonoid M) (closure s)
    (mrange (F := FreeMonoid { x : M // x ∈ s } →* M)
      ((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
          (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
        FreeMonoid { x : M // x ∈ s } →* M))

Tactic:
rw [FreeMonoid.mrange_lift, Subtype.range_coe]

Premises used: Subtype.range_coe, FreeMonoid.mrange_lift