awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s t : Set G
⊢ Eq (α := Subgroup G) (closure (s ∪ t)) (closure s ⊔ closure t)

Tactic:
(Subgroup.gi G).gc.l_sup

Premises used: Subgroup.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H H' : Subgroup G
simp_rw : H ⊔ H' = closure (↑H : Set G) ⊔ closure (↑H' : Set G)
⊢ H ⊔ H' = closure ((↑H : Set G) ∪ (↑H' : Set G))

Tactic:
simp_rw [closure_union, closure_eq]

Premises used: Subgroup.closure_eq, Subgroup.closure_union
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
s : ι → Set G
⊢ Eq.{u_1 + 1} (α := Subgroup G) (closure (⋃ (i : ι), s i)) (⨆ (i : ι), closure (s i))

Tactic:
(Subgroup.gi G).gc.l_iSup

Premises used: GaloisConnection.l_iSup, Subgroup.gi, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
⊢ Eq (α := Subgroup G) (closure k) ⊥ ↔ k ⊆ {1}

Tactic:
le_bot_iff.symm.trans <| closure_le _

Premises used: le_bot_iff, Subgroup.closure_le, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
p : ι → Subgroup G
simp_rw : Eq.{u_1 + 1} (α := Subgroup G) (⨆ (i : ι), p i) (⨆ (i : ι), closure (↑(p i) : Set G))
⊢ Eq.{u_1 + 1} (α := Subgroup G) (⨆ (i : ι), p i) (closure (⋃ (i : ι), (↑(p i) : Set G)))

Tactic:
simp_rw [closure_iUnion, closure_eq]

Premises used: Subgroup.closure_eq, Subgroup.closure_iUnion
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y : G
⊢ Membership.mem (γ := Subgroup G) (closure {x}) y ↔ ∃ (n : ℤ), x ^ n = y

Tactic:
⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
      hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩

Premises used: Set.mem_singleton, _private.0.Subgroup.mem_closure_singleton.match_1, Subgroup.closure, zpow_mem, Membership.mem, Eq.rec, Subgroup.subset_closure, Iff.intro, Subgroup.closure_induction, Singleton.singleton
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y : G
refine_1 :
  ∀ (hy : Membership.mem (γ := Subgroup G) (closure {x}) y) (x_1 : G) (hx : Membership.mem (γ := Set G) {x} x_1),
    ∃ (n : ℤ), x ^ n = x_1
refine_2 : ∀ (hy : Membership.mem (γ := Subgroup G) (closure {x}) y), ∃ (n : ℤ), x ^ n = 1
refine_3 :
  ∀ (hy : Membership.mem (γ := Subgroup G) (closure {x}) y) (x_1 y : G)
    (hx : Membership.mem (γ := Subgroup G) (closure {x}) x_1) (hy : Membership.mem (γ := Subgroup G) (closure {x}) y),
    (∃ (n : ℤ), x ^ n = x_1) → (∃ (n : ℤ), x ^ n = y) → ∃ (n : ℤ), x ^ n = x_1 * y
refine_4 :
  ∀ (hy : Membership.mem (γ := Subgroup G) (closure {x}) y) (x_1 : G)
    (hx : Membership.mem (γ := Subgroup G) (closure {x}) x_1), (∃ (n : ℤ), x ^ n = x_1) → ∃ (n : ℤ), x ^ n = x_1⁻¹
⊢ Membership.mem (γ := Subgroup G) (closure {x}) y ↔ ∃ (n : ℤ), x ^ n = y

Tactic:
refine
    ⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
      hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y_1 : G
hy_1 : Membership.mem (γ := Subgroup G) (closure {x}) y_1
y : G
hy : Membership.mem (γ := Set G) {x} y
refine_1 : ∃ (n : ℤ), x ^ n = x
⊢ ∃ (n : ℤ), x ^ n = y

Tactic:
rw [eq_of_mem_singleton hy]

Premises used: Set.eq_of_mem_singleton
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y_1 : G
hy_1 : Membership.mem (γ := Subgroup G) (closure {x}) y_1
y : G
hy : Membership.mem (γ := Set G) {x} y
⊢ ∃ (n : ℤ), x ^ n = x

Tactic:
⟨1, zpow_one x⟩

Premises used: zpow_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y_1 : G
hy_1 : Membership.mem (γ := Subgroup G) (closure {x}) y_1
y : G
hy : Membership.mem (γ := Set G) {x} y
⊢ ∃ (n : ℤ), x ^ n = x

Tactic:
exact ⟨1, zpow_one x⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y : G
hy : Membership.mem (γ := Subgroup G) (closure {x}) y
⊢ ∃ (n : ℤ), x ^ n = 1

Tactic:
⟨0, zpow_zero x⟩

