awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S₁ S₂ : Subgroup G
⊢ (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Subgroup.op, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S₁ S₂ : Subgroup Gᵐᵒᵖ
⊢ (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, Subgroup.unop, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S : Set (Subgroup G)
⊢ (sSup S).op = sSup (Subgroup.unop ⁻¹' S)

Tactic:
opEquiv.map_sSup_eq_sSup_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sSup_eq_sSup_symm_preimage, Subgroup.op, Subgroup.opEquiv, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S : Set (Subgroup Gᵐᵒᵖ)
⊢ (sSup S).unop = sSup (Subgroup.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sSup_eq_sSup_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sSup_eq_sSup_symm_preimage, OrderIso.symm, Subgroup.op, Subgroup.opEquiv, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S : Set (Subgroup G)
⊢ (sInf S).op = sInf (Subgroup.unop ⁻¹' S)

Tactic:
opEquiv.map_sInf_eq_sInf_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, Subgroup.op, Subgroup.opEquiv, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S : Set (Subgroup Gᵐᵒᵖ)
⊢ (sInf S).unop = sInf (Subgroup.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, OrderIso.symm, Subgroup.op, Subgroup.opEquiv, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
ι : Sort u_1
G : Type u_2
inst : Group G
S : ι → Subgroup G
⊢ (iSup S).op = ⨆ (i : ι), (S i).op

Tactic:
opEquiv.map_iSup _

Premises used: Set.Mem, OrderIso.map_iSup, Subgroup.op, Subgroup.opEquiv
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
ι : Sort u_1
G : Type u_2
inst : Group G
S : ι → Subgroup Gᵐᵒᵖ
⊢ (iSup S).unop = ⨆ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iSup _

Premises used: Set.Mem, OrderIso.map_iSup, OrderIso.symm, Subgroup.opEquiv, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
ι : Sort u_1
G : Type u_2
inst : Group G
S : ι → Subgroup G
⊢ (iInf S).op = ⨅ (i : ι), (S i).op

Tactic:
opEquiv.map_iInf _

Premises used: Set.Mem, OrderIso.map_iInf, Subgroup.op, Subgroup.opEquiv
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
ι : Sort u_1
G : Type u_2
inst : Group G
S : ι → Subgroup Gᵐᵒᵖ
⊢ (iInf S).unop = ⨅ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iInf _

Premises used: Set.Mem, OrderIso.map_iInf, OrderIso.symm, Subgroup.opEquiv, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
s : Set G
simp_rw :
  Eq.{u_2 + 1} (α := Subgroup Gᵐᵒᵖ) (sInf {a : Subgroup Gᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Gᵐᵒᵖ)})
    (sInf {K : Subgroup Gᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑K : Set Gᵐᵒᵖ)})
⊢ Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))

Tactic:
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Subgroup.coe_unop]

Premises used: Subgroup.closure, Set.preimage_setOf_eq, Subgroup.op_sInf, Subgroup.coe_unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
s : Set G
e_a : ∀ (a : Subgroup Gᵐᵒᵖ), s ⊆ MulOpposite.op ⁻¹' (↑a : Set Gᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Gᵐᵒᵖ)
⊢ Eq.{u_2 + 1} (α := Subgroup Gᵐᵒᵖ) (sInf {a : Subgroup Gᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Gᵐᵒᵖ)})
    (sInf {K : Subgroup Gᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑K : Set Gᵐᵒᵖ)})

Tactic:
congr with a
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
s : Set G
a : Subgroup Gᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' (↑a : Set Gᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Gᵐᵒᵖ)

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.Subset, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
s : Set G
a : Subgroup Gᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' (↑a : Set Gᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Gᵐᵒᵖ)

Tactic:
exact MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, MulOpposite.unop_surjective
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
s : Set Gᵐᵒᵖ
rw : Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
⊢ Eq (α := Subgroup G) (Subgroup.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))

Tactic:
rw [← op_inj, op_unop, op_closure]

