awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Premises used: iSup, Membership.mem, le_iSup, Iff.intro, _private.0.Subsemigroup.mem_iSup_of_directed.match_1
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
refine : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
this : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
simpa only [closure_iUnion, closure_eq (S _)] using this

Premises used: Subsemigroup.closure_iUnion, Subsemigroup.closure_eq
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
suffices : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i

Tactic:
fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ hx

Premises used: Subsemigroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
refine_1 :
  ∀ (hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x) (x : M)
    (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x), ∃ (i : ι), x ∈ S i
refine_2 :
  ∀ (hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x) (x y : M)
    (hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y),
    (∃ (i : ι), x ∈ S i) → (∃ (i : ι), y ∈ S i) → ∃ (i : ι), x * y ∈ S i
⊢ Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i

Tactic:
refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ hx
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
x_1 : M
⊢ ∀ (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x_1), ∃ (i : ι), x_1 ∈ S i

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x_1 : M
hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
x y : M
hx_1 : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
hy : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
refine_2 : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), ∃ (i : ι), x * y ∈ S i
⊢ ∃ (i : ι), x * y ∈ S i

Tactic:
obtain ⟨k, hik, hjk⟩ := hS i j
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x_1 : M
hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
x y : M
hx_1 : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
hy : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ ∃ (i : ι), x * y ∈ S i

Tactic:
⟨k, mul_mem (hik hi) (hjk hj)⟩

Premises used: Exists.intro, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x_1 : M
hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
x y : M
hx_1 : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
hy : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ ∃ (i : ι), x * y ∈ S i

Tactic:
exact ⟨k, mul_mem (hik hi) (hjk hj)⟩
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
rw : (∃ (i : Subtype p), x ∈ S (↑i : ι)) ↔ ∃ (i : ι), p i ∧ x ∈ S i
hS₁ : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) fun (x : Subtype p) ↦ S (↑x : ι)
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i