Premises used: zpow_zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y : G
hy : Membership.mem (γ := Subgroup G) (closure {x}) y
⊢ ∃ (n : ℤ), x ^ n = 1

Tactic:
exact ⟨0, zpow_zero x⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y : G
hy : Membership.mem (γ := Subgroup G) (closure {x}) y
n : ℤ
hx : Membership.mem (γ := Subgroup G) (closure {x}) (x ^ n)
m : ℤ
hy_1 : Membership.mem (γ := Subgroup G) (closure {x}) (x ^ m)
⊢ ∃ (n_1 : ℤ), x ^ n_1 = x ^ n * x ^ m

Tactic:
⟨n + m, zpow_add x n m⟩

Premises used: zpow_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y : G
hy : Membership.mem (γ := Subgroup G) (closure {x}) y
n : ℤ
hx : Membership.mem (γ := Subgroup G) (closure {x}) (x ^ n)
m : ℤ
hy_1 : Membership.mem (γ := Subgroup G) (closure {x}) (x ^ m)
⊢ ∃ (n_1 : ℤ), x ^ n_1 = x ^ n * x ^ m

Tactic:
exact ⟨n + m, zpow_add x n m⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y : G
hy : Membership.mem (γ := Subgroup G) (closure {x}) y
n : ℤ
hx : Membership.mem (γ := Subgroup G) (closure {x}) (x ^ n)
⊢ ∃ (n_1 : ℤ), x ^ n_1 = (x ^ n)⁻¹

Tactic:
⟨-n, zpow_neg x n⟩

Premises used: zpow_neg, Exists.intro, Neg.neg
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x y : G
hy : Membership.mem (γ := Subgroup G) (closure {x}) y
n : ℤ
hx : Membership.mem (γ := Subgroup G) (closure {x}) (x ^ n)
⊢ ∃ (n_1 : ℤ), x ^ n_1 = (x ^ n)⁻¹

Tactic:
exact ⟨-n, zpow_neg x n⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (closure {1}) ⊥

Tactic:
simp [eq_bot_iff_forall, mem_closure_singleton]

Premises used: Subgroup.mem_closure_singleton, Subgroup.eq_bot_iff_forall
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x : G
⊢ Membership.mem (γ := Subgroup G) (closure {x}) x

Tactic:
simpa [-subset_closure] using subset_closure (k := {x})

Premises used: Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S : Set G
⊢ LE.le (α := Submonoid G) (Submonoid.closure S) (toSubmonoid (closure S))

Tactic:
Submonoid.closure_le.2 subset_closure

Premises used: Iff.mpr, Subgroup.subset_closure, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S : Set G
h : Eq (α := Submonoid G) (Submonoid.closure S) ⊤
⊢ Eq (α := Subgroup G) (closure S) ⊤

