awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H₁ H₂ K : Subgroup G
⊢ H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

Tactic:
simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall

Premises used: Subtype.forall, SetLike.ext_iff, and_congr_left_iff, Subgroup.mem_subgroupOf, Subgroup.mem_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (H ⊓ K).subgroupOf K = H.subgroupOf K

Tactic:
subgroupOf_inj.2 (inf_right_idem _ _)

Premises used: Iff.mpr, Subgroup.subgroupOf_inj, inf_right_idem
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : (H ⊓ K).subgroupOf K = H.subgroupOf K
rw₁ rw₂ : H.subgroupOf K = H.subgroupOf K
⊢ (K ⊓ H).subgroupOf K = H.subgroupOf K

Tactic:
rw [inf_comm, inf_subgroupOf_right]

Premises used: Subgroup.inf_subgroupOf_right, inf_comm
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.subgroupOf K = ⊥ ↔ H ⊓ K = ⊥
rw₁ : H.subgroupOf K = subgroupOf ⊥ K ↔ H ⊓ K = ⊥
rw₂ : H ⊓ K = ⊥ ⊓ K ↔ H ⊓ K = ⊥
rw₃ rw₄ : H ⊓ K = ⊥ ↔ H ⊓ K = ⊥
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K

Tactic:
rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]

Premises used: Subgroup.subgroupOf_inj, disjoint_iff, Subgroup.bot_subgroupOf, bot_inf_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.subgroupOf K = subgroupOf ⊤ K ↔ K ≤ H
rw₁ : H ⊓ K = ⊤ ⊓ K ↔ K ≤ H
rw₂ : H ⊓ K = K ↔ K ≤ H
rw₃ rw₄ : K ≤ H ↔ K ≤ H
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H

Tactic:
rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]

Premises used: Subgroup.subgroupOf_inj, top_inf_eq, Subgroup.top_subgroupOf, inf_eq_right
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H_1 K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
H : Subgroup G
inst_6 : IsMulCommutative G
⊢ IsMulCommutative.{u_1} ↥H

Tactic:
IsMulCommutative.of_setLike_mul_comm fun a _ b _ ↦ mul_comm' a b

Premises used: Set.Mem, IsMulCommutative.of_setLike_mul_comm, mul_comm'
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H_1 K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
H : Subgroup G
f : G →* G'
inst_6 : IsMulCommutative.{u_1} ↥H
⊢ IsMulCommutative.{u_2} ↥(map f H)

Tactic:
.of_setLike_mul_comm ?_

Premises used: Set.Mem, IsMulCommutative.of_setLike_mul_comm
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H_1 K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
H : Subgroup G
f : G →* G'
inst_6 : IsMulCommutative.{u_1} ↥H
refine : ∀ a ∈ map f H, ∀ b ∈ map f H, a * b = b * a
⊢ IsMulCommutative.{u_2} ↥(map f H)

