awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₃ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₄ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₅ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
rwa₆ : ∀ (hxy : y.1 = x.1 ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
rwa₇ : ∀ (hxy : y.1 = x.1 ∧ x.2 = y.2), x = y
rwa₈ : ∀ (hxy : x.1 = y.1 ∧ x.2 = y.2), x = y
rwa₉ rwa₁₀ rwa₁₁ rwa₁₂ : ∀ (hxy : x = y), x = y
⊢ x = y

Tactic:
rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy

Premises used: mul_inv_eq_one, Subgroup.coe_inv, Prod.ext_iff, eq_comm, Subtype.ext_iff, Subgroup.coe_mul, inv_mul_eq_one
-- 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_1 : Type u_5
inst_4 : Group N_1
P : Type u_6
inst_5 : Group P
N : Type u_7
inst_6 : Group N
f : G →* N
H : Subgroup N
a : G
ha : Membership.mem (γ := Set G) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) a
rw : Membership.mem (α := N) H (((f : (a : G) → N) a)⁻¹ : N)
⊢ Membership.mem (α := N) H ((f : (a : G) → N) a⁻¹ : N)

Tactic:
rw [f.map_inv]

Premises used: MonoidHom.map_inv
-- 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_1 : Type u_5
inst_4 : Group N_1
P : Type u_6
inst_5 : Group P
N : Type u_7
inst_6 : Group N
f : G →* N
H : Subgroup N
a : G
ha : Membership.mem (γ := Set G) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) a
⊢ Membership.mem (α := N) H (((f : (a : G) → N) a)⁻¹ : N)

Tactic:
H.inv_mem ha

Premises used: Set.Mem, Subgroup.inv_mem
-- 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_1 : Type u_5
inst_4 : Group N_1
P : Type u_6
inst_5 : Group P
N : Type u_7
inst_6 : Group N
f : G →* N
H : Subgroup N
a : G
ha : Membership.mem (γ := Set G) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) a
⊢ Membership.mem (α := N) H (((f : (a : G) → N) a)⁻¹ : N)

Tactic:
exact H.inv_mem ha

Premises used: Subgroup.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup N
f : G →* N
⊢ (↑(comap f K) : Set G) = (⇑f : (a : G) → N) ⁻¹' (↑K : Set N)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup N
f : G →* N
x : G
⊢ x ∈ comap f K ↔ Membership.mem (α := N) K ((f : (a : G) → N) x : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- 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
K K' : Subgroup N
⊢ K ≤ K' → comap f K ≤ comap f K'

Tactic:
preimage_mono

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage_mono, Set.preimage
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
P : Type u_6
inst_2 : Group P
K : Subgroup P
g : N →* P
f : G →* N
⊢ comap f (comap g K) = comap (g.comp f) K

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
N : Type u_5
inst : Group N
K : Subgroup N
h : ∀ (x : N), x ∈ comap (MonoidHom.id N) K ↔ x ∈ K
⊢ comap (MonoidHom.id N) K = K

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
N : Type u_5
inst : Group N
K : Subgroup N
x : N
⊢ x ∈ comap (MonoidHom.id N) K ↔ x ∈ K

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
G₂ : Type u_7
inst_1 : Group G₂
f : G →* G₂
s : Subgroup G₂
⊢ Eq.{u_1 + 1} (α := AddSubgroup (Additive G))
    (AddSubgroup.comap.{u_1, u_7} (N := Additive G₂)
      ((MonoidHom.toAdditive : (a : G →* G₂) → Additive G →+ Additive G₂) f)
      ((toAddSubgroup : (a : Subgroup G₂) → AddSubgroup (Additive G₂)) s))
    ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) (comap f s))

Tactic:
rfl

