awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
i j : PLift ι
hK₁ :
  ∀ (a : ι),
    (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) (K i.down) (K a) ∧ (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) (K j.down) (K a) →
      K i.down ≤ K a ∧ K j.down ≤ K a
⊢ ∃ (x : ι), K i.down ≤ K x ∧ K j.down ≤ K x

Tactic:
refine (hK i.down j.down).imp ?_

Premises used: Exists.imp, PLift.down
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
i j : PLift ι
⊢ ∀ (a : ι),
    (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) (K i.down) (K a) ∧ (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) (K j.down) (K a) →
      K i.down ≤ K a ∧ K j.down ≤ K a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
⊢ PLift ι

Tactic:
exact PLift.up hι.some

Premises used: Nonempty.some, PLift.up
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
p : Prop
K : p → Subgroup G
x : G
pos : ∀ (h : p), Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
neg : ∀ (h : ¬p), Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
⊢ Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

Tactic:
by_cases h : p
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
p : Prop
K : p → Subgroup G
x : G
h : p
⊢ Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

Tactic:
simp +contextual [h]
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
p : Prop
K : p → Subgroup G
x : G
h : ¬p
⊢ Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

Tactic:
simp +contextual [h]
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
x : G
⊢ x ∈ (↑(⨆ (i : ι), S i) : Set G) ↔ Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x

Tactic:
simp [mem_iSup_of_directed hS]

Premises used: Subgroup.mem_iSup_of_directed
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
⊢ Nonempty.{u_1 + 1} (↑K : Type u_1)

Tactic:
haveI : Nonempty K := Kne.to_subtype
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : Nonempty.{u_1 + 1} (↑K : Type u_1)
⊢ x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

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

Premises used: SetCoe.exists, exists_prop, DirectedOn.directed_val, Subgroup.mem_iSup_of_directed, sSup_eq_iSup'
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u_1} ↥(⨆ (i : ι), S i)

Tactic:
.of_setLike_mul_comm ?_

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

Tactic:
refine .of_setLike_mul_comm ?_
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
simp_rw : ∀ (a : G) (x : ι) (h : a ∈ S x) (b : G) (x : ι) (h : b ∈ S x), a * b = b * a
⊢ ∀ (a : G),
    Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) a →
      ∀ (b : G), Membership.mem (γ := Subgroup G) (⨆ (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, Subgroup.coe_iSup_of_directed, SetLike.mem_coe
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
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.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
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.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
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.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
k : Set G
ι : Type u_2
inst_1 : Nonempty ι
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
S : OrderHom.{u_2, u_1} ι (Subgroup G)
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥((S : (a : ι) → Subgroup G) i : Subgroup G)
⊢ IsMulCommutative.{u_1} ↥(⨆ (i : ι), (S : (a : ι) → Subgroup G) i)

Tactic:
isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, Subgroup.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : x ∈ s ⊔ t
⊢ Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x

Tactic:
rw [sup_eq_closure] at h

Premises used: Subgroup.sup_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
Subgroup.closure_induction ?_ ?_ ?_ ?_ h

Premises used: Subgroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
refine_1 : ∀ (x : C) (hx : x ∈ (↑s : Set C) ∪ (↑t : Set C)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
refine_2 : ∃ y ∈ s, ∃ z ∈ t, y * z = 1
refine_3 :
  ∀ (x y : C) (hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x)
    (hy : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) y),
    (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y
refine_4 :
  ∀ (x : C) (hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x),
    (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h_1 : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
y : C
h : y ∈ (↑s : Set C)
⊢ y * 1 = y

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h_1 : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
y : C
h : y ∈ (↑s : Set C)
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

Tactic:
exact ⟨y, h, 1, t.one_mem, by simp⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h_1 : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
y : C
h : y ∈ (↑t : Set C)
⊢ 1 * y = y

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h_1 : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
y : C
h : y ∈ (↑t : Set C)
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

Tactic:
exact ⟨1, s.one_mem, y, h, by simp⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = 1

Tactic:
⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩

Premises used: Subgroup.one_mem, And.intro, Exists.intro, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = 1

Tactic:
exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) (y₁ * z₁)
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
hy : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) (y₂ * z₂)
⊢ y₁ * y₂ * (z₁ * z₂) = y₁ * z₁ * (y₂ * z₂)

Tactic:
simp [mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) (y₁ * z₁)
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
hy : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) (y₂ * z₂)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = y₁ * z₁ * (y₂ * z₂)

Tactic:
exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
y : C
hy : y ∈ s
z : C
hz : z ∈ t
hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) (y * z)
⊢ ∃ y_1 ∈ s, ∃ z_1 ∈ t, y_1 * z_1 = (y * z)⁻¹