Tactic:
refine .of_setLike_mul_comm ?_
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H_1 K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
H : Subgroup G
f : G →* G'
inst_6 : IsMulCommutative.{u_1} ↥H
a : G
ha : a ∈ (↑H : Set G)
b : G
hb : b ∈ (↑H : Set G)
⊢ HMul.hMul (α := G') (β := G') ((f : (a : G) → G') a : G') ((f : (a : G) → G') b : G') =
    HMul.hMul (α := G') (β := G') ((f : (a : G) → G') b : G') ((f : (a : G) → G') a : G')

Tactic:
simpa [map_mul] using congr(f $(setLike_mul_comm ha hb))

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Injective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
inst_2 : IsMulCommutative.{u_1} ↥H
a : G'
ha : Membership.mem (α := G) H ((f : (a : G') → G) a : G)
b : G'
hb : Membership.mem (α := G) H ((f : (a : G') → G) b : G)
⊢ Eq.{u_1 + 1} (α := G) ((f : (a : G') → G) (a * b) : G) ((f : (a : G') → G) (b * a) : G)

Tactic:
simpa using setLike_mul_comm ha hb

Premises used: setLike_mul_comm
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H_1 K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
H : Subgroup G
inst_6 : IsMulCommutative.{u_1} ↥H
⊢ IsMulCommutative.{u_1} ↥(H.subgroupOf K)

Tactic:
H.comap_injective_isMulCommutative Subtype.coe_injective

Premises used: Subgroup.subgroupOf, Set.Mem, Subgroup.comap_injective_isMulCommutative, Subtype.coe_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H : Type u_5
inst_4 : Group H
f : G ≃* H
sg : Subgroup H
⊢ Subgroup.comap (↑f.symm : H →* G) (Subgroup.comap (↑f : G →* H) sg) = sg

Tactic:
simp [Subgroup.comap_comap]

Premises used: Subgroup.comap_comap
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H : Type u_5
inst_4 : Group H
f : G ≃* H
sh : Subgroup G
⊢ Subgroup.comap (↑f : G →* H) (Subgroup.comap (↑f.symm : H →* G) sh) = sh

Tactic:
simp [Subgroup.comap_comap]

Premises used: Subgroup.comap_comap
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H : Type u_5
inst_4 : Group H
f : G ≃* H
sg1 sg2 : Subgroup H
h :
  LE.le.{u_1} (α := Subgroup G)
    ((({ toFun := Subgroup.comap (↑f : G →* H), invFun := Subgroup.comap (↑f.symm : H →* G), left_inv := ⋯,
              right_inv := ⋯ } :
            Equiv.{u_5 + 1, u_1 + 1} (Subgroup H) (Subgroup G)) :
          (a : Subgroup H) → Subgroup G)
        sg1 :
      Subgroup G)
    ((({ toFun := Subgroup.comap (↑f : G →* H), invFun := Subgroup.comap (↑f.symm : H →* G), left_inv := ⋯,
              right_inv := ⋯ } :
            Equiv.{u_5 + 1, u_1 + 1} (Subgroup H) (Subgroup G)) :
          (a : Subgroup H) → Subgroup G)
        sg2 :
      Subgroup G)
⊢ sg1 ≤ sg2

Tactic:
simpa [Subgroup.comap_comap] using
      Subgroup.comap_mono (f := (f.symm : H →* G)) h

Premises used: Subgroup.comap_mono, Subgroup.comap_comap
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Type u_5
inst_1 : Group H
e : G ≃* H
⊢ (⇑e.comapSubgroup : (a : Subgroup H) → Subgroup G) = Subgroup.comap e.toMonoidHom

Tactic:
rfl

Premises used: Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Type u_5
inst_1 : Group H
e : G ≃* H
⊢ e.comapSubgroup.symm = e.symm.comapSubgroup

Tactic:
rfl

Premises used: MulEquiv.comapSubgroup, RelIso.symm, OrderIso.symm, Equiv.symm, MulEquiv.symm, Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H_1 : Type u_5
inst_4 : Group H_1
H : Type u_6
inst_5 : Group H
f : G ≃* H
sg : Subgroup G
⊢ Subgroup.map (↑f.symm : H →* G) (Subgroup.map (↑f : G →* H) sg) = sg

Tactic:
simp [Subgroup.map_map]

Premises used: Subgroup.map_map
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H_1 : Type u_5
inst_4 : Group H_1
H : Type u_6
inst_5 : Group H
f : G ≃* H
sh : Subgroup H
⊢ Subgroup.map (↑f : G →* H) (Subgroup.map (↑f.symm : H →* G) sh) = sh

Tactic:
simp [Subgroup.map_map]

Premises used: Subgroup.map_map
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H_1 : Type u_5
inst_4 : Group H_1
H : Type u_6
inst_5 : Group H
f : G ≃* H
sg1 sg2 : Subgroup G
h :
  LE.le.{u_6} (α := Subgroup H)
    ((({ toFun := Subgroup.map (↑f : G →* H), invFun := Subgroup.map (↑f.symm : H →* G), left_inv := ⋯,
              right_inv := ⋯ } :
            Equiv.{u_1 + 1, u_6 + 1} (Subgroup G) (Subgroup H)) :
          (a : Subgroup G) → Subgroup H)
        sg1 :
      Subgroup H)
    ((({ toFun := Subgroup.map (↑f : G →* H), invFun := Subgroup.map (↑f.symm : H →* G), left_inv := ⋯,
              right_inv := ⋯ } :
            Equiv.{u_1 + 1, u_6 + 1} (Subgroup G) (Subgroup H)) :
          (a : Subgroup G) → Subgroup H)
        sg2 :
      Subgroup H)
⊢ sg1 ≤ sg2

Tactic:
simpa [Subgroup.map_map] using
      Subgroup.map_mono (f := (f.symm : H →* G)) h

Premises used: Subgroup.map_mono, Subgroup.map_map
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Type u_5
inst_1 : Group H
e : G ≃* H
⊢ (⇑e.mapSubgroup : (a : Subgroup G) → Subgroup H) = Subgroup.map e.toMonoidHom

Tactic:
rfl

Premises used: Subgroup.map, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Type u_5
inst_1 : Group H
e : G ≃* H
⊢ e.mapSubgroup.symm = e.symm.mapSubgroup

Tactic:
rfl

Premises used: Subgroup.map, RelIso.symm, MulEquiv.mapSubgroup, OrderIso.symm, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
e : G ≃* N
s : Subgroup N
⊢ Eq (α := Submonoid G) (toSubmonoid (comap (↑e : G →* N) s)) (Submonoid.comap e.toMonoidHom s.toSubmonoid)

Tactic:
rfl

Premises used: Submonoid.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup N
⊢ map f (comap f H) ≤ H

Tactic:
(gc_map_comap f).l_u_le _

Premises used: Subgroup.gc_map_comap, GaloisConnection.l_u_le
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
⊢ H ≤ comap f (map f H)

Tactic:
(gc_map_comap f).le_u_l _

Premises used: Subgroup.gc_map_comap, GaloisConnection.le_u_l
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
g : N →* G
hl : LeftInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
hr : RightInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
H : Subgroup G
rw : (⇑f : (a : G) → N) '' (↑H : Set G) = (↑(comap g H) : Set N)
rw₁ : Eq.{u_5 + 1} (α := Set N) ((⇑f : (a : G) → N) '' (↑H : Set G)) ((⇑g : (a : N) → G) ⁻¹' (↑H : Set G))
rw₂ rw₃ : Eq.{u_5 + 1} (α := Set N) ((⇑g : (a : N) → G) ⁻¹' (↑H : Set G)) ((⇑g : (a : N) → G) ⁻¹' (↑H : Set G))
⊢ (↑(map f H) : Set N) = (↑(comap g H) : Set N)

Tactic:
rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]

Premises used: Subgroup.coe_map, Set.image_eq_preimage_of_inverse, Subgroup.coe_comap
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
h : ↥H
⊢ Eq.{u_5 + 1} (α := N) ((↑((H.equivMapOfInjective f hf : (a : ↥H) → ↥(map f H)) h) : N) : N)
    ((f : (a : G) → N) (↑h : G) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
H' : Subgroup G'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := ↥(Subgroup.comap f H')) (β := ↥H')
    (⇑(f.subgroupComap H') : (a : ↥(Subgroup.comap f H')) → ↥H')

Tactic:
f.submonoidComap_surjective_of_surjective H'.toSubmonoid hf

Premises used: Set.Mem, MonoidHom.submonoidComap_surjective_of_surjective, Subgroup.toSubmonoid
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
H : Subgroup G
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := ↥H) (β := ↥(Subgroup.map f H))
    (⇑(f.subgroupMap H) : (a : ↥H) → ↥(Subgroup.map f H))

Tactic:
f.submonoidMap_surjective H.toSubmonoid

Premises used: Set.Mem, Subgroup.toSubmonoid, MonoidHom.submonoidMap_surjective
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H = K
x : ↥H
⊢ (↑((subgroupCongr h : (a : ↥H) → ↥K) x) : G) = (↑x : G)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H = K
x : ↥K
⊢ (↑(((subgroupCongr h).symm : (a : ↥K) → ↥H) x) : G) = (↑x : G)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
e : G ≃* G'
H : Subgroup G
g : ↥H
⊢ Eq.{u_2 + 1} (α := G') ((↑((e.subgroupMap H : (a : ↥H) → ↥(Subgroup.map (↑e : G →* G') H)) g) : G') : G')
    ((e : (a : G) → G') (↑g : G) : G')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
e : G ≃* G'
H : Subgroup G
g : ↥(Subgroup.map (↑e : G →* G') H)
⊢ Eq.{u_1 + 1} (α := ↥H) (((e.subgroupMap H).symm : (a : ↥(Subgroup.map (↑e : G →* G') H)) → ↥H) g : ↥H)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((e.symm : (a : G') → G) (↑g : G')) ⋯ : ↥H)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
s : Set N
x : G
hx : Membership.mem (γ := Set G) ((⇑f : (a : G) → N) ⁻¹' s) x
⊢ Membership.mem (α := N) (γ := Subgroup N) (closure s) ((f : (a : G) → N) x : N)

Tactic:
subset_closure hx

Premises used: Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
s : Set N
x : G
hx : Membership.mem (γ := Set G) ((⇑f : (a : G) → N) ⁻¹' s) x
⊢ Membership.mem (α := N) (γ := Subgroup N) (closure s) ((f : (a : G) → N) x : N)

Tactic:
exact subset_closure hx

Premises used: Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
s : Set G
⊢ map f (closure s) = closure ((⇑f : (a : G) → N) '' s)

Tactic:
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subgroup.gi N).gc (Subgroup.gi G).gc
    fun _ ↦ rfl

Premises used: Subgroup.gc_map_comap, GaloisConnection.l_comm_of_u_comm, Set.image_preimage, Subgroup.gi, rfl, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
K : Subgroup N
⊢ Set.SurjOn (⇑f : (a : G) → N) (↑H : Set G) (↑K : Set N) ↔ K ≤ map f H

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.SurjOn, Set.Subset, Set.image
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
e : G ≃* G'
h :
  ∀ (x : ↥H),
    Eq.{u_2 + 1} (α := G')
      (↑(((H.equivMapOfInjective (↑e : G →* G') ⋯ : MulEquiv.{u_1, u_2} ↥H ↥(map (↑e : G →* G') H)) :
              (a : ↥H) → ↥(map (↑e : G →* G') H))
            x) :
        G')
      (↑((e.subgroupMap H : (a : ↥H) → ↥(map (↑e : G →* G') H)) x) : G')
⊢ H.equivMapOfInjective (↑e : G →* G') ⋯ = e.subgroupMap H

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
e : G ≃* G'
x : ↥H
⊢ Eq.{u_2 + 1} (α := G')
    (↑(((H.equivMapOfInjective (↑e : G →* G') ⋯ : MulEquiv.{u_1, u_2} ↥H ↥(map (↑e : G →* G') H)) :
            (a : ↥H) → ↥(map (↑e : G →* G') H))
          x) :
      G')
    (↑((e.subgroupMap H : (a : ↥H) → ↥(map (↑e : G →* G') H)) x) : G')

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
x : Gᵐᵒᵖ
S : Subgroup G
⊢ x ∈ S.op ↔ MulOpposite.unop x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
⊢ H.op.toSubmonoid = H.op

Tactic:
rfl

Premises used: Submonoid.op, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
⊢ H.op.toSubsemigroup = H.op

Tactic:
dsimp
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
x : G
S : Subgroup Gᵐᵒᵖ
⊢ x ∈ S.unop ↔ MulOpposite.op x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.toSubmonoid = H.unop

Tactic:
rfl

Premises used: Submonoid.unop, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.toSubsemigroup = H.unop

Tactic:
dsimp
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
S : Subgroup G
⊢ S.op.unop = S

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, MulOpposite.unop, Subgroup.unop, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
S : Subgroup Gᵐᵒᵖ
⊢ S.unop.op = S

Tactic:
rfl

Premises used: Set.Mem, MulOpposite, setOf, Subgroup.op, Set.preimage, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
S₁ : Subgroup G
S₂ : Subgroup Gᵐᵒᵖ
⊢ S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
S₁ : Subgroup Gᵐᵒᵖ
S₂ : Subgroup G
⊢ S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
S₁ S₂ : Subgroup G
⊢ S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
S₁ S₂ : Subgroup Gᵐᵒᵖ
⊢ S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subgroup G) Subgroup.op

Tactic:
opEquiv.injective

Premises used: Subgroup.op, OrderIso.injective, Subgroup.opEquiv
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subgroup Gᵐᵒᵖ) Subgroup.unop

Tactic:
opEquiv.symm.injective

Premises used: OrderIso.symm, OrderIso.injective, Subgroup.opEquiv, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
S T : Subgroup G
⊢ S.op = T.op ↔ S = T

Tactic:
opEquiv.eq_iff_eq

Premises used: RelIso.eq_iff_eq, Subgroup.op, Subgroup.opEquiv
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
S T : Subgroup Gᵐᵒᵖ
⊢ S.unop = T.unop ↔ S = T

Tactic:
opEquiv.symm.eq_iff_eq

Premises used: RelIso.eq_iff_eq, OrderIso.symm, Subgroup.opEquiv, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h :
  ∀ (x : Gᵐᵒᵖ),
    Membership.mem (γ := Subgroup Gᵐᵒᵖ) (Subgroup.op (normalizer (↑H : Set G))) x ↔
      Membership.mem (γ := Subgroup Gᵐᵒᵖ) (normalizer (↑H.op : Set Gᵐᵒᵖ)) x
⊢ Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (normalizer (↑H : Set G))) (normalizer (↑H.op : Set Gᵐᵒᵖ))

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : Gᵐᵒᵖ
h : (∀ (n : G), n * MulOpposite.unop x ∈ H ↔ MulOpposite.unop x * n ∈ H) ↔ ∀ (n : Gᵐᵒᵖ), n * x ∈ H.op ↔ x * n ∈ H.op
⊢ Membership.mem (γ := Subgroup Gᵐᵒᵖ) (Subgroup.op (normalizer (↑H : Set G))) x ↔
    Membership.mem (γ := Subgroup Gᵐᵒᵖ) (normalizer (↑H.op : Set Gᵐᵒᵖ)) x

Tactic:
rw [mem_op, mem_normalizer_iff', mem_normalizer_iff']

Premises used: Subgroup.mem_op, Subgroup.mem_normalizer_iff'
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ (∀ (n : G), n * MulOpposite.unop x ∈ H ↔ MulOpposite.unop x * n ∈ H) ↔ ∀ (n : Gᵐᵒᵖ), n * x ∈ H.op ↔ x * n ∈ H.op

Tactic:
simp [iff_comm]

Premises used: iff_comm
-- Module: Mathlib.Algebra.Group.Subgroup.MulOpposite
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
rw :
  Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))))
    (Subgroup.op (normalizer (↑H.unop : Set G)))
rw₁ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (Subgroup.op (normalizer (↑H.unop : Set G)))
rw₂ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (normalizer (↑H.unop.op : Set Gᵐᵒᵖ))
rw₃ rw₄ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (normalizer (↑H : Set Gᵐᵒᵖ))
⊢ Eq (α := Subgroup G) (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))) (normalizer (↑H.unop : Set G))

Tactic:
rw [← op_inj, op_unop, op_normalizer, op_unop]

Premises used: Subgroup.op_normalizer, Subgroup.op_unop, Subgroup.op_inj
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
⊢ Eq.{u_2 + 1} (α := Subgroup Gᵐᵒᵖ) (Subgroup.op ⊥) ⊥

Tactic:
opEquiv.map_bot

Premises used: Subgroup.op, Subgroup.opEquiv, OrderIso.map_bot
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S : Subgroup G
⊢ S.op = ⊥ ↔ S = ⊥

Tactic:
op_injective.eq_iff' op_bot

Premises used: Subgroup.op_bot, Function.Injective.eq_iff', Subgroup.op_injective
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
⊢ Eq.{u_2 + 1} (α := Subgroup G) (Subgroup.unop ⊥) ⊥

Tactic:
opEquiv.symm.map_bot

Premises used: OrderIso.symm, Subgroup.opEquiv, OrderIso.map_bot, Subgroup.unop
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S : Subgroup Gᵐᵒᵖ
⊢ S.unop = ⊥ ↔ S = ⊥

Tactic:
unop_injective.eq_iff' unop_bot

Premises used: Function.Injective.eq_iff', Subgroup.unop_injective, Subgroup.unop_bot
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
⊢ Eq.{u_2 + 1} (α := Subgroup Gᵐᵒᵖ) (Subgroup.op ⊤) ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Subgroup.op, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S : Subgroup G
⊢ S.op = ⊤ ↔ S = ⊤

Tactic:
op_injective.eq_iff' op_top

Premises used: Subgroup.op_top, Function.Injective.eq_iff', Subgroup.op_injective
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
⊢ Eq.{u_2 + 1} (α := Subgroup G) (Subgroup.unop ⊤) ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, Subgroup.unop, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Goal:
G : Type u_2
inst : Group G
S : Subgroup Gᵐᵒᵖ
⊢ S.unop = ⊤ ↔ S = ⊤

Tactic:
unop_injective.eq_iff' unop_top

Premises used: Function.Injective.eq_iff', Subgroup.unop_injective, Subgroup.unop_top
-- 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:
opEquiv.map_sup _ _

Premises used: Set.Mem, setOf, Subgroup.op, Subgroup.opEquiv, OrderIso.map_sup
-- 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:
opEquiv.symm.map_sup _ _

Premises used: Set.Mem, setOf, OrderIso.symm, Subgroup.opEquiv, OrderIso.map_sup, Subgroup.unop