Premises used: AddSubgroup.comap, Set.Mem, Additive, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
A : Type u_7
A₂ : Type u_8
inst : AddGroup A
inst_1 : AddGroup A₂
f : A →+ A₂
s : AddSubgroup A₂
⊢ Eq.{u_7 + 1} (α := Subgroup (Multiplicative A))
    (comap.{u_7, u_8} (N := Multiplicative A₂)
      ((AddMonoidHom.toMultiplicative : (a : A →+ A₂) → Multiplicative A →* Multiplicative A₂) f)
      ((AddSubgroup.toSubgroup : (a : AddSubgroup A₂) → Subgroup (Multiplicative A₂)) s))
    ((AddSubgroup.toSubgroup : (a : AddSubgroup A) → Subgroup (Multiplicative A)) (AddSubgroup.comap f s))

Tactic:
rfl

Premises used: Set.Mem, setOf, Multiplicative, Set.preimage, 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 K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
f : G →* N
H : Subgroup G
x : G
hx : x ∈ (↑H : Set G)
⊢ Membership.mem.{u_5, u_5} (α := N) (γ := Set N) ((⇑f : (a : G) → N) '' (↑H : Set G)) (((f : (a : G) → N) x)⁻¹ : N)

Tactic:
⟨x⁻¹, H.inv_mem hx, f.map_inv x⟩

Premises used: Set.Mem, setOf, Inv.inv, Subgroup.inv_mem, MonoidHom.map_inv, And.intro, Exists.intro, Set.image
-- 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
f : G →* N
H : Subgroup G
x : G
hx : x ∈ (↑H : Set G)
⊢ Membership.mem.{u_5, u_5} (α := N) (γ := Set N) ((⇑f : (a : G) → N) '' (↑H : Set G)) (((f : (a : G) → N) x)⁻¹ : N)

Tactic:
exact ⟨x⁻¹, H.inv_mem hx, f.map_inv x⟩
-- 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
K : Subgroup G
⊢ (↑(map f K) : Set N) = (⇑f : (a : G) → N) '' (↑K : Set G)

Tactic:
rfl

Premises used: setOf, Set.image, 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'
K : Subgroup G
⊢ (map f K).toSubmonoid = Submonoid.map f K.toSubmonoid

Tactic:
rfl

Premises used: Submonoid.map, 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
K : Subgroup G
y : N
⊢ y ∈ map f K ↔ ∃ x ∈ K, (f : (a : G) → N) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- 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
K : Subgroup G
x : G
hx : x ∈ K
⊢ Membership.mem (α := N) (map f K) ((f : (a : G) → N) x : N)

Tactic:
mem_image_of_mem f hx

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, Set.image, DFunLike.coe
-- 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
K : Subgroup G
x : ↥K
⊢ Membership.mem (α := N) (map f K) ((f : (a : G) → N) (↑x : G) : N)

Tactic:
mem_map_of_mem f x.prop

Premises used: Subgroup.mem_map_of_mem, Subtype.prop
-- 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
K K' : Subgroup G
⊢ K ≤ K' → map f K ≤ map f K'

Tactic:
image_mono

Premises used: Set.Mem, Set.image_mono, setOf, Set.Subset, Set.image
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
⊢ map (MonoidHom.id G) K = K

Tactic:
SetLike.coe_injective <| image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
P : Type u_6
inst_2 : Group P
g : N →* P
f : G →* N
⊢ map g (map f K) = map (g.comp f) K

Tactic:
SetLike.coe_injective <| image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
y : G
left : y ∈ (↑K : Set G)
⊢ Membership.mem.{u_5, u_5} (α := N) (γ := Subgroup N) ⊥ ((1 : (a : G) → N) y : N)

Tactic:
simp
-- 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
K : Subgroup G
x : N
⊢ x ∈ map f.toMonoidHom K ↔ Membership.mem (α := G) K ((f.symm : (a : N) → G) x : G)

Tactic:
Set.mem_image_equiv

Premises used: Set.Mem, setOf, Set.image, Set.mem_image_equiv
-- 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
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
K : Subgroup G
x : G
⊢ Membership.mem (α := N) (map f K) ((f : (a : G) → N) x : N) ↔ x ∈ K

Tactic:
hf.mem_set_image

