awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ (↑(toSubmonoid (closure S)) : Set G)

Tactic:
simp only [true_and, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]

Premises used: Set.union_subset_iff, Subgroup.subset_closure, Subgroup.inv_subset_closure, Subgroup.coe_toSubmonoid, true_and
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
g : G
rw : Eq (α := Submonoid G) (toSubmonoid (closure {g})) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₁ : Eq (α := Submonoid G) (Submonoid.closure ({g} ∪ {g}⁻¹)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₂ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₃ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.closure {g} ⊔ Submonoid.powers g⁻¹)
rw₄ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹)
    (Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹})
rw₅ rw₆ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹})
    (Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹})
⊢ Eq (α := Submonoid G) (toSubmonoid (zpowers g)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)

Tactic:
rw [zpowers_eq_closure, closure_toSubmonoid, Submonoid.closure_union,
    Submonoid.powers_eq_closure, Submonoid.powers_eq_closure, Set.inv_singleton]

Premises used: Subgroup.closure_toSubmonoid, Submonoid.powers_eq_closure, Set.inv_singleton, Submonoid.closure_union, Subgroup.zpowers_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
g : G
rw : LE.le (α := Submonoid G) (Submonoid.powers g) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
⊢ LE.le (α := Submonoid G) (Submonoid.powers g) (toSubmonoid (zpowers g))

Tactic:
rw [toSubmonoid_zpowers]

Premises used: Subgroup.toSubmonoid_zpowers
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
g : G
⊢ LE.le (α := Submonoid G) (Submonoid.powers g) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
g : G
⊢ LE.le (α := Submonoid G) (Submonoid.powers g) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Subgroup G) (closure s) y), p y hy → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Subgroup G) (closure s) y), p y hy → p (x⁻¹ * y) ⋯
x : G
h : Membership.mem (γ := Subgroup G) (closure s) x
revert : ∀ (h : Membership.mem (γ := Subgroup G) (closure s) x), p x h
⊢ p x h

Tactic:
revert h
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Subgroup G) (closure s) y), p y hy → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Subgroup G) (closure s) y), p y hy → p (x⁻¹ * y) ⋯
x : G
simp_rw :
  ∀
    (mul_left :
      ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
        p y ⋯ → p (x * y) ⋯)
    (inv_mul_cancel :
      ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
        p y ⋯ → p (x⁻¹ * y) ⋯)
    (h : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) x), p x ⋯
⊢ ∀ (h : Membership.mem (γ := Subgroup G) (closure s) x), p x h

Tactic:
simp_rw [← mem_toSubmonoid, closure_toSubmonoid] at *

Premises used: Subgroup.closure_toSubmonoid, Subgroup.mem_toSubmonoid
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
⊢ p 1 ⋯

Tactic:
one
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
⊢ p 1 ⋯

Tactic:
exact one
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x_1 : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
x y : G
hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y
ih : p y ⋯
hx : x ∈ s
⊢ p (x * y) ⋯

Tactic:
mul_left _ hx _ hy ih
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x_1 : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
x y : G
hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y
ih : p y ⋯
hx : x ∈ s
⊢ p (x * y) ⋯

Tactic:
exact mul_left _ hx _ hy ih
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x_1 : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
x y : G
hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y
ih : p y ⋯
hx : x ∈ s⁻¹
⊢ p (x * y) ⋯

Tactic:
simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x_1 : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
x : G
hx : x ∈ s ∪ s⁻¹
y : G
hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y
ih : p y ⋯
mul_left₁ : ∀ (hx : x ∈ s), p (x * y) ⋯
mul_left₂ : ∀ (hx : x ∈ s⁻¹), p (x * y) ⋯
⊢ p (x * y) ⋯

Tactic:
cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
h : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) x
one₁ : p 1 ⋯
mul_left₁ :
  ∀ (x : G) (hx : x ∈ s ∪ s⁻¹) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y)
    (ih : p y ⋯), p (x * y) ⋯
⊢ p x ⋯

Tactic:
induction h using Submonoid.closure_induction_left with
  | one => exact one
  | mul_left x hx y hy ih =>
    cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel :
  ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : Membership.mem (γ := Subgroup G) (closure s) x