Tactic:
(eq_top_iff' _).2 fun _ => le_closure_toSubmonoid _ <| h.symm ▸ trivial

Premises used: Iff.mpr, trivial, Eq.rec, Subgroup.le_closure_toSubmonoid, Subgroup.eq_top_iff', Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s : Set G
rw : Eq (α := Subgroup G) (closure {1} ⊔ closure s) (closure s)
⊢ Eq (α := Subgroup G) (closure (insert 1 s)) (closure s)

Tactic:
rw [insert_eq, closure_union]

Premises used: Set.insert_eq, Subgroup.closure_union
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ Eq (α := Subgroup G) (closure {1} ⊔ closure s) (closure s)

Tactic:
simp [one_mem]

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s : Set G
rw : Eq (α := Subgroup G) (closure (insert 1 s)) (closure s)
rw₁ rw₂ : Eq (α := Subgroup G) (closure s) (closure s)
⊢ Eq (α := Subgroup G) (closure (s ∪ {1})) (closure s)

Tactic:
rw [union_singleton, closure_insert_one]

Premises used: Subgroup.closure_insert_one, Set.union_singleton
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s : Set G
rw : Eq (α := Subgroup G) (closure (s \ {1} ∪ {1})) (closure s)
rw₁ : Eq (α := Subgroup G) (closure (s ∪ {1})) (closure s)
rw₂ rw₃ : Eq (α := Subgroup G) (closure s) (closure s)
⊢ Eq (α := Subgroup G) (closure (s \ {1})) (closure s)

Tactic:
rw [← closure_union_one (s \ {1}), diff_union_self, closure_union_one]

Premises used: Set.diff_union_self, SDiff.sdiff, Singleton.singleton, OfNat.ofNat, Subgroup.closure_union_one
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S : Set G
⊢ Eq (α := AddSubgroup (Additive G))
    ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) (closure S) : AddSubgroup (Additive G))
    (AddSubgroup.closure ((⇑Additive.toMul : (a : Additive G) → G) ⁻¹' S) : AddSubgroup (Additive G))

Tactic:
le_antisymm (toAddSubgroup.le_symm_apply.mp <|
      (closure_le _).mpr (AddSubgroup.subset_closure (G := Additive G)))
    ((AddSubgroup.closure_le _).mpr (subset_closure (G := G)))

Premises used: Iff.mpr, Subgroup.toAddSubgroup, Subgroup.closure_le, Subgroup.subset_closure, le_antisymm, OrderIso.le_symm_apply, Iff.mp, AddSubgroup.closure_le, AddSubgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
A : Type u_2
inst : AddGroup A
S : Set A
⊢ Eq (α := Subgroup (Multiplicative A))
    ((AddSubgroup.toSubgroup : (a : AddSubgroup A) → Subgroup (Multiplicative A)) (AddSubgroup.closure S) :
      Subgroup (Multiplicative A))
    (closure ((⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' S) : Subgroup (Multiplicative A))

Tactic:
Subgroup.toAddSubgroup.injective (Subgroup.toAddSubgroup_closure _).symm

Premises used: Subgroup.toAddSubgroup, Subgroup.toAddSubgroup_closure, OrderIso.injective, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
A : Type u_2
inst : AddGroup A
S : Set (Multiplicative A)
⊢ Eq (α := AddSubgroup A)
    ((toAddSubgroup' : (a : Subgroup (Multiplicative A)) → AddSubgroup A) (closure S) : AddSubgroup A)
    (AddSubgroup.closure ((⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' S) : AddSubgroup A)

Tactic:
le_antisymm (toAddSubgroup'.to_galoisConnection.l_le <|
      (closure_le _).mpr <| AddSubgroup.subset_closure (G := A))
    ((AddSubgroup.closure_le _).mpr <| Subgroup.subset_closure (G := Multiplicative A))

Premises used: Iff.mpr, Subgroup.toAddSubgroup', OrderIso.to_galoisConnection, Subgroup.closure_le, GaloisConnection.l_le, Subgroup.subset_closure, le_antisymm, AddSubgroup.closure_le, AddSubgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S : Set (Additive G)
⊢ Eq (α := Subgroup G)
    ((AddSubgroup.toSubgroup' : (a : AddSubgroup (Additive G)) → Subgroup G) (AddSubgroup.closure S) : Subgroup G)
    (closure ((⇑Additive.ofMul : (a : G) → Additive G) ⁻¹' S) : Subgroup G)

Tactic:
congr_arg AddSubgroup.toSubgroup' (toAddSubgroup'_closure _).symm

Premises used: iInf, Subgroup.closure, Submonoid.copy, Set.Mem, Set.iInter, Additive, setOf, congr_arg, Multiplicative, Set.preimage, AddSubgroup.toSubgroup', Subgroup.toAddSubgroup'_closure, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
⊢ Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x ↔ ∃ (i : ι), p i ∧ x ∈ K i

Tactic:
⟨?_, fun ⟨i, hi', hi⟩ ↦ ?_⟩

Premises used: iSup, Membership.mem, _private.0.Subgroup.mem_biSup_of_directedOn.match_1, Iff.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
refine_1 : Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x → ∃ (i : ι), p i ∧ x ∈ K i
refine_2 :
  (∃ (i : ι), p i ∧ x ∈ K i) →
    ∀ (i : ι) (hi' : p i) (hi : x ∈ K i), Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x
⊢ Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x ↔ ∃ (i : ι), p i ∧ x ∈ K i

Tactic:
refine ⟨?_, fun ⟨i, hi', hi⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
this :
  Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i
⊢ Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x → ∃ (i : ι), p i ∧ x ∈ K i

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

Premises used: Subgroup.closure_eq, Subgroup.closure_iUnion
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
refine_1 :
  Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i
⊢ Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x → ∃ (i : ι), p i ∧ x ∈ K i

Tactic:
suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set G)) → ∃ i, p i ∧ x ∈ K i by
      simpa only [closure_iUnion, closure_eq (K _)] using this
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
⊢ Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i

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

Premises used: Subgroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
refine_1 :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x : G)
    (hx : Membership.mem (γ := Set G) (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G)) x), ∃ (i : ι), p i ∧ x ∈ K i
refine_1₁ :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x),
    ∃ (i : ι), p i ∧ 1 ∈ K i
refine_1₂ :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x y : G)
    (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x)
    (hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) y),
    (∃ (i : ι), p i ∧ x ∈ K i) → (∃ (i : ι), p i ∧ y ∈ K i) → ∃ (i : ι), p i ∧ x * y ∈ K i
refine_1₃ :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x : G)
    (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x),
    (∃ (i : ι), p i ∧ x ∈ K i) → ∃ (i : ι), p i ∧ x⁻¹ ∈ K i
⊢ Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i

Tactic:
refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
x_1 : G
⊢ ∀ (hx : Membership.mem (γ := Set G) (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G)) x_1), ∃ (i : ι), p i ∧ x_1 ∈ K i

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
⊢ ∃ (i : ι), p i ∧ 1 ∈ K i

Tactic:
⟨i, hp, (K i).one_mem⟩

Premises used: Subgroup.one_mem, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
⊢ ∃ (i : ι), p i ∧ 1 ∈ K i

Tactic:
exact ⟨i, hp, (K i).one_mem⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x_1 : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x_1
x y : G
hx_1 : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) y
i : ι
hip : p i
hi : x ∈ K i
j : ι
hjp : p j
hj : y ∈ K j
refine_1 :
  ∀ (k : ι) (hk : Membership.mem (γ := Set ι) {i : ι | p i} k) (hki : ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) i k)
    (hkj : ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) j k), ∃ (i : ι), p i ∧ x * y ∈ K i
⊢ ∃ (i : ι), p i ∧ x * y ∈ K i

Tactic:
rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x_1 : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x_1
x y : G
hx_1 : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) y
i : ι
hip : p i
hi : x ∈ K i
j : ι
hjp : p j
hj : y ∈ K j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | p i} k
hki : ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) i k
hkj : ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) j k
⊢ ∃ (i : ι), p i ∧ x * y ∈ K i

