awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
S : Submonoid M
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ Eq (α := Submonoid N) (map f (comap f (map f S))) (map f S)

Tactic:
(gc_map_comap f).l_u_l_eq_l _

Premises used: GaloisConnection.l_u_l_eq_l, Submonoid.gc_map_comap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
S : Submonoid N
f : F
⊢ Eq (α := Submonoid M) (comap f (map f (comap f S))) (comap f S)

Tactic:
(gc_map_comap f).u_l_u_eq_u _

Premises used: Submonoid.gc_map_comap, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
S T : Submonoid M
f : F
⊢ Eq (α := Submonoid N) (map f (S ⊔ T)) (map f S ⊔ map f T)

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).l_sup

Premises used: Submonoid.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
f : F
s : ι → Submonoid M
⊢ Eq (α := Submonoid N) (map f (iSup s)) (⨆ (i : ι), map f (s i))

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup

Premises used: GaloisConnection.l_iSup, Submonoid.gc_map_comap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
S T : Submonoid M
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Eq (α := Submonoid N) (map f (S ⊓ T)) (map f S ⊓ map f T)

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst_3 : Nonempty ι
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
s : ι → Submonoid M
a : (↑(map f (iInf s)) : Set N) = (↑(⨅ (i : ι), map f (s i)) : Set N)
⊢ Eq (α := Submonoid N) (map f (iInf s)) (⨅ (i : ι), map f (s i))

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst_3 : Nonempty ι
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
s : ι → Submonoid M
⊢ (↑(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.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
S T : Submonoid N
f : F
⊢ Eq (α := Submonoid M) (comap f (S ⊓ T)) (comap f S ⊓ comap f T)

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).u_inf

Premises used: GaloisConnection.u_inf, Submonoid.gc_map_comap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
f : F
s : ι → Submonoid N
⊢ Eq (α := Submonoid M) (comap f (iInf s)) (⨅ (i : ι), comap f (s i))

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).u_iInf

Premises used: GaloisConnection.u_iInf, Submonoid.gc_map_comap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ Eq (α := Submonoid N) (map f ⊥) ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: Submonoid.gc_map_comap, GaloisConnection.l_bot
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Disjoint H K
rw : Eq (α := Submonoid N) (map f H ⊓ map f K) ⊥
rw₁ : Eq (α := Submonoid N) (map f (H ⊓ K)) ⊥
rw₂ : Eq (α := Submonoid N) (map f ⊥) ⊥
rw₃ rw₄ : Eq.{u_2 + 1} (α := Submonoid N) ⊥ ⊥
⊢ Disjoint (α := Submonoid N) (map f H) (map f K)

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

Premises used: disjoint_iff, Submonoid.map_inf, Iff.mp, Submonoid.map_bot
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ Eq (α := Submonoid M) (comap f ⊤) ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: GaloisConnection.u_top, Submonoid.gc_map_comap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
⊢ map (F := M →* M) (MonoidHom.id M) S = S

Tactic:
ext fun _ => ⟨fun ⟨_, h, rfl⟩ => h, fun h => ⟨_, h, rfl⟩⟩

Premises used: Membership.mem, Submonoid.ext, And.intro, Iff.intro, Exists.intro, _private.0.Submonoid.map_id.match_1, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S_1 : Submonoid M
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Submonoid M
x : M
⊢ Membership.mem (γ := Submonoid M) (comap f (map f S)) x → x ∈ S

Tactic:
simp [mem_comap, mem_map, hf.eq_iff]

Premises used: Submonoid.mem_map, Function.Injective.eq_iff, Submonoid.mem_comap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Submonoid M
⊢ comap f (map f S) = S

Tactic:
(gciMapComap hf).u_l_eq _

Premises used: Submonoid.gciMapComap, GaloisCoinsertion.u_l_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Surjective (α := Submonoid N) (β := Submonoid M) (comap f)

Tactic:
(gciMapComap hf).u_surjective

