awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
toAddSubmonoid : AddSubmonoid (Additive G)
neg_mem' : ∀ {x : Additive G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier
⊢ (fun (S : Subgroup G) ↦
        let __src : AddSubmonoid (Additive G) :=
          (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
        ({ toAddSubmonoid := __src, neg_mem' := ⋯ } : AddSubgroup (Additive G)))
      ((fun (S : AddSubgroup (Additive G)) ↦
          let __src : Submonoid (Multiplicative (Additive G)) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
              S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ : Subgroup G })
        { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' }) =
    { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' : AddSubgroup (Additive G) }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S : Subgroup G
g : Additive G
⊢ Membership.mem (γ := AddSubgroup (Additive G))
      ((Subgroup.toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) S : AddSubgroup (Additive G)) g ↔
    Membership.mem (α := G) S ((toMul : (a : Additive G) → G) g : G)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S : AddSubgroup (Additive G)
g : G
⊢ Membership.mem (γ := Subgroup G) ((toSubgroup' : (a : AddSubgroup (Additive G)) → Subgroup G) S : Subgroup G) g ↔
    Membership.mem (α := Additive G) S ((Additive.ofMul : (a : G) → Additive G) g : Additive G)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
x : AddSubgroup A
mk :
  ∀ (toAddSubmonoid : AddSubmonoid A) (neg_mem' : ∀ {x : A}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier),
    (fun (S : Subgroup (Multiplicative A)) ↦
          let __src : AddSubmonoid (Additive (Multiplicative A)) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
              S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ : AddSubgroup A })
        ((fun (S : AddSubgroup A) ↦
            let __src : Submonoid (Multiplicative A) :=
              (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
            ({ toSubmonoid := __src, inv_mem' := ⋯ } : Subgroup (Multiplicative A)))
          { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' }) =
      { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' : AddSubgroup A }
⊢ (fun (S : Subgroup (Multiplicative A)) ↦
        let __src : AddSubmonoid (Additive (Multiplicative A)) :=
          (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
            S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ : AddSubgroup A })
      ((fun (S : AddSubgroup A) ↦
          let __src : Submonoid (Multiplicative A) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
          ({ toSubmonoid := __src, inv_mem' := ⋯ } : Subgroup (Multiplicative A)))
        x) =
    x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
toAddSubmonoid : AddSubmonoid A
neg_mem' : ∀ {x : A}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier
⊢ (fun (S : Subgroup (Multiplicative A)) ↦
        let __src : AddSubmonoid (Additive (Multiplicative A)) :=
          (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
            S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ : AddSubgroup A })
      ((fun (S : AddSubgroup A) ↦
          let __src : Submonoid (Multiplicative A) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
          ({ toSubmonoid := __src, inv_mem' := ⋯ } : Subgroup (Multiplicative A)))
        { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' }) =
    { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' : AddSubgroup A }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
x : Subgroup (Multiplicative A)
mk :
  ∀ (toSubmonoid : Submonoid (Multiplicative A))
    (inv_mem' : ∀ {x : Multiplicative A}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier),
    (fun (S : AddSubgroup A) ↦
          let __src : Submonoid (Multiplicative A) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
          ({ toSubmonoid := __src, inv_mem' := ⋯ } : Subgroup (Multiplicative A)))
        ((fun (S : Subgroup (Multiplicative A)) ↦
            let __src : AddSubmonoid (Additive (Multiplicative A)) :=
              (Submonoid.toAddSubmonoid :
                  (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
                S.toSubmonoid;
            { toAddSubmonoid := __src, neg_mem' := ⋯ : AddSubgroup A })
          { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' }) =
      { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' : Subgroup (Multiplicative A) }
⊢ (fun (S : AddSubgroup A) ↦
        let __src : Submonoid (Multiplicative A) :=
          (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
        ({ toSubmonoid := __src, inv_mem' := ⋯ } : Subgroup (Multiplicative A)))
      ((fun (S : Subgroup (Multiplicative A)) ↦
          let __src : AddSubmonoid (Additive (Multiplicative A)) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
              S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ : AddSubgroup A })
        x) =
    x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
toSubmonoid : Submonoid (Multiplicative A)
inv_mem' : ∀ {x : Multiplicative A}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier
⊢ (fun (S : AddSubgroup A) ↦
        let __src : Submonoid (Multiplicative A) :=
          (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
        ({ toSubmonoid := __src, inv_mem' := ⋯ } : Subgroup (Multiplicative A)))
      ((fun (S : Subgroup (Multiplicative A)) ↦
          let __src : AddSubmonoid (Additive (Multiplicative A)) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
              S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ : AddSubgroup A })
        { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' }) =
    { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' : Subgroup (Multiplicative A) }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
A : Type u_2
inst : AddGroup A
S : AddSubgroup A
a : Multiplicative A
⊢ Membership.mem (γ := Subgroup (Multiplicative A))
      ((AddSubgroup.toSubgroup : (a : AddSubgroup A) → Subgroup (Multiplicative A)) S : Subgroup (Multiplicative A)) a ↔
    Membership.mem (α := A) S ((toAdd : (a : Multiplicative A) → A) a : A)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
A : Type u_2
inst : AddGroup A
S : Subgroup (Multiplicative A)
a : A
⊢ Membership.mem (γ := AddSubgroup A)
      ((toAddSubgroup' : (a : Subgroup (Multiplicative A)) → AddSubgroup A) S : AddSubgroup A) a ↔
    Membership.mem (α := Multiplicative A) S ((Multiplicative.ofAdd : (a : A) → Multiplicative A) a : Multiplicative A)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ ∀ {x : G},
    Membership.mem (γ := Set G) (Subsemigroup.carrier (Submonoid.toSubsemigroup ⊥)) x →
      Membership.mem (γ := Set G) (Subsemigroup.carrier (Submonoid.toSubsemigroup ⊥)) x⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x : G
⊢ Membership.mem (γ := Subgroup G) ⊥ x ↔ x = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
x : G
⊢ Membership.mem (γ := Subgroup G) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
⊢ (↑⊤ : Set G) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
⊢ (↑⊥ : Set G) = {1}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
⊢ Eq.{u_1 + 1} (α := Submonoid G) (toSubmonoid ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
⊢ Eq.{u_1 + 1} (α := Submonoid G) (toSubmonoid ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H = ⊥ ↔ ∀ x ∈ H, x = 1

Tactic:
toSubmonoid_injective.eq_iff.symm.trans <| Submonoid.eq_bot_iff_forall _

Premises used: Submonoid.eq_bot_iff_forall, Function.Injective.eq_iff, Iff.trans, Subgroup.toSubmonoid_injective, Iff.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Subsingleton.{u_1 + 1} ↥H
rw : ∀ x ∈ H, x = 1
⊢ H = ⊥

Tactic:
rw [Subgroup.eq_bot_iff_forall]

Premises used: Subgroup.eq_bot_iff_forall
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Subsingleton.{u_1 + 1} ↥H
y : G
hy : y ∈ H
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) y hy) : G) = 1
rw₁ : Eq.{u_1 + 1} (α := G) (↑1 : G) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := G) 1 1
⊢ y = 1

Tactic:
rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]

Premises used: Subgroup.coe_mk, Subtype.mk, Subgroup.coe_one, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (↑H : Set G) = (↑⊤ : Set G) ↔ (↑H : Set G) = Set.univ

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : ∃ (g : G), (↑H : Set G) = {g}
g : G
hg : (↑H : Set G) = {g}
rw : Subsingleton.{u_1 + 1} (↑{g} : Type u_1)
⊢ Subsingleton.{u_1 + 1} (↑(↑H : Set G) : Type u_1)

Tactic:
rw [hg]
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : ∃ (g : G), (↑H : Set G) = {g}
g : G
hg : (↑H : Set G) = {g}
⊢ Subsingleton.{u_1 + 1} (↑{g} : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (∃ (y : G) (_ : y ∈ H), y ≠ (↑1 : G)) ↔ ∃ x ∈ H, x ≠ 1
⊢ Nontrivial.{u_1} ↥H ↔ ∃ x ∈ H, x ≠ 1

Tactic:
rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]

Premises used: Subtype.nontrivial_iff_exists_ne, Membership.mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (∃ (y : G) (_ : y ∈ H), y ≠ (↑1 : G)) ↔ ∃ x ∈ H, x ≠ 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 rwa rwa₁ rwa₂ rwa₃ : Nontrivial.{u_1} ↥H
⊢ ∃ x ∈ H, x ≠ 1

Tactic:
rwa [← Subgroup.nontrivial_iff_exists_ne_one]

Premises used: Subgroup.nontrivial_iff_exists_ne_one
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1
⊢ Nontrivial.{u_1} ↥H ↔ H ≠ ⊥

Tactic:
rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]

Premises used: Subgroup.nontrivial_iff_exists_ne_one, ne_eq, Subgroup.eq_bot_iff_forall
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1

Tactic:
simp only [ne_eq, not_forall, exists_prop]

Premises used: exists_prop, ne_eq, Classical.not_forall
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Nontrivial.{u_1} ↥H ↔ H ≠ ⊥

Tactic:
have := nontrivial_iff_ne_bot H
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
this : Nontrivial.{u_1} ↥H ↔ H ≠ ⊥
inl : Nontrivial.{u_1} ↥H → H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inr : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inl₁ : Nontrivial.{u_1} ↥H → H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inr₁ : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inl₂ : Nontrivial.{u_1} ↥H → H ≠ ⊥ → ¬H = ⊥ → Nontrivial.{u_1} ↥H
inr₂ : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → ¬H = ⊥ → Nontrivial.{u_1} ↥H
inr₃ : ¬Nontrivial.{u_1} ↥H → H = ⊥ → ¬H = ⊥ → Nontrivial.{u_1} ↥H
⊢ H = ⊥ ∨ Nontrivial.{u_1} ↥H

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H = ⊥ ∨ Nontrivial.{u_1} ↥H

Tactic:
H.bot_or_nontrivial

Premises used: Subgroup.bot_or_nontrivial
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : (∃ x ∈ H, x ≠ 1) ↔ Nontrivial.{u_1} ↥H
⊢ H = ⊥ ∨ ∃ x ∈ H, x ≠ 1

Tactic:
convert! H.bot_or_nontrivial

Premises used: Subgroup.bot_or_nontrivial
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h h₁ : (∃ x ∈ H, x ≠ 1) ↔ ∃ x ∈ H, x ≠ 1
⊢ (∃ x ∈ H, x ≠ 1) ↔ Nontrivial.{u_1} ↥H

Tactic:
rw [nontrivial_iff_exists_ne_one]

Premises used: Subgroup.nontrivial_iff_exists_ne_one
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (∃ x ∈ H, x ≠ 1) ↔ ∃ (a : ↥H), a ≠ 1
⊢ H ≠ ⊥ ↔ ∃ (a : ↥H), a ≠ 1

Tactic:
rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]

Premises used: Subgroup.nontrivial_iff_exists_ne_one, Subgroup.nontrivial_iff_ne_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ∃ (a : ↥H), a ≠ 1

Tactic:
simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]

Premises used: Subtype.exists, exists_prop, ne_eq, Subgroup.mk_eq_one
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
p p' : Subgroup G
⊢ (↑(p ⊓ p') : Set G) = (↑p : Set G) ∩ (↑p' : Set G)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
p p' : Subgroup G
x : G
⊢ x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
s : Set (Subgroup G)
⊢ ⋂ S ∈ s, (↑S : Set G) = (↑(⨅ S ∈ s, S.toSubmonoid) : Set G)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
s : Set (Subgroup G)
x : G
hx : x ∈ (Submonoid.copy (⨅ S ∈ s, S.toSubmonoid) (⋂ S ∈ s, (↑S : Set G)) ⋯).carrier
i : Subgroup G
h : i ∈ s
⊢ x ∈ i

Tactic:
apply Set.mem_iInter₂.1 hx i h

Premises used: Set.mem_iInter₂, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Set (Subgroup G)
⊢ (↑(sInf H) : Set G) = ⋂ s ∈ H, (↑s : Set G)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S : Set (Subgroup G)
x : G
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
S : ι → Subgroup G
x : G
⊢ Membership.mem (γ := Subgroup G) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, Subgroup.mem_sInf
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
S : ι → Subgroup G
⊢ (↑(⨅ (i : ι), S i) : Set G) = ⋂ (i : ι), (↑(S i) : Set G)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Premises used: iInf, Set.biInter_range, Subgroup.coe_sInf
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S T : Subgroup G
x : G
⊢ x ∈ S → x ∈ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left; fun h ↦ this h

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S T : Subgroup G
x : G
⊢ x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right; fun h ↦ this h

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S T : Subgroup G
x y : G
hx : x ∈ S
hy : y ∈ T
⊢ x * y ∈ S ⊔ T

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

Premises used: Subgroup.mem_sup_left, Max.max, Subgroup.mul_mem, Subgroup.mem_sup_right
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
S : ι → Subgroup G
i : ι
x : G
⊢ x ∈ S i → x ∈ iSup S

Tactic:
have : S i ≤ iSup S := le_iSup _ _; fun h ↦ this h

Premises used: le_iSup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
S : Set (Subgroup G)
s : Subgroup G
hs : s ∈ S
x : G
⊢ x ∈ s → x ∈ sSup S

Tactic:
have : s ≤ sSup S := le_sSup hs; fun h ↦ this h

Premises used: le_sSup
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
h : Subsingleton G
x y : Subgroup G
i : G
⊢ 1 ∈ x ↔ 1 ∈ y

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
⊢ Nontrivial.{u_1} (Subgroup G) ↔ Nontrivial G

Tactic:
not_iff_not.mp
    ((not_nontrivial_iff_subsingleton.trans subsingleton_iff).trans
      not_nontrivial_iff_subsingleton.symm)

Premises used: not_iff_not, not_nontrivial_iff_subsingleton, Subgroup.subsingleton_iff, Iff.mp, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Nontrivial G
⊢ Nontrivial.{u_1} (Subgroup G)

Tactic:
nontrivial_iff.mpr ‹_›

Premises used: Iff.mpr, Subgroup.nontrivial_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Nontrivial G
rw : Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊥
⊢ Nontrivial.{u_1} ↥⊤

Tactic:
rw [nontrivial_iff_ne_bot]

Premises used: Subgroup.nontrivial_iff_ne_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Nontrivial G
⊢ Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊥

Tactic:
top_ne_bot

Premises used: top_ne_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Nontrivial G
⊢ Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊥

Tactic:
exact top_ne_bot

Premises used: top_ne_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H = ⊤ ↔ ∀ (x : G), x ∈ H

Tactic:
eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩

Premises used: eq_top_iff, Iff.intro, Subgroup.mem_top, Iff.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
x : G
⊢ Membership.mem (γ := Subgroup G) (closure k) x ↔ ∀ (K : Subgroup G), k ⊆ (↑K : Set G) → x ∈ K

Tactic:
mem_sInf

Premises used: Set.Mem, setOf, Subgroup.mem_sInf
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
⊢ k ⊆ (↑(closure k) : Set G)

Tactic:
fun _ hx => mem_closure.2 fun _ hK => hK hx

Premises used: Iff.mpr, Set.Subset, Subgroup.mem_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
hx : x ∈ s
⊢ Membership.mem (γ := Subgroup G) (closure s) x

Tactic:
subset_closure hx

Premises used: Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
P : G
hP : P ∉ closure k
⊢ P ∉ k

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: Subgroup.subset_closure, Not
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
k : Set G
⊢ closure k ≤ K ↔ k ⊆ (↑K : Set G)

Tactic:
⟨Subset.trans subset_closure, fun h => sInf_le h⟩

Premises used: Set.Subset.trans, Subgroup.subset_closure, sInf_le, Iff.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
k : Set G
h₁ : k ⊆ (↑K : Set G)
h₂ : K ≤ closure k
⊢ closure k = K

Tactic:
le_antisymm ((closure_le <| K).2 h₁) h₂

Premises used: Iff.mpr, Subgroup.closure_le, le_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (g : G) → Membership.mem (γ := Subgroup G) (closure k) g → Prop
mem : ∀ (x : G) (hx : x ∈ k), p x ⋯
one : p 1 ⋯
mul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x hx → p y hy → p (x * y) ⋯
inv : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x hx → p x⁻¹ ⋯
x : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
⊢ p x hx

Tactic:
let K : Subgroup G :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, ha⟩ ⟨_, hb⟩ ↦ ⟨_, mul _ _ _ _ ha hb⟩
      one_mem' := ⟨_, one⟩
      inv_mem' := fun ⟨_, hb⟩ ↦ ⟨_, inv _ _ hb⟩ }
  closure_le (K := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, HMul.hMul, Subgroup.closure, Subsemigroup.mk, setOf, Subgroup.closure_le, Membership.mem, Exists, Subgroup.mk, id, InvMemClass.inv_mem, Subgroup.subset_closure, Inv.inv, Exists.intro, Submonoid.mk, OneMemClass.one_mem, _private.0.Subgroup.closure_induction.match_1, Exists.elim, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x_1 : G
h : x_1 ∈ k
⊢ p x_1 z ⋯ ⋯

Tactic:
mem _ _ h hz