Premises used: Subgroup.op_closure, Subgroup.op_unop, Subgroup.op_inj
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
s : Set Gᵐᵒᵖ
simp_rw : Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure ((fun (x : Gᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
simp_rw₁ : Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure ((fun (x : Gᵐᵒᵖ) ↦ x) ⁻¹' s))
⊢ Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Premises used: Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id'
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
ι : Sort u_1
G : Type u_2
inst : Group G
H : Subgroup G
inst_1 : Countable.{u_2 + 1} ↥H
⊢ Countable.{u_2 + 1} ↥H.op

Tactic:
Countable.of_equiv H H.equivOp

Premises used: Countable.of_equiv, Membership.mem, Subgroup.equivOp, Subtype
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x g : G
h : ↥H.op
⊢ h • (g * x) = g * h • x

Tactic:
mul_assoc _ _ _

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
⊢ H.op.Normal ↔ H.Normal

Tactic:
simp only [← normalizer_eq_top_iff, ← op_normalizer, op_eq_top]

Premises used: Subgroup.op_normalizer, Subgroup.op_eq_top, Subgroup.normalizer_eq_top_iff
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
ι : Sort u_1
G : Type u_2
inst : Group G
H : Subgroup G
inst_1 : H.Normal
⊢ H.op.Normal

Tactic:
.op ‹_›

Premises used: Subgroup.Normal.op
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
rw : H.unop.op.Normal ↔ H.Normal
rw₁ rw₂ : H.Normal ↔ H.Normal
⊢ H.unop.Normal ↔ H.Normal

Tactic:
rw [← normal_op, op_unop]

Premises used: Subgroup.normal_op, Subgroup.op_unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
ι : Sort u_1
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
inst_1 : H.Normal
⊢ H.unop.Normal

Tactic:
.unop ‹_›

Premises used: Subgroup.Normal.unop
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
S : Type u_1
G : Type u_2
inst : Group G
inst_1 : LinearOrder G
x_1 : SetLike S G
inst_2 : InvMemClass S G
H : S
x : G
inl : |x|ₘ = x → (|x|ₘ ∈ H ↔ x ∈ H)
inr : |x|ₘ = x⁻¹ → (|x|ₘ ∈ H ↔ x ∈ H)
⊢ |x|ₘ ∈ H ↔ x ∈ H

Tactic:
cases mabs_choice x

Premises used: mabs_choice
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
S : Type u_1
G : Type u_2
inst : Group G
inst_1 : LinearOrder G
x_1 : SetLike S G
inst_2 : InvMemClass S G
H : S
x : G
h : |x|ₘ = x
⊢ |x|ₘ ∈ H ↔ x ∈ H

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
S : Type u_1
G : Type u_2
inst : Group G
inst_1 : LinearOrder G
x_1 : SetLike S G
inst_2 : InvMemClass S G
H : S
x : G
h : |x|ₘ = x⁻¹
⊢ |x|ₘ ∈ H ↔ x ∈ H

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
C : Type u_1
inst : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : a ∈ (x ⊔ y) ⊓ z
⊢ (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z

Tactic:
rw [mem_inf, mem_sup] at ha

Premises used: Subgroup.mem_sup, Subgroup.mem_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
C : Type u_1
inst : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z
rcases : ∀ (b : C) (hb : b ∈ x) (c : C) (hc : c ∈ y) (haz : b * c ∈ z), b * c ∈ x ⊔ y ⊓ z
⊢ a ∈ x ⊔ y ⊓ z

Tactic:
rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
C : Type u_1
inst : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
rw : ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c
⊢ b * c ∈ x ⊔ y ⊓ z

Tactic:
rw [mem_sup]

Premises used: Subgroup.mem_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
C : Type u_1
inst : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c

Tactic:
⟨b, hb, c, mem_inf.2 ⟨hc, (mul_mem_cancel_left (xz hb)).1 haz⟩, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Iff.mp, Subgroup.mem_inf, mul_mem_cancel_left, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
C : Type u_1
inst : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c

Tactic:
exact ⟨b, hb, c, mem_inf.2 ⟨hc, (mul_mem_cancel_left (xz hb)).1 haz⟩, rfl⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hnc : NormalizerCondition G
hmax : IsCoatom H
⊢ H.Normal

Tactic:
normalizer_eq_top_iff.mp (hmax.2 _ (hnc H (lt_top_iff_ne_top.mpr hmax.1)))

Premises used: Iff.mpr, lt_top_iff_ne_top, And.right, And.left, Subgroup.normalizer_eq_top_iff, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G ≃* H
K : Subgroup H
⊢ IsCoatom (α := Subgroup G) (comap (↑f : G →* H) K) ↔ IsCoatom K

Tactic:
OrderIso.isCoatom_iff (f.comapSubgroup) K

Premises used: OrderIso.isCoatom_iff, MulEquiv.comapSubgroup, Subgroup.comap
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : G ≃* ↥H
K : Subgroup G
⊢ IsCoatom (α := Subgroup ↥H) (map (↑f : G →* ↥H) K) ↔ IsCoatom K

Tactic:
OrderIso.isCoatom_iff (f.mapSubgroup) K

Premises used: OrderIso.isCoatom_iff, Subgroup.map, Set.Mem, MulEquiv.mapSubgroup
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM : IsCoatom M
⊢ IsCoatom (comap φ M)

Tactic:
And.imp (fun hM ↦ ?_) (fun hM ↦ ?_) hM

Premises used: And.imp, IsCoatom
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM : IsCoatom M
refine_1 : ∀ (hM : M ≠ ⊤), comap φ M ≠ ⊤
refine_2 : ∀ (hM : ∀ (b : Subgroup H), M < b → b = ⊤) (b : Subgroup G), comap φ M < b → b = ⊤
⊢ IsCoatom (comap φ M)

Tactic:
refine And.imp (fun hM ↦ ?_) (fun hM ↦ ?_) hM

Premises used: And.imp
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
hM : M ≠ ⊤
refine_1 : ∀ (hM : comap φ M ≠ comap φ ⊤), comap φ M ≠ ⊤
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (hM : comap φ M ≠ ⊤), comap φ M ≠ ⊤
⊢ comap φ M ≠ ⊤

Tactic:
rwa [← (comap_injective hφ).ne_iff, comap_top] at hM

Premises used: Subgroup.comap_injective, Function.Injective.ne_iff, Subgroup.comap_top
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
K : Subgroup G
hK : comap φ M < K
⊢ M < map φ K → map φ K = ⊤

Tactic:
specialize hM (K.map φ)

Premises used: Subgroup.map
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : M < map φ K → map φ K = ⊤
⊢ comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤

Tactic:
rw [← comap_lt_comap_of_surjective hφ, ← (comap_injective hφ).eq_iff] at hM

Premises used: Subgroup.comap_injective, Function.Injective.eq_iff, Subgroup.comap_lt_comap_of_surjective
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤
⊢ comap φ M < K → K = ⊤

Tactic:
rw [comap_map_eq_self ((M.ker_le_comap φ).trans hK.le), comap_top] at hM

Premises used: LT.lt.le, Subgroup.ker_le_comap, Subgroup.comap_map_eq_self, Subgroup.comap_top, LE.le.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : comap φ M < K → K = ⊤
⊢ K = ⊤

Tactic:
hM hK
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : comap φ M < K → K = ⊤
⊢ K = ⊤

Tactic:
exact hM hK
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Preorder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
⊢ IsOrderedMonoid.{u_1} ↥H

Tactic:
Function.Injective.isOrderedMonoid Subtype.val (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Function.Injective.isOrderedMonoid, Subtype.val, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : CommMonoid G
inst_1 : Preorder G
⊢ StrictMono.{u_1, u_1} (α := ↥⊤) (β := G) (⇑topEquiv : (a : ↥⊤) → G)

Tactic:
fun _ _ ↦ id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
inst : CommMonoid G
inst_1 : Preorder G
S T : Subsemigroup G
h : S = T
⊢ StrictMono (α := ↥S) (β := ↥T) (⇑(subsemigroupCongr h) : (a : ↥S) → ↥T)

Tactic:
fun _ _ ↦ id

Premises used: StrictMono, Set.Mem, id
-- Module: Mathlib.Algebra.Group.Subgroup.Order
Goal:
G : Type u_1
G' : Type u_2
inst : CommMonoid G
inst_1 : LinearOrder G
inst_2 : CommMonoid G'
inst_3 : Preorder G'
e : G ≃* G'
he : StrictMono.{u_1, u_2} (α := G) (β := G') (⇑e : (a : G) → G')
a : G'
⊢ ∀ ⦃b : G'⦄, a < b → LT.lt.{u_1} (α := G) ((e.symm : (a : G') → G) a : G) ((e.symm : (a : G') → G) b : G)

Tactic:
simp [← he.lt_iff_lt]

Premises used: StrictMono.lt_iff_lt
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
S : Type u_4
inst : InvolutiveInv G
inst_1 : SetLike S G
inst_2 : InvMemClass S G
H : S
⊢ (↑H : Set G)⁻¹ = (↑H : Set G)

Tactic:
Set.ext fun _ => inv_mem_iff

Premises used: Set.ext, inv_mem_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
S : Type u_4
inst : Group G
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
s : S
a : G
ha : a ∈ s
h : ∀ (x : G), x ∈ a • (↑s : Set G) ↔ x ∈ (↑s : Set G)
⊢ a • (↑s : Set G) = (↑s : Set G)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
S : Type u_4
inst : Group G
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x : G
⊢ x ∈ a • (↑s : Set G) ↔ x ∈ (↑s : Set G)

Tactic:
simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_left, ha]

Premises used: Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Subgroup G
⊢ (↑s : Set G) = (↑⊥ : Set G) ↔ (↑s : Set G) = 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
S : Type u_4
inst : Group G
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
s : S
a : G
ha : a ∈ s
h : ∀ (x : G), x ∈ MulOpposite.op a • (↑s : Set G) ↔ x ∈ (↑s : Set G)
⊢ MulOpposite.op a • (↑s : Set G) = (↑s : Set G)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
S : Type u_4
inst : Group G
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x : G
⊢ x ∈ MulOpposite.op a • (↑s : Set G) ↔ x ∈ (↑s : Set G)

Tactic:
simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_right, ha]

Premises used: Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_right
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
S : Type u_4
inst : SetLike S G
inst_1 : DivisionMonoid G
inst_2 : SubgroupClass S G
H : S
⊢ (↑H : Set G) / (↑H : Set G) = (↑H : Set G)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
rw : ⋃ a ∈ s, a • (↑(closure s) : Set G) = (↑(closure s) : Set G)
⊢ s * (↑(closure s) : Set G) = (↑(closure s) : Set G)

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]

Premises used: Set.iUnion_smul_set, smul_eq_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
⊢ ∀ (a : G) (ha : a ∈ s), a • (↑(closure s) : Set G) = (↑(closure s) : Set G)

Tactic:
have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s :=
    smul_coe_set <| subset_closure ha
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
h : ∀ (a : G) (ha : a ∈ s), a • (↑(closure s) : Set G) = (↑(closure s) : Set G)
⊢ ⋃ a ∈ s, a • (↑(closure s) : Set G) = (↑(closure s) : Set G)

Tactic:
simp +contextual [h, hs]
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
rw : ⋃ a ∈ s, (↑(closure s) : Set G) <• a = (↑(closure s) : Set G)
⊢ (↑(closure s) : Set G) * s = (↑(closure s) : Set G)

Tactic:
rw [← Set.iUnion_op_smul_set]

Premises used: Set.iUnion_op_smul_set
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
⊢ ∀ (a : G) (ha : a ∈ s), (↑(closure s) : Set G) <• a = (↑(closure s) : Set G)

Tactic:
have h a (ha : a ∈ s) : (closure s : Set G) <• a = closure s :=
    op_smul_coe_set <| subset_closure ha
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
h : ∀ (a : G) (ha : a ∈ s), (↑(closure s) : Set G) <• a = (↑(closure s) : Set G)
⊢ ⋃ a ∈ s, (↑(closure s) : Set G) <• a = (↑(closure s) : Set G)

Tactic:
simp +contextual [h, hs]
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
⊢ HPow.hPow (β := ℕ) s 0 * (↑(closure s) : Set G) = (↑(closure s) : Set G)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
rw : s ^ n * s * (↑(closure s) : Set G) = (↑(closure s) : Set G)
rw₁ : s ^ n * (s * (↑(closure s) : Set G)) = (↑(closure s) : Set G)
rw₂ : s ^ n * (↑(closure s) : Set G) = (↑(closure s) : Set G)
rw₃ rw₄ : (↑(closure s) : Set G) = (↑(closure s) : Set G)
⊢ s ^ (n + 1) * (↑(closure s) : Set G) = (↑(closure s) : Set G)

Tactic:
rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]

Premises used: pow_succ, mul_assoc, Set.mul_subgroupClosure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
⊢ (↑(closure s) : Set G) * HPow.hPow (β := ℕ) s 0 = (↑(closure s) : Set G)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
rw : (↑(closure s) : Set G) * (s * s ^ n) = (↑(closure s) : Set G)
rw₁ : (↑(closure s) : Set G) * s * s ^ n = (↑(closure s) : Set G)
rw₂ : (↑(closure s) : Set G) * s ^ n = (↑(closure s) : Set G)
rw₃ rw₄ : (↑(closure s) : Set G) = (↑(closure s) : Set G)
⊢ (↑(closure s) : Set G) * s ^ (n + 1) = (↑(closure s) : Set G)

Tactic:
rw [pow_succ', ← mul_assoc, subgroupClosure_mul hs, subgroupClosure_mul_pow hs]

Premises used: mul_assoc, pow_succ', Set.subgroupClosure_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
rw : Membership.mem (γ := Subgroup G) (closure S) s⁻¹
⊢ s ∈ (↑(closure S) : Set G)

Tactic:
rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]

Premises used: SetLike.mem_coe, Subgroup.inv_mem_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ Membership.mem (γ := Subgroup G) (closure S) s⁻¹

Tactic:
subset_closure (mem_inv.mp hs)

Premises used: Subgroup.subset_closure, Iff.mp, Set.mem_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ Membership.mem (γ := Subgroup G) (closure S) s⁻¹

Tactic:
exact subset_closure (mem_inv.mp hs)

Premises used: Subgroup.subset_closure, Iff.mp, Set.mem_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
⊢ Eq (α := Submonoid G) (toSubmonoid (closure S)) (Submonoid.closure (S ∪ S⁻¹))

Tactic:
le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)

Premises used: Iff.mpr, le_antisymm, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
refine_1 :
  ∀ (x : G) (hx : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x),
    Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
refine_2 : S ∪ S⁻¹ ⊆ (↑(toSubmonoid (closure S)) : Set G)
⊢ Eq (α := Submonoid G) (toSubmonoid (closure S)) (Submonoid.closure (S ∪ S⁻¹))

Tactic:
refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)

Premises used: Iff.mpr, le_antisymm, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
x : G
hx : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x

Tactic:
closure_induction
        (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
        (Submonoid.one_mem _) (fun x y _ _ hx hy => Submonoid.mul_mem _ hx hy) (fun x _ hx => ?_) hx

Premises used: Subgroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
x : G
hx : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x
refine_1 :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (closure S) x →
      ∀ (hx : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x),
        Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x⁻¹
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x

Tactic:
refine
      closure_induction
        (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
        (Submonoid.one_mem _) (fun x y _ _ hx hy => Submonoid.mul_mem _ hx hy) (fun x _ hx => ?_) hx
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
x_1 : G
hx_1 : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x_1
x : G
h : Membership.mem (γ := Subgroup G) (closure S) x
hx : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
refine_1 : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)⁻¹) x
refine_1₁ : Membership.mem (γ := Submonoid G) (Submonoid.closure (S⁻¹ ∪ S⁻¹⁻¹)) x
refine_1₂ : Membership.mem (γ := Submonoid G) (Submonoid.closure (S⁻¹ ∪ S)) x
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x⁻¹

Tactic:
rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]

Premises used: Set.union_comm, Set.union_inv, inv_inv, Submonoid.mem_closure_inv