Premises used: Submonoid.gciMapComap, GaloisCoinsertion.u_surjective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Injective (α := Submonoid M) (β := Submonoid N) (map f)

Tactic:
(gciMapComap hf).l_injective

Premises used: GaloisCoinsertion.l_injective, Submonoid.gciMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Submonoid M
⊢ comap f (map f S ⊓ map f T) = S ⊓ T

Tactic:
(gciMapComap hf).u_inf_l _ _

Premises used: Submonoid.gciMapComap, GaloisCoinsertion.u_inf_l
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → Submonoid M
⊢ comap f (⨅ (i : ι), map f (S i)) = iInf S

Tactic:
(gciMapComap hf).u_iInf_l _

Premises used: GaloisCoinsertion.u_iInf_l, Submonoid.gciMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Submonoid M
⊢ comap f (map f S ⊔ map f T) = S ⊔ T

Tactic:
(gciMapComap hf).u_sup_l _ _

Premises used: Submonoid.gciMapComap, GaloisCoinsertion.u_sup_l
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → Submonoid M
⊢ comap f (⨆ (i : ι), map f (S i)) = iSup S

Tactic:
(gciMapComap hf).u_iSup_l _

Premises used: Submonoid.gciMapComap, GaloisCoinsertion.u_iSup_l
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Submonoid M
⊢ LE.le (α := Submonoid N) (map f S) (map f T) ↔ S ≤ T

Tactic:
(gciMapComap hf).l_le_l_iff

Premises used: GaloisCoinsertion.l_le_l_iff, Submonoid.gciMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ StrictMono (α := Submonoid M) (β := Submonoid N) (map f)

Tactic:
(gciMapComap hf).strictMono_l

Premises used: GaloisCoinsertion.strictMono_l, Submonoid.gciMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S_1 : Submonoid M
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Submonoid N
x : N
h : x ∈ S
y : M
hy : (f : (a : M) → N) y = x
⊢ Membership.mem (γ := Submonoid M) (comap f S) y ∧ (f : (a : M) → N) y = x

Tactic:
simp [hy, h]
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Submonoid N
⊢ map f (comap f S) = S

Tactic:
(giMapComap hf).l_u_eq _

Premises used: GaloisInsertion.l_u_eq, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Surjective (α := Submonoid M) (β := Submonoid N) (map f)

Tactic:
(giMapComap hf).l_surjective

Premises used: GaloisInsertion.l_surjective, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Injective (α := Submonoid N) (β := Submonoid M) (comap f)

Tactic:
(giMapComap hf).u_injective

Premises used: GaloisInsertion.u_injective, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Submonoid N
⊢ map f (comap f S ⊓ comap f T) = S ⊓ T

Tactic:
(giMapComap hf).l_inf_u _ _

Premises used: GaloisInsertion.l_inf_u, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → Submonoid N
⊢ map f (⨅ (i : ι), comap f (S i)) = iInf S

Tactic:
(giMapComap hf).l_iInf_u _

Premises used: GaloisInsertion.l_iInf_u, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Submonoid N
⊢ map f (comap f S ⊔ comap f T) = S ⊔ T

Tactic:
(giMapComap hf).l_sup_u _ _

Premises used: GaloisInsertion.l_sup_u, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → Submonoid N
⊢ map f (⨆ (i : ι), comap f (S i)) = iSup S

Tactic:
(giMapComap hf).l_iSup_u _

Premises used: GaloisInsertion.l_iSup_u, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Submonoid N
⊢ LE.le (α := Submonoid M) (comap f S) (comap f T) ↔ S ≤ T

Tactic:
(giMapComap hf).u_le_u_iff

Premises used: GaloisInsertion.u_le_u_iff, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ StrictMono (α := Submonoid N) (β := Submonoid M) (comap f)

Tactic:
(giMapComap hf).strictMono_u