Premises used: Set.Mem, setOf, Set.image, Function.Injective.mem_set_image
-- 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
K : Subgroup G
⊢ map f.toMonoidHom K = comap f.symm.toMonoidHom K

Tactic:
SetLike.coe_injective (f.toEquiv.image_eq_preimage_symm K)

Premises used: MulEquiv.toEquiv, SetLike.coe_injective, Equiv.image_eq_preimage_symm, SetLike.coe
-- 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
K : Subgroup G
⊢ Eq (α := Subgroup N) (map (↑f : G →* N) K) (comap (↑f.symm : N →* G) K)

Tactic:
map_equiv_eq_comap_symm' _ _

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, Subgroup.map_equiv_eq_comap_symm'
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : N ≃* G
K : Subgroup G
⊢ Eq (α := Subgroup N) (comap (↑f : N →* G) K) (map (↑f.symm : G →* N) K)

Tactic:
(map_equiv_eq_comap_symm f.symm K).symm

Premises used: Equiv.symm, Eq.symm, MulEquiv.symm, Subgroup.map_equiv_eq_comap_symm
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : N ≃* G
K : Subgroup G
⊢ comap f.toMonoidHom K = map f.symm.toMonoidHom K

Tactic:
(map_equiv_eq_comap_symm f.symm K).symm

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, Eq.symm, MulEquiv.symm, Subgroup.map_equiv_eq_comap_symm
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
mp : map (↑e.symm : N →* G) H = K → map (↑e : G →* N) K = H
mpr : map (↑e : G →* N) K = H → map (↑e.symm : N →* G) H = K
⊢ map (↑e.symm : N →* G) H = K ↔ map (↑e : G →* N) K = H

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
mp : map (MonoidHom.comp (↑e : G →* N) (↑e.symm : N →* G)) H = H
mp₁ : map (↑(e.symm.trans e) : N →* N) H = H
mp₂ : map (↑(MulEquiv.refl N) : N →* N) H = H
mp₃ : map (MonoidHom.id N) H = H
mp₄ mp₅ : H = H
⊢ map (↑e : G →* N) (map (↑e.symm : N →* G) H) = H

Tactic:
rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
      MulEquiv.coe_monoidHom_refl, map_id]

Premises used: MulEquiv.symm_trans_self, Subgroup.map_id, MulEquiv.coe_monoidHom_trans, MulEquiv.coe_monoidHom_refl, Subgroup.map_map
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
e : G ≃* N
mpr : map (MonoidHom.comp (↑e.symm : N →* G) (↑e : G →* N)) K = K
mpr₁ : map (↑(e.trans e.symm) : G →* G) K = K
mpr₂ : map (↑(MulEquiv.refl G) : G →* G) K = K
mpr₃ : map (MonoidHom.id G) K = K
mpr₄ mpr₅ : K = K
⊢ map (↑e.symm : N →* G) (map (↑e : G →* N) K) = K

Tactic:
rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
      MulEquiv.coe_monoidHom_refl, map_id]

Premises used: Subgroup.map_id, MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm, MulEquiv.coe_monoidHom_refl, Subgroup.map_map
-- 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
K : Subgroup G
H : Subgroup N
⊢ map f K ≤ H ↔ K ≤ comap f H

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- 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
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ =>
  map_le_iff_le_comap

Premises used: Subgroup.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H K : Subgroup G
f : G →* N
⊢ map f (H ⊔ K) = map f H ⊔ map f K

Tactic:
(gc_map_comap f).l_sup