m : Gᵐᵒᵖ
hm : Membership.mem (γ := Subgroup Gᵐᵒᵖ) (closure (MulOpposite.unop ⁻¹' s)) m
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hm : Membership.mem (γ := Subgroup Gᵐᵒᵖ) (Subgroup.op (closure s)) m),
    Membership.mem (γ := Subgroup G) (closure s) (MulOpposite.unop m)
⊢ Membership.mem (γ := Subgroup G) (closure s) (MulOpposite.unop m)

Tactic:
rwa [← op_closure] at hm

Premises used: Subgroup.op_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel :
  ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : Membership.mem (γ := Subgroup G) (closure s) x
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Subgroup Gᵐᵒᵖ) (Subgroup.op (closure s)) { unop' := x : PreOpposite G }
⊢ Membership.mem (γ := Subgroup Gᵐᵒᵖ) (closure (MulOpposite.unop ⁻¹' s)) { unop' := x : PreOpposite G }

Tactic:
rwa [← op_closure]

Premises used: Subgroup.op_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ Eq (α := Subgroup G) (closure s⁻¹) (closure s)

Tactic:
simp only [← toSubmonoid_inj, closure_toSubmonoid, inv_inv, union_comm]

Premises used: Subgroup.closure_toSubmonoid, Set.union_comm, inv_inv, Subgroup.toSubmonoid_inj
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
x : G
rw : Eq (α := Subgroup G) (closure {x}⁻¹) (closure {x})
rw₁ rw₂ : Eq (α := Subgroup G) (closure {x}) (closure {x})
⊢ Eq (α := Subgroup G) (closure {x⁻¹}) (closure {x})

Tactic:
rw [← Set.inv_singleton, closure_inv]

Premises used: Subgroup.closure_inv, Set.inv_singleton
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (g : G) → Membership.mem (γ := Subgroup G) (closure s) g → Prop
mem : ∀ (x : G) (hx : x ∈ s), p x ⋯
inv_mem : ∀ (x : G) (hx : x ∈ s), p x⁻¹ ⋯
one : p 1 ⋯
mul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x)
    (hy : Membership.mem (γ := Subgroup G) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : G
h : Membership.mem (γ := Subgroup G) (closure s) x
⊢ p x h

Tactic:
closure_induction_left one (fun x hx y _ hy => mul x y _ _ (mem x hx) hy)
    (fun x hx y _ => mul x⁻¹ y _ _ <| inv_mem x hx) h

Premises used: Subgroup.closure_induction_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x

Tactic:
rw [iSup_eq_closure] at hx

Premises used: Subgroup.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
hx₁ : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
⊢ ∀ (i : ι), ∀ x ∈ S i, C x

Tactic:
rw [iSup_eq_closure] at hx

Premises used: Subgroup.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
hx₁ : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
mem₁ : ∀ (i : ι), ∀ x ∈ S i, C x
⊢ C 1

Tactic:
rw [iSup_eq_closure] at hx

Premises used: Subgroup.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
hx₁ : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
mem₁ : ∀ (i : ι), ∀ x ∈ S i, C x
one₁ : C 1
⊢ ∀ (x y : G), C x → C y → C (x * y)

Tactic:
rw [iSup_eq_closure] at hx

Premises used: Subgroup.iSup_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C 1

Tactic:
one
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C 1

Tactic:
exact one
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x
mem₁ : ∀ (i : ι) (hi : x ∈ (↑(S i) : Set G)), C x
⊢ C x

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

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x
i : ι
hi : x ∈ (↑(S i) : Set G)
⊢ C x

Tactic:
mem _ _ hi
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x
i : ι
hi : x ∈ (↑(S i) : Set G)
⊢ C x

Tactic:
exact mem _ _ hi
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x
inv_mem : ∀ (i : ι) (hi : x ∈ (↑(S i) : Set G)), C x⁻¹
⊢ C x⁻¹

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

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x
i : ι
hi : x ∈ (↑(S i) : Set G)
⊢ C x⁻¹

Tactic:
mem _ _ (inv_mem hi)

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x
i : ι
hi : x ∈ (↑(S i) : Set G)
⊢ C x⁻¹

Tactic:
exact mem _ _ (inv_mem hi)

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x y : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) y
ihx : C x
ihy : C y
⊢ C (x * y)

Tactic:
mul x y ihx ihy
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x y : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) y
ihx : C x
ihy : C y
⊢ C (x * y)

Tactic:
exact mul x y ihx ihy
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
one₁ : C 1
mem₁ : ∀ (x : G) (hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x), C x
inv_mem : ∀ (x : G) (hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x), C x⁻¹
mul₁ :
  ∀ (x y : G),
    Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x →
      Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) y → ∀ (ihx : C x) (ihy : C y), C (x * y)
⊢ C x

Tactic:
induction hx using closure_induction'' with
  | one => exact one
  | mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ hi
  | inv_mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ (inv_mem hi)
  | mul x y _ _ ihx ihy => exact mul x y ihx ihy

Premises used: Set.mem_iUnion, InvMemClass.inv_mem, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
suffices : ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h
⊢ C x hx

Tactic:
suffices ∃ h, C x h from this.snd
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
⊢ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h

Tactic:
iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => ?_) ?_ fun x y => ?_

Premises used: Subgroup.iSup_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
refine_1 :
  ∀ (i : ι) (x : G) (hx : x ∈ S i), (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) x
refine_2 : ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) 1), C 1 h
refine_3 :
  ∀ (x y : G),
    (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) x →
      (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) y →
        (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) (x * y)
⊢ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h

Tactic:
refine iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => ?_) ?_ fun x y => ?_

Premises used: Subgroup.iSup_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x_1
i : ι
x : G
hx : x ∈ S i
⊢ (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) x

Tactic:
⟨_, hp i _ hx⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x_1
i : ι
x : G
hx : x ∈ S i
⊢ (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) x

Tactic:
exact ⟨_, hp i _ hx⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
⊢ (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) 1

Tactic:
⟨_, h1⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
⊢ (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) 1

Tactic:
exact ⟨_, h1⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x_1 : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x_1
x y : G
w : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
Cx : C x w
w_1 : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y
Cy : C y w_1
⊢ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) (x * y)), C (x * y) h

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

Premises used: Exists.intro