Premises used: GaloisInsertion.strictMono_u, Submonoid.giMapComap
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_5
inst : MulOneClass M
⊢ (↑topEquiv : ↥⊤ →* M) = subtype ⊤

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, Submonoid.subtype, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
S : Submonoid M
f : M →* N
hf : Injective.{u_5 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : ↥S
⊢ Eq.{u_2 + 1} (α := N) ((↑((S.equivMapOfInjective f hf : (a : ↥S) → ↥(map f S)) x) : N) : N)
    ((f : (a : M) → N) (↑x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_5
inst : MulOneClass M
s : Set M
⊢ Eq (α := Submonoid ↥(closure s))
    (closure (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (closure s) x) ⁻¹' s)) ⊤

Tactic:
eq_top_iff.2 fun x _ ↦ Subtype.recOn x fun _ hx' ↦
    closure_induction (fun _ h ↦ subset_closure h) (one_mem _) (fun _ _ _ _ ↦ mul_mem) hx'

Premises used: Iff.mpr, eq_top_iff, Subtype.recOn
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
⊢ (↑(s.prod t) : Set (M × N)) = (↑s : Set M) ×ˢ (↑t : Set N)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
p : M × N
⊢ p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s₁ s₂ : Submonoid M
t₁ t₂ : Submonoid N
hs : s₁ ≤ s₂
ht : t₁ ≤ t₂
⊢ s₁.prod t₁ ≤ s₂.prod t₂

Tactic:
Set.prod_mono hs ht

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
x : M × N
⊢ Membership.mem (γ := Submonoid (M × N)) (s.prod ⊤) x ↔
    Membership.mem (γ := Submonoid (M × N)) (comap (F := M × N →* M) (MonoidHom.fst M N) s) x

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

Premises used: Submonoid.mem_prod, MonoidHom.coe_fst
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid N
x : M × N
⊢ Membership.mem (γ := Submonoid (M × N)) (prod ⊤ s) x ↔
    Membership.mem (γ := Submonoid (M × N)) (comap (F := M × N →* N) (MonoidHom.snd M N) s) x

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

Premises used: MonoidHom.coe_snd, Submonoid.mem_prod
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
⊢ Eq (α := Submonoid (M × N)) (prod ⊤ ⊤) ⊤

Tactic:
(top_prod _).trans <| comap_top _

Premises used: Submonoid.top_prod, Submonoid.comap_top, Eq.trans
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
⊢ (↑(prod ⊥ ⊥) : Set (M × N)) = (↑⊥ : Set (M × N))

Tactic:
simp [coe_prod]

Premises used: Submonoid.coe_prod
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
⊢ Eq (α := Submonoid (M × N)) (map (F := M →* M × N) (inl M N) s) (s.prod ⊥)

Tactic:
ext fun p =>
    ⟨fun ⟨_, hx, hp⟩ => hp ▸ ⟨hx, Set.mem_singleton 1⟩, fun ⟨hps, hp1⟩ =>
      ⟨p.1, hps, Prod.ext rfl <| (Set.eq_of_mem_singleton hp1).symm⟩⟩

Premises used: Set.mem_singleton, Set.eq_of_mem_singleton, MonoidHom.inl, _private.0.Submonoid.map_inl.match_2, Membership.mem, Eq.rec, _private.0.Submonoid.map_inl.match_1, Bot.bot, Submonoid.ext, Prod.fst, Submonoid.map, Prod.ext, And.intro, Iff.intro, Exists.intro, OfNat.ofNat, Eq.symm, rfl, Submonoid.prod
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid N
⊢ Eq (α := Submonoid (M × N)) (map (F := N →* M × N) (inr M N) s) (prod ⊥ s)

Tactic:
ext fun p =>
    ⟨fun ⟨_, hx, hp⟩ => hp ▸ ⟨Set.mem_singleton 1, hx⟩, fun ⟨hp1, hps⟩ =>
      ⟨p.2, hps, Prod.ext (Set.eq_of_mem_singleton hp1).symm rfl⟩⟩

Premises used: Set.mem_singleton, Set.eq_of_mem_singleton, MonoidHom.inr, Membership.mem, Eq.rec, Bot.bot, Submonoid.ext, Submonoid.map, Prod.ext, And.intro, Iff.intro, Exists.intro, _private.0.Submonoid.map_inr.match_1, _private.0.Submonoid.map_inr.match_2, OfNat.ofNat, Eq.symm, Prod.snd, rfl, Submonoid.prod
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
⊢ s.prod ⊥ ⊔ prod ⊥ t = s.prod t

Tactic:
(le_antisymm (sup_le (prod_mono (le_refl s) bot_le) (prod_mono bot_le (le_refl t))))
    fun p hp => Prod.fst_mul_snd p ▸ mul_mem
        ((le_sup_left : prod s ⊥ ≤ prod s ⊥ ⊔ prod ⊥ t) ⟨hp.1, Set.mem_singleton 1⟩)
        ((le_sup_right : prod ⊥ t ≤ prod s ⊥ ⊔ prod ⊥ t) ⟨Set.mem_singleton 1, hp.2⟩)

Premises used: Set.mem_singleton, le_refl, Prod.fst_mul_snd, le_sup_left, Set.Mem, setOf, Eq.rec, Submonoid.prod_mono, le_sup_right, le_antisymm, And.right, And.left, And.intro, sup_le, OfNat.ofNat, bot_le, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
f : M ≃* N
K : Submonoid M
x : N
⊢ Membership.mem (γ := Submonoid N) (map f.toMonoidHom K) x ↔ Membership.mem (α := M) K ((f.symm : (a : N) → M) x : M)

Tactic:
Set.mem_image_equiv

Premises used: Set.Mem, setOf, Set.image, Set.mem_image_equiv
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
f : M ≃* N
K : Submonoid M
⊢ Eq (α := Submonoid N) (map f K) (comap f.symm 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.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
f : N ≃* M
K : Submonoid M
⊢ Eq (α := Submonoid N) (comap f K) (map f.symm K)

Tactic:
(map_equiv_eq_comap_symm f.symm K).symm

Premises used: Submonoid.map_equiv_eq_comap_symm, Equiv.symm, Eq.symm, MulEquiv.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
f : M ≃* N
⊢ Eq (α := Submonoid N) (map f ⊤) ⊤

Tactic:
SetLike.coe_injective <| Set.image_univ.trans f.surjective.range_eq

Premises used: Set.image_univ, MulEquiv.surjective, SetLike.coe_injective, Function.Surjective.range_eq, Eq.trans
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
mp : u ≤ s.prod t → map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t
mpr : map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t → u ≤ s.prod t
⊢ u ≤ s.prod t ↔ map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
mp : map (F := M × N →* M) (fst M N) u ≤ s
mp₁ : map (F := M × N →* N) (snd M N) u ≤ t
⊢ map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ (↑u : Set (M × N))
⊢ Membership.mem (α := M) s ((fst M N : (a : M × N) → M) (y1, y2) : M)

Tactic:
(h hy1).1

Premises used: Set.Mem, And.left
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ (↑u : Set (M × N))
⊢ Membership.mem (α := M) s ((fst M N : (a : M × N) → M) (y1, y2) : M)

Tactic:
exact (h hy1).1

Premises used: And.left
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ (↑u : Set (M × N))
⊢ Membership.mem (α := N) t ((snd M N : (a : M × N) → N) (y1, y2) : N)

Tactic:
(h hy1).2

Premises used: Set.Mem, And.right
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ (↑u : Set (M × N))
⊢ Membership.mem (α := N) t ((snd M N : (a : M × N) → N) (y1, y2) : N)

Tactic:
exact (h hy1).2

Premises used: And.right
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M × N →* M) (fst M N) u ≤ s
hK : map (F := M × N →* N) (snd M N) u ≤ t
x1 : M
x2 : N
h : (x1, x2) ∈ u
⊢ (x1, x2) ∈ s.prod t

Tactic:
⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro, Exists.intro, rfl