Tactic:
⟨k, hk, mul_mem (hki hi) (hkj hj)⟩

Premises used: And.intro, Exists.intro, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x_1 : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x_1
x y : G
hx_1 : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) y
i : ι
hip : p i
hi : x ∈ K i
j : ι
hjp : p j
hj : y ∈ K j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | p i} k
hki : ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) i k
hkj : ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) j k
⊢ ∃ (i : ι), p i ∧ x * y ∈ K i

Tactic:
exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x_1
i : ι
hi' : p i
hi : x_1 ∈ K i
⊢ ∃ (i : ι), p i ∧ x_1⁻¹ ∈ K i

Tactic:
⟨i, hi', inv_mem hi⟩

Premises used: InvMemClass.inv_mem, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x_1
i : ι
hi' : p i
hi : x_1 ∈ K i
⊢ ∃ (i : ι), p i ∧ x_1⁻¹ ∈ K i

Tactic:
exact ⟨i, hi', inv_mem hi⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
h : ∃ (i : ι), p i ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
refine_2 : Membership.mem (γ := Subgroup G) (⨆ (_ : p i), K i) x
⊢ Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x

Tactic:
apply le_iSup (fun i ↦ ⨆ (_ : p i), K i) i

Premises used: iSup, le_iSup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
h : ∃ (i : ι), p i ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ Membership.mem (γ := Subgroup G) (⨆ (_ : p i), K i) x

Tactic:
simp [hi, hi']
-- 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
⊢ iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down

Tactic:
simp [iSup_plift_down]

Premises used: iSup_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
⊢ iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down

Tactic:
have : iSup K = ⨆ i : PLift ι, ⨆ (_ : True), K i.down := by simp [iSup_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
rw : (∃ (i : PLift ι), True ∧ x ∈ K i.down) ↔ ∃ (i : ι), x ∈ K i
hK₁ :
  DirectedOn.{u_2} (α := PLift ι) ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on fun (i : PLift ι) ↦ K i.down)
    {i : PLift ι | True}
rw₁ : PLift ι
⊢ x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i

Tactic:
rw [this, mem_biSup_of_directedOn trivial]

Premises used: Subgroup.mem_biSup_of_directedOn
-- 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 : PLift ι), True ∧ x ∈ K i.down) ↔ ∃ (i : ι), x ∈ K i

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
hK₁ : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) fun (i : PLift ι) ↦ K i.down
⊢ DirectedOn.{u_2} (α := PLift ι) ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on fun (i : PLift ι) ↦ K i.down) univ

Tactic:
rw [directedOn_onFun_iff, Set.image_univ, directedOn_range]

Premises used: Set.image_univ, directedOn_range, directedOn_onFun_iff
-- 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 : PLift ι
hK₁ : ∀ (y : PLift ι), ∃ (x : ι), K i.down ≤ K x ∧ K y.down ≤ K x
⊢ ∀ (y : PLift ι),
    ∃ (z : PLift ι),
      (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) ((fun (i : PLift ι) ↦ K i.down) i) ((fun (i : PLift ι) ↦ K i.down) z) ∧
        (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) ((fun (i : PLift ι) ↦ K i.down) y) ((fun (i : PLift ι) ↦ K i.down) z)

Tactic:
simp only [PLift.exists]

Premises used: PLift.exists
-- 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 ι
⊢ ∃ (x : ι), K i.down ≤ K x ∧ K j.down ≤ K x

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

Premises used: Exists.imp, PLift.down