Premises used: Subgroup.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
ι : Sort u_7
f : G →* N
s : ι → Subgroup G
⊢ map f (iSup s) = ⨆ (i : ι), map f (s i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: Subgroup.gc_map_comap, GaloisConnection.l_iSup
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H K : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ map f (H ⊓ K) = map f H ⊓ map f K

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
ι : Sort u_7
inst_2 : Nonempty ι
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
s : ι → Subgroup G
a : (↑(map f (iInf s)) : Set N) = (↑(⨅ (i : ι), map f (s i)) : Set N)
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
ι : Sort u_7
inst_2 : Nonempty ι
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
s : ι → Subgroup G
⊢ (↑(map f (iInf s)) : Set N) = (↑(⨅ (i : ι), map f (s i)) : Set N)

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Premises used: Set.InjOn.image_iInter_eq, Set.injOn_of_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H K : Subgroup N
f : G →* N
⊢ comap f H ⊔ comap f K ≤ comap f (H ⊔ K)

Tactic:
Monotone.le_map_sup (fun _ _ => comap_mono) H K

Premises used: Monotone.le_map_sup, Subgroup.comap_mono
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
ι : Sort u_7
f : G →* N
s : ι → Subgroup N
⊢ ⨆ (i : ι), comap f (s i) ≤ comap f (iSup s)

Tactic:
Monotone.le_map_iSup fun _ _ => comap_mono

Premises used: Monotone.le_map_iSup, Subgroup.comap_mono
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H K : Subgroup N
f : G →* N
⊢ comap f (H ⊓ K) = comap f H ⊓ comap f K

Tactic:
(gc_map_comap f).u_inf

Premises used: Subgroup.gc_map_comap, GaloisConnection.u_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
ι : Sort u_7
f : G →* N
s : ι → Subgroup N
⊢ comap f (iInf s) = ⨅ (i : ι), comap f (s i)

Tactic:
(gc_map_comap f).u_iInf

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

Tactic:
le_inf (map_mono inf_le_left) (map_mono inf_le_right)

Premises used: Set.Mem, inf_le_right, le_inf, Subgroup.map_mono, inf_le_left
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H K : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
rw : (↑(map f (H ⊓ K)) : Set N) = (↑(map f H ⊓ map f K) : Set N)
⊢ map f (H ⊓ K) = map f H ⊓ map f K

Tactic:
rw [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H K : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ (↑(map f (H ⊓ K)) : Set N) = (↑(map f H ⊓ map f K) : Set N)

Tactic:
simp [Set.image_inter hf]

Premises used: Set.image_inter
-- 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
⊢ map f ⊥ = ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: Subgroup.gc_map_comap, GaloisConnection.l_bot
-- 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
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
h : Disjoint H K
rw : map f H ⊓ map f K = ⊥
rw₁ : map f (H ⊓ K) = ⊥
rw₂ : map f ⊥ = ⊥
rw₃ rw₄ : Eq.{u_5 + 1} (α := Subgroup N) ⊥ ⊥
⊢ Disjoint (map f H) (map f K)

Tactic:
rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]

Premises used: disjoint_iff, Subgroup.map_bot, Iff.mp, Subgroup.map_inf
-- 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 : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
rw : ⊤ ≤ map f ⊤
⊢ map f ⊤ = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- 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 : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
x : N
_ : Membership.mem (γ := Subgroup N) ⊤ x → x ∈ map f ⊤
⊢ Membership.mem (γ := Subgroup N) ⊤ x → x ∈ map f ⊤

Tactic:
_
-- 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 : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
x : N
h_1 : Membership.mem (γ := Subgroup N) ⊤ x
obtain : ∀ (y : G) (hy : (f : (a : G) → N) y = x), x ∈ map f ⊤
⊢ x ∈ map f ⊤

Tactic:
obtain ⟨y, hy⟩ := h x
-- 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 : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
x : N
h_1 : Membership.mem (γ := Subgroup N) ⊤ x
y : G
hy : (f : (a : G) → N) y = x
⊢ x ∈ map f ⊤

Tactic:
⟨y, trivial, hy⟩

Premises used: trivial, Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- 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 : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
x : N
h_1 : Membership.mem (γ := Subgroup N) ⊤ x
y : G
hy : (f : (a : G) → N) y = x
⊢ x ∈ map f ⊤

Tactic:
exact ⟨y, trivial, hy⟩
-- 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
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
h : Codisjoint H K
rw : map f H ⊔ map f K = ⊤
rw₁ : map f (H ⊔ K) = ⊤
rw₂ : map f ⊤ = ⊤
rw₃ rw₄ : Eq.{u_5 + 1} (α := Subgroup N) ⊤ ⊤
⊢ Codisjoint (map f H) (map f K)

Tactic:
rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, map_top_of_surjective _ hf]