Tactic:
⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩

Premises used: Eq.rec, InvMemClass.inv_mem, And.intro, Exists.intro, mul_comm, mul_inv_rev, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
y : C
hy : y ∈ s
z : C
hz : z ∈ t
hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) (y * z)
⊢ ∃ y_1 ∈ s, ∃ z_1 ∈ t, y_1 * z_1 = (y * z)⁻¹

Tactic:
exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Tactic:
mul_mem_sup hy hz

Premises used: Subgroup.mul_mem_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Tactic:
exact mul_mem_sup hy hz

Premises used: Subgroup.mul_mem_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) ↔ ∃ (y : ↥s) (z : ↥t), (↑y : C) * (↑z : C) = x

Tactic:
simp only [SetLike.exists, exists_prop]

Premises used: exists_prop, SetLike.exists
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
P : C → Prop
⊢ (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
grind [mem_sup]

Premises used: Subgroup.mem_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
P : C → Prop
⊢ (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)

Tactic:
simp [mem_sup]

Premises used: Subgroup.mem_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
mp : x ∈ s ⊔ t → ∃ y ∈ s, ∃ z ∈ t, y * z = x
mpr : (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ s ⊔ t
⊢ Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x

Tactic:
rw [sup_eq_closure] at hx

Premises used: Subgroup.sup_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
closure_induction ?_ ?_ ?_ ?_ hx

Premises used: Subgroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
mp : ∀ (x : G) (hx : x ∈ (↑s : Set G) ∪ (↑t : Set G)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
mp₁ : ∃ y ∈ s, ∃ z ∈ t, y * z = 1
mp₂ :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x)
    (hy : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) y),
    (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y
mp₃ :
  ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x),
    (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
refine closure_induction ?_ ?_ ?_ ?_ hx
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x_1
x : G
hx : x ∈ (↑s : Set G)
⊢ x * 1 = x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x_1
x : G
hx : x ∈ (↑s : Set G)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
exact ⟨x, hx, 1, t.one_mem, by simp⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x_1
x : G
hx : x ∈ (↑t : Set G)
⊢ 1 * x = x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x_1
x : G
hx : x ∈ (↑t : Set G)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
exact ⟨1, s.one_mem, x, hx, by simp⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
⊢ HMul.hMul (α := G) 1 1 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = 1

Tactic:
exact ⟨1, s.one_mem, 1, t.one_mem, by simp⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
y₁ : G
hy₁ : y₁ ∈ s
z₁ : G
hz₁ : z₁ ∈ t
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) (y₁ * z₁)
y₂ : G
hy₂ : y₂ ∈ s
z₂ : G
hz₂ : z₂ ∈ t
hy : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) (y₂ * z₂)
⊢ y₁ * y₂ * (y₂⁻¹ * z₁ * y₂ * z₂) = y₁ * z₁ * (y₂ * z₂)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
y₁ : G
hy₁ : y₁ ∈ s
z₁ : G
hz₁ : z₁ ∈ t
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) (y₁ * z₁)
y₂ : G
hy₂ : y₂ ∈ s
z₂ : G
hz₂ : z₂ ∈ t
hy : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) (y₂ * z₂)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = y₁ * z₁ * (y₂ * z₂)

Tactic:
exact ⟨y₁ * y₂, s.mul_mem hy₁ hy₂,
            (y₂⁻¹ * z₁ * y₂) * z₂, t.mul_mem (ht.conj_mem' z₁ hz₁ y₂) hz₂, by simp [mul_assoc]⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
y : G
hy : y ∈ s
z : G
hz : z ∈ t
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) (y * z)
⊢ y⁻¹ * (y * z⁻¹ * y⁻¹) = (y * z)⁻¹

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
y : G
hy : y ∈ s
z : G
hz : z ∈ t
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) (y * z)
⊢ ∃ y_1 ∈ s, ∃ z_1 ∈ t, y_1 * z_1 = (y * z)⁻¹

Tactic:
exact ⟨y⁻¹, s.inv_mem hy,
            y * z⁻¹ * y⁻¹, ht.conj_mem z⁻¹ (t.inv_mem hz) y, by simp [mul_assoc]⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