Tactic:
rw [iSup_subtype', mem_iSup_of_directed]

Premises used: iSup_subtype', Subsemigroup.mem_iSup_of_directed
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ (∃ (i : Subtype p), x ∈ S (↑i : ι)) ↔ ∃ (i : ι), p i ∧ x ∈ S i

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
hS₁ : Directed (ι := Subtype p) (S ⁻¹'o fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) (Subtype.val (p := p))
⊢ Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) fun (x : Subtype p) ↦ S (↑x : ι)

Tactic:
rw [← Function.comp_def, directed_comp]

Premises used: Function.comp_def, directed_comp
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Directed (ι := Subtype p) (S ⁻¹'o fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) (Subtype.val (p := p))

Tactic:
hS.directed_val

Premises used: Set.Mem, setOf, DirectedOn.directed_val, Order.Preimage
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Directed (ι := Subtype p) (S ⁻¹'o fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) (Subtype.val (p := p))

Tactic:
exact hS.directed_val

Premises used: DirectedOn.directed_val
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
p : Prop
S : p → Subsemigroup M
x : M
pos : ∀ (h : p), Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h
neg : ∀ (h : ¬p), Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h

Tactic:
by_cases h : p
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : p
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h

Tactic:
simp +contextual [h]
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : ¬p
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h

Tactic:
simpa [h] using id

Premises used: id
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
⊢ x ∈ (↑(⨆ (i : ι), S i) : Set M) ↔ Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x

Tactic:
simp [mem_iSup_of_directed hS]

Premises used: Subsemigroup.mem_iSup_of_directed
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u_2} ↥(⨆ (i : ι), S i)

Tactic:
.of_setLike_mul_comm ?_

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

Tactic:
refine .of_setLike_mul_comm ?_
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemigroup 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 (γ := Subsemigroup M) (⨆ (i : ι), S i) a →
      ∀ (b : M), Membership.mem (γ := Subsemigroup 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: Set.mem_iUnion, forall_exists_index, SetLike.mem_coe, Subsemigroup.coe_iSup_of_directed
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemigroup 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.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemigroup 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.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemigroup 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.Subsemigroup.Membership
Goal:
ι_1 : Sort u_1
M : Type u_2
inst : Mul M
ι : Type u_3
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
S : OrderHom.{u_3, u_2} ι (Subsemigroup M)
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥((S : (a : ι) → Subsemigroup M) i : Subsemigroup M)
⊢ IsMulCommutative.{u_2} ↥(⨆ (i : ι), (S : (a : ι) → Subsemigroup M) i)

Tactic:
isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, Subsemigroup.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, exists_prop]

Premises used: Subsemigroup.mem_iSup_of_directed, SetCoe.exists, exists_prop, DirectedOn.directed_val, sSup_eq_iSup'
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
⊢ x ∈ (↑(sSup S) : Set M) ↔ Membership.mem (γ := Set M) (⋃ s ∈ S, (↑s : Set M)) x

Tactic:
simp [mem_sSup_of_directed_on hS]

Premises used: Subsemigroup.mem_sSup_of_directed_on
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup M
⊢ S ≤ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup M
⊢ T ≤ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup M
x y : M
hx : x ∈ S
hy : y ∈ T
⊢ x * y ∈ S ⊔ T

Tactic:
mul_mem (mem_sup_left hx) (mem_sup_right hy)

Premises used: Subsemigroup.mem_sup_left, Subsemigroup.mem_sup_right, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
i : ι
⊢ S i ≤ iSup S

Tactic:
have : S i ≤ iSup S := le_iSup _ _
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
⊢ s ≤ sSup S

Tactic:
have : s ≤ sSup S := le_sSup hs
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁

Tactic:
rw [iSup_eq_closure] at hx₁

Premises used: Subsemigroup.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
hx₂ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
⊢ ∀ (i : ι), ∀ x₂ ∈ S i, C x₂

Tactic:
rw [iSup_eq_closure] at hx₁

Premises used: Subsemigroup.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
hx₂ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
mem₁ : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
⊢ ∀ (x y : M), C x → C y → C (x * y)

Tactic:
rw [iSup_eq_closure] at hx₁

Premises used: Subsemigroup.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁

Tactic:
closure_induction (fun x₂ hx₂ => ?_) (fun x y _ _ ↦ mul x y) hx₁

Premises used: Subsemigroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
refine : ∀ (x₂ : M) (hx₂ : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x₂), C x₂
⊢ C x₁

Tactic:
refine closure_induction (fun x₂ hx₂ => ?_) (fun x y _ _ ↦ mul x y) hx₁
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x₂
obtain : ∀ (i : ι) (hi : x₂ ∈ (↑(S i) : Set M)), C x₂
⊢ C x₂

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

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x₂
i : ι
hi : x₂ ∈ (↑(S i) : Set M)
⊢ C x₂

Tactic:
mem _ _ hi
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x₂
i : ι
hi : x₂ ∈ (↑(S i) : Set M)
⊢ C x₂

Tactic:
exact mem _ _ hi
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
⊢ C x₁ hx₁

Tactic:
Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
refine : ∃ (x : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁), C x₁ x
⊢ C x₁ hx₁

Tactic:
refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
⊢ ∃ (x : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁), C x₁ x

Tactic:
@iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
      (fun i x₂ hx₂ => ?_) fun x₃ y => ?_

Premises used: Subsemigroup.iSup_induction
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
refine_1 :
  ∀ (i : ι) (x₂ : M) (hx₂ : x₂ ∈ S i),
    (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') x₂
refine_2 :
  ∀ (x₃ y : M),
    (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') x₃ →
      (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') y →
        (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') (x₃ * y)
⊢ ∃ (x : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁), C x₁ x

Tactic:
refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
      (fun i x₂ hx₂ => ?_) fun x₃ y => ?_

Premises used: Subsemigroup.iSup_induction
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
i : ι
x₂ : M
hx₂ : x₂ ∈ S i
⊢ (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') x₂

Tactic:
⟨_, mem _ _ hx₂⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
i : ι
x₂ : M
hx₂ : x₂ ∈ S i
⊢ (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') x₂

Tactic:
exact ⟨_, mem _ _ hx₂⟩
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
x₃ y : M
w : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₃
Cx : C x₃ w
w_1 : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y
Cy : C y w_1
⊢ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) (x₃ * y)), C (x₃ * y) hx''

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

Premises used: Exists.intro