Premises used: Subgroup.map_sup, Subgroup.map_top_of_surjective, codisjoint_iff, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
F : Type u_7
inst_2 : EquivLike F G N
inst_3 : MulEquivClass F G N
f : F
⊢ Eq (α := Subgroup N) (map (↑f : G →* N) ⊤) ⊤

Tactic:
map_top_of_surjective _ (EquivLike.surjective f)

Premises used: Subgroup.map_top_of_surjective, EquivLike.surjective
-- 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
⊢ comap f ⊤ = ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: Subgroup.gc_map_comap, GaloisConnection.u_top
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H₁ H₂ H₃ : Subgroup G
h : H₁ ≤ H₂
⊢ H₁.subgroupOf H₃ ≤ H₂.subgroupOf H₃

Tactic:
comap_mono h

Premises used: Set.Mem, Subgroup.comap_mono
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ comap K.subtype H = H.subgroupOf K

Tactic:
rfl

Premises used: Subgroup.subgroupOf, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
K₁ K₂ : Subgroup G
h : K₁ ≤ K₂
H : Subgroup G
⊢ comap (inclusion h) (H.subgroupOf K₂) = H.subgroupOf K₁

Tactic:
rfl

Premises used: Subgroup.subgroupOf, MonoidHom.mk', Set.Mem, Subgroup.subtype, setOf, Set.preimage, Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (↑(H.subgroupOf K) : Set ↥K) = (⇑K.subtype : (a : ↥K) → G) ⁻¹' (↑H : Set G)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : ↥K
⊢ h ∈ H.subgroupOf K ↔ (↑h : G) ∈ H

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (↑(map K.subtype (H.subgroupOf K)) : Set G) = (↑(H ⊓ K) : Set G)

Tactic:
Subtype.image_preimage_coe _ _ |>.trans ?_

Premises used: Set.Mem, Subtype.image_preimage_coe, setOf, Set.preimage, Set.image, Eq.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
refine : (↑K : Set G) ∩ H.toSubsemigroup.1 = (↑(H ⊓ K) : Set G)
⊢ (↑(map K.subtype (H.subgroupOf K)) : Set G) = (↑(H ⊓ K) : Set G)

Tactic:
refine Subtype.image_preimage_coe _ _ |>.trans ?_

Premises used: Subtype.image_preimage_coe, Eq.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (↑K : Set G) ∩ H.toSubsemigroup.1 = (↑(H ⊓ K) : Set G)

Tactic:
apply Set.inter_comm

Premises used: Set.inter_comm
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
rwa : H ⊓ K = H
rwa₁ rwa₂ rwa₃ rwa₄ : H ≤ K
⊢ map K.subtype (H.subgroupOf K) = H

Tactic:
rwa [subgroupOf_map_subtype, inf_eq_left]

Premises used: Subgroup.subgroupOf_map_subtype, inf_eq_left
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ subgroupOf ⊥ H = ⊥

Tactic:
Eq.symm (Subgroup.ext fun _g => Subtype.ext_iff)

Premises used: Subtype.ext_iff, Eq.symm, Subgroup.ext
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ subgroupOf ⊤ H = ⊤

Tactic:
rfl

Premises used: Subgroup.subgroupOf, Set.Mem, Set.univ, setOf, Set.preimage, Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq (α := Subgroup ↥⊥) (H.subgroupOf ⊥) ⊥

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq (α := Subgroup ↥⊥) (H.subgroupOf ⊥) ⊤

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Group.Subgroup.Map
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.subgroupOf H = ⊤

Tactic:
top_unique fun g _hg => g.2

Premises used: top_unique, Subtype.property