y : G
hy : y ∈ s
z : G
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Tactic:
mul_mem_sup hy hz

Premises used: Subgroup.mul_mem_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
y : G
hy : y ∈ s
z : G
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Tactic:
exact mul_mem_sup hy hz

Premises used: Subgroup.mul_mem_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
hs : s.Normal
x : G
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x

Tactic:
have h := (sup_comm t s) ▸ mem_sup_of_normal_right (s := t) (t := s) (x := x)
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
hs : s.Normal
x : G
h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
h_1 : ∃ y ∈ t, ∃ z ∈ s, y * z = x
y : G
hy : y ∈ t
z : G
hz : z ∈ s
hp : y * z = x
⊢ y * z * y⁻¹ * y = x

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
hs : s.Normal
x : G
h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
h_1 : ∃ y ∈ s, ∃ z ∈ t, y * z = x
y : G
hy : y ∈ s
z : G
hz : z ∈ t
hp : y * z = x
⊢ z * (z⁻¹ * y * z) = x

Tactic:
simp [mul_assoc, hp]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
hs : s.Normal
x : G
h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
exact h.trans
    ⟨fun ⟨y, hy, z, hz, hp⟩ ↦ ⟨y * z * y⁻¹, hs.conj_mem z hz y, y, hy, by simp [hp]⟩,
    fun ⟨y, hy, z, hz, hp⟩ ↦ ⟨z, hz, z⁻¹ * y * z, hs.conj_mem' y hy z, by simp [mul_assoc, hp]⟩⟩

Premises used: Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
x y z : C
rw :
  (∃ (y_1 : C),
      Membership.mem (γ := Subgroup C) (closure {x}) y_1 ∧
        ∃ (z_1 : C), Membership.mem (γ := Subgroup C) (closure {y}) z_1 ∧ y_1 * z_1 = z) ↔
    ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z
⊢ Membership.mem (γ := Subgroup C) (closure {x, y}) z ↔ ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z

Tactic:
rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]

Premises used: Set.singleton_union, Subgroup.mem_sup, Subgroup.closure_union
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
C : Type u_2
inst : CommGroup C
x y z : C
simp_rw :
  (∃ (y_1 : C), (∃ (n : ℤ), x ^ n = y_1) ∧ ∃ (z_1 : C), (∃ (n : ℤ), y ^ n = z_1) ∧ y_1 * z_1 = z) ↔
    ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z
⊢ (∃ (y_1 : C),
      Membership.mem (γ := Subgroup C) (closure {x}) y_1 ∧
        ∃ (z_1 : C), Membership.mem (γ := Subgroup C) (closure {y}) z_1 ∧ y_1 * z_1 = z) ↔
    ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z

Tactic:
simp_rw [mem_closure_singleton, exists_exists_eq_and]

Premises used: Subgroup.mem_closure_singleton, exists_exists_eq_and
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ H₁ ⊓ H₂ ≤ ⊥ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1

Tactic:
simp only [SetLike.le_def, mem_inf, mem_bot, and_imp]

Premises used: and_imp, SetLike.le_def, Subgroup.mem_inf, Subgroup.mem_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1

Tactic:
disjoint_def.trans ⟨fun h _x _y hx hy hxy ↦ h hx <| hxy.symm ▸ hy, fun h _x hx hx' ↦ h hx hx' rfl⟩

Premises used: Eq.rec, Subgroup.disjoint_def, Iff.intro, Iff.trans, Eq.symm, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
hxy : x * y = 1
hx1 : x = 1 := ⋯
⊢ y = 1

Tactic:
simpa [hx1] using hxy
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy :
  Eq.{u_1 + 1} (α := G) ((fun (g : ↥H₁ × ↥H₂) ↦ (↑g.1 : G) * (↑g.2 : G)) x)
    ((fun (g : ↥H₁ × ↥H₂) ↦ (↑g.1 : G) * (↑g.2 : G)) y)
⊢ (↑y.1 : G)⁻¹ * (↑x.1 : G) * ((↑x.2 : G) * (↑y.2 : G)⁻¹) = 1

Tactic:
rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy

Premises used: mul_inv_eq_one, mul_assoc, inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) * ((↑x.2 : G) * (↑y.2 : G)⁻¹) = 1
⊢ (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1

Tactic:
replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy