/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
Amelia Livingston, Yury Kudryashov

! This file was ported from Lean 3 source module group_theory.submonoid.operations
! leanprover-community/mathlib commit cf8e77c636317b059a8ce20807a29cf3772a0640
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.Monoid.Cancel.Basic
import Mathlib.GroupTheory.GroupAction.Defs
import Mathlib.GroupTheory.Submonoid.Basic
import Mathlib.GroupTheory.Subsemigroup.Operations

/-!
# Operations on `Submonoid`s

In this file we define various operations on `Submonoid`s and `MonoidHom`s.

## Main definitions

### Conversion between multiplicative and additive definitions

* `Submonoid.toAddSubmonoid`, `Submonoid.toAddSubmonoid'`, `AddSubmonoid.toSubmonoid`,
  `AddSubmonoid.toSubmonoid'`: convert between multiplicative and additive submonoids of `M`,
  `Multiplicative M`, and `Additive M`. These are stated as `OrderIso`s.

### (Commutative) monoid structure on a submonoid

* `Submonoid.toMonoid`, `Submonoid.toCommMonoid`: a submonoid inherits a (commutative) monoid
  structure.

### Group actions by submonoids

* `Submonoid.MulAction`, `Submonoid.DistribMulAction`: a submonoid inherits (distributive)
  multiplicative actions.

### Operations on submonoids

* `Submonoid.comap`: preimage of a submonoid under a monoid homomorphism as a submonoid of the
  domain;
* `Submonoid.map`: image of a submonoid under a monoid homomorphism as a submonoid of the codomain;
* `Submonoid.prod`: product of two submonoids `s : Submonoid M` and `t : Submonoid N` as a submonoid
  of `M × N`;

### Monoid homomorphisms between submonoid

* `Submonoid.subtype`: embedding of a submonoid into the ambient monoid.
* `Submonoid.inclusion`: given two submonoids `S`, `T` such that `S ≤ T`, `S.inclusion T` is the
  inclusion of `S` into `T` as a monoid homomorphism;
* `MulEquiv.submonoidCongr`: converts a proof of `S = T` into a monoid isomorphism between `S`
  and `T`.
* `Submonoid.prodEquiv`: monoid isomorphism between `s.prod t` and `s × t`;

### Operations on `MonoidHom`s

* `MonoidHom.mrange`: range of a monoid homomorphism as a submonoid of the codomain;
* `MonoidHom.mker`: kernel of a monoid homomorphism as a submonoid of the domain;
* `MonoidHom.restrict`: restrict a monoid homomorphism to a submonoid;
* `MonoidHom.codRestrict`: restrict the codomain of a monoid homomorphism to a submonoid;
* `MonoidHom.mrangeRestrict`: restrict a monoid homomorphism to its range;

## Tags

submonoid, range, product, map, comap
-/


variable {M: Type ?u.86057
M N: Type ?u.33229
N P: Type ?u.48758
P : Type _: Type (?u.48755+1)
Type _} [MulOneClass: Type ?u.34652 → Type ?u.34652
MulOneClass M: Type ?u.29
M] [MulOneClass: Type ?u.123590 → Type ?u.123590
MulOneClass N: Type ?u.5
N] [MulOneClass: Type ?u.15878 → Type ?u.15878
MulOneClass P: Type ?u.35
P] (S: Submonoid M
S : Submonoid: (M : Type ?u.181499) → [inst : MulOneClass M] → Type ?u.181499
Submonoid M: Type ?u.2
M)

/-!
### Conversion to/from `Additive`/`Multiplicative`
-/


section

/-- Submonoids of monoid `M` are isomorphic to additive submonoids of `Additive M`. -/
@[simps: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), ↑(↑toAddSubmonoid S) = ↑Additive.toMul ⁻¹' ↑S
simps]
def Submonoid.toAddSubmonoid: {M : Type u_1} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid : Submonoid: (M : Type ?u.58) → [inst : MulOneClass M] → Type ?u.58
Submonoid M: Type ?u.29
M ≃o AddSubmonoid: (M : Type ?u.65) → [inst : AddZeroClass M] → Type ?u.65
AddSubmonoid (Additive: Type ?u.66 → Type ?u.66
Additive M: Type ?u.29
M) where
  toFun S: ?m.183
S :=
    { carrier := Additive.toMul: {α : Type ?u.281} → Additive α ≃ α
Additive.toMul ⁻¹' S: ?m.183
S
      zero_mem' := S: ?m.183
S.one_mem': ∀ {M : Type ?u.552} [inst : MulOneClass M] (self : Submonoid M), 1 ∈ self.carrier
one_mem'
      add_mem' := fun ha: ?m.452
ha hb: ?m.455
hb => S: ?m.183
S.mul_mem': ∀ {M : Type ?u.462} [inst : Mul M] (self : Subsemigroup M) {a b : M},
  a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
mul_mem' ha: ?m.452
ha hb: ?m.455
hb }
  invFun S: ?m.560
S :=
    { carrier := Additive.ofMul: {α : Type ?u.573} → α ≃ Additive α
Additive.ofMul ⁻¹' S: ?m.560
S
      one_mem' := S: ?m.560
S.zero_mem': ∀ {M : Type ?u.756} [inst : AddZeroClass M] (self : AddSubmonoid M), 0 ∈ self.carrier
zero_mem'
      mul_mem' := fun ha: ?m.719
ha hb: ?m.722
hb => S: ?m.560
S.add_mem': ∀ {M : Type ?u.727} [inst : Add M] (self : AddSubsemigroup M) {a b : M},
  a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
add_mem' ha: ?m.719
ha hb: ?m.722
hb}
  left_inv x: ?m.764
x := by
Goals accomplished! 🐙 M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S, x: Submonoid M

(fun S =>
      {
        toSubsemigroup :=
          { carrier := ↑Additive.ofMul ⁻¹' ↑S,
            mul_mem' :=
              (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) },
        one_mem' := (_ : 0 ∈ S.carrier) })
    ((fun S =>
        {
          toAddSubsemigroup :=
            { carrier := ↑Additive.toMul ⁻¹' ↑S,
              add_mem' :=
                (_ :
                  ∀ {a b : Additive M},
                    a ∈ ↑Additive.toMul ⁻¹' ↑S →
                      b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) },
          zero_mem' := (_ : 1 ∈ S.carrier) })
      x) =   xcases x: Submonoid M
xM: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

toSubsemigroup✝: Subsemigroup M

one_mem'✝: 1 ∈ toSubsemigroup✝.carrier

mk(fun S =>
      {
        toSubsemigroup :=
          { carrier := ↑Additive.ofMul ⁻¹' ↑S,
            mul_mem' :=
              (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) },
        one_mem' := (_ : 0 ∈ S.carrier) })
    ((fun S =>
        {
          toAddSubsemigroup :=
            { carrier := ↑Additive.toMul ⁻¹' ↑S,
              add_mem' :=
                (_ :
                  ∀ {a b : Additive M},
                    a ∈ ↑Additive.toMul ⁻¹' ↑S →
                      b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) },
          zero_mem' := (_ : 1 ∈ S.carrier) })
      { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =   { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ };M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

toSubsemigroup✝: Subsemigroup M

one_mem'✝: 1 ∈ toSubsemigroup✝.carrier

mk(fun S =>
      {
        toSubsemigroup :=
          { carrier := ↑Additive.ofMul ⁻¹' ↑S,
            mul_mem' :=
              (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) },
        one_mem' := (_ : 0 ∈ S.carrier) })
    ((fun S =>
        {
          toAddSubsemigroup :=
            { carrier := ↑Additive.toMul ⁻¹' ↑S,
              add_mem' :=
                (_ :
                  ∀ {a b : Additive M},
                    a ∈ ↑Additive.toMul ⁻¹' ↑S →
                      b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) },
          zero_mem' := (_ : 1 ∈ S.carrier) })
      { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =   { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ } M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S, x: Submonoid M

(fun S =>
      {
        toSubsemigroup :=
          { carrier := ↑Additive.ofMul ⁻¹' ↑S,
            mul_mem' :=
              (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) },
        one_mem' := (_ : 0 ∈ S.carrier) })
    ((fun S =>
        {
          toAddSubsemigroup :=
            { carrier := ↑Additive.toMul ⁻¹' ↑S,
              add_mem' :=
                (_ :
                  ∀ {a b : Additive M},
                    a ∈ ↑Additive.toMul ⁻¹' ↑S →
                      b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) },
          zero_mem' := (_ : 1 ∈ S.carrier) })
      x) =   xrfl
Goals accomplished! 🐙
  right_inv x: ?m.770
x := by
Goals accomplished! 🐙 M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

x: AddSubmonoid (Additive M)

(fun S =>
      {
        toAddSubsemigroup :=
          { carrier := ↑Additive.toMul ⁻¹' ↑S,
            add_mem' :=
              (_ :
                ∀ {a b : Additive M},
                  a ∈ ↑Additive.toMul ⁻¹' ↑S →
                    b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) },
        zero_mem' := (_ : 1 ∈ S.carrier) })
    ((fun S =>
        {
          toSubsemigroup :=
            { carrier := ↑Additive.ofMul ⁻¹' ↑S,
              mul_mem' :=
                (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) },
          one_mem' := (_ : 0 ∈ S.carrier) })
      x) =   xcases x: AddSubmonoid (Additive M)
xM: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

toAddSubsemigroup✝: AddSubsemigroup (Additive M)

zero_mem'✝: 0 ∈ toAddSubsemigroup✝.carrier

mk(fun S =>
      {
        toAddSubsemigroup :=
          { carrier := ↑Additive.toMul ⁻¹' ↑S,
            add_mem' :=
              (_ :
                ∀ {a b : Additive M},
                  a ∈ ↑Additive.toMul ⁻¹' ↑S →
                    b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) },
        zero_mem' := (_ : 1 ∈ S.carrier) })
    ((fun S =>
        {
          toSubsemigroup :=
            { carrier := ↑Additive.ofMul ⁻¹' ↑S,
              mul_mem' :=
                (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) },
          one_mem' := (_ : 0 ∈ S.carrier) })
      { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =   { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ };M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

toAddSubsemigroup✝: AddSubsemigroup (Additive M)

zero_mem'✝: 0 ∈ toAddSubsemigroup✝.carrier

mk(fun S =>
      {
        toAddSubsemigroup :=
          { carrier := ↑Additive.toMul ⁻¹' ↑S,
            add_mem' :=
              (_ :
                ∀ {a b : Additive M},
                  a ∈ ↑Additive.toMul ⁻¹' ↑S →
                    b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) },
        zero_mem' := (_ : 1 ∈ S.carrier) })
    ((fun S =>
        {
          toSubsemigroup :=
            { carrier := ↑Additive.ofMul ⁻¹' ↑S,
              mul_mem' :=
                (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) },
          one_mem' := (_ : 0 ∈ S.carrier) })
      { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =   { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ } M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

x: AddSubmonoid (Additive M)

(fun S =>
      {
        toAddSubsemigroup :=
          { carrier := ↑Additive.toMul ⁻¹' ↑S,
            add_mem' :=
              (_ :
                ∀ {a b : Additive M},
                  a ∈ ↑Additive.toMul ⁻¹' ↑S →
                    b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) },
        zero_mem' := (_ : 1 ∈ S.carrier) })
    ((fun S =>
        {
          toSubsemigroup :=
            { carrier := ↑Additive.ofMul ⁻¹' ↑S,
              mul_mem' :=
                (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) },
          one_mem' := (_ : 0 ∈ S.carrier) })
      x) =   xrfl
Goals accomplished! 🐙
  map_rel_iff' := Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align submonoid.to_add_submonoid Submonoid.toAddSubmonoid: {M : Type u_1} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid
#align submonoid.to_add_submonoid_symm_apply_coe Submonoid.toAddSubmonoid_symm_apply_coe: ∀ {M : Type u_1} [inst : MulOneClass M] (S : AddSubmonoid (Additive M)),
  ↑(↑(RelIso.symm Submonoid.toAddSubmonoid) S) = ↑Additive.ofMul ⁻¹' ↑S
Submonoid.toAddSubmonoid_symm_apply_coe
#align submonoid.to_add_submonoid_apply_coe Submonoid.toAddSubmonoid_apply_coe: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), ↑(↑Submonoid.toAddSubmonoid S) = ↑Additive.toMul ⁻¹' ↑S
Submonoid.toAddSubmonoid_apply_coe

/-- Additive submonoids of an additive monoid `Additive M` are isomorphic to submonoids of `M`. -/
abbrev AddSubmonoid.toSubmonoid': {M : Type u_1} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
AddSubmonoid.toSubmonoid' : AddSubmonoid: (M : Type ?u.1222) → [inst : AddZeroClass M] → Type ?u.1222
AddSubmonoid (Additive: Type ?u.1223 → Type ?u.1223
Additive M: Type ?u.1193
M) ≃o Submonoid: (M : Type ?u.1238) → [inst : MulOneClass M] → Type ?u.1238
Submonoid M: Type ?u.1193
M :=
  Submonoid.toAddSubmonoid: {M : Type ?u.1318} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid.symm: {α : Type ?u.1334} → {β : Type ?u.1333} → [inst : LE α] → [inst_1 : LE β] → α ≃o β → β ≃o α
symm
#align add_submonoid.to_submonoid' AddSubmonoid.toSubmonoid': {M : Type u_1} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
AddSubmonoid.toSubmonoid'

theorem Submonoid.toAddSubmonoid_closure: ∀ (S : Set M), ↑toAddSubmonoid (closure S) = AddSubmonoid.closure (↑Additive.toMul ⁻¹' S)
Submonoid.toAddSubmonoid_closure (S: Set M
S : Set: Type ?u.1532 → Type ?u.1532
Set M: Type ?u.1505
M) :
    Submonoid.toAddSubmonoid: {M : Type ?u.1536} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid (Submonoid.closure: {M : Type ?u.1611} → [inst : MulOneClass M] → Set M → Submonoid M
Submonoid.closure S: Set M
S)
      = AddSubmonoid.closure: {M : Type ?u.1639} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
AddSubmonoid.closure (Additive.toMul: {α : Type ?u.1648} → Additive α ≃ α
Additive.toMul ⁻¹' S: Set M
S) :=
  le_antisymm: ∀ {α : Type ?u.1747} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
    (Submonoid.toAddSubmonoid: {M : Type ?u.1780} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid.le_symm_apply: ∀ {α : Type ?u.1795} {β : Type ?u.1796} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x : α} {y : β},
  x ≤ ↑(OrderIso.symm e) y ↔ ↑e x ≤ y
le_symm_apply.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 <|
      Submonoid.closure_le: ∀ {M : Type ?u.1967} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, closure s ≤ S ↔ s ⊆ ↑S
Submonoid.closure_le.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (AddSubmonoid.subset_closure: ∀ {M : Type ?u.1999} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(AddSubmonoid.closure s)
AddSubmonoid.subset_closure (M := Additive: Type ?u.2000 → Type ?u.2000
Additive M: Type ?u.1505
M)))
    (AddSubmonoid.closure_le: ∀ {M : Type ?u.2058} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, AddSubmonoid.closure s ≤ S ↔ s ⊆ ↑S
AddSubmonoid.closure_le.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| Submonoid.subset_closure: ∀ {M : Type ?u.2090} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(closure s)
Submonoid.subset_closure (M := M: Type ?u.1505
M))
#align submonoid.to_add_submonoid_closure Submonoid.toAddSubmonoid_closure: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set M),
  ↑Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (↑Additive.toMul ⁻¹' S)
Submonoid.toAddSubmonoid_closure

theorem AddSubmonoid.toSubmonoid'_closure: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set (Additive M)),
  ↑toSubmonoid' (closure S) = Submonoid.closure (↑Multiplicative.ofAdd ⁻¹' S)
AddSubmonoid.toSubmonoid'_closure (S: Set (Additive M)
S : Set: Type ?u.2156 → Type ?u.2156
Set (Additive: Type ?u.2157 → Type ?u.2157
Additive M: Type ?u.2129
M)) :
    AddSubmonoid.toSubmonoid': {M : Type ?u.2161} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
AddSubmonoid.toSubmonoid' (AddSubmonoid.closure: {M : Type ?u.2236} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
AddSubmonoid.closure S: Set (Additive M)
S)
      = Submonoid.closure: {M : Type ?u.2278} → [inst : MulOneClass M] → Set M → Submonoid M
Submonoid.closure (Multiplicative.ofAdd: {α : Type ?u.2287} → α ≃ Multiplicative α
Multiplicative.ofAdd ⁻¹' S: Set (Additive M)
S) :=
  le_antisymm: ∀ {α : Type ?u.2375} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
    (AddSubmonoid.toSubmonoid': {M : Type ?u.2408} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
AddSubmonoid.toSubmonoid'.le_symm_apply: ∀ {α : Type ?u.2423} {β : Type ?u.2424} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x : α} {y : β},
  x ≤ ↑(OrderIso.symm e) y ↔ ↑e x ≤ y
le_symm_apply.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 <|
      AddSubmonoid.closure_le: ∀ {M : Type ?u.2594} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, closure s ≤ S ↔ s ⊆ ↑S
AddSubmonoid.closure_le.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (Submonoid.subset_closure: ∀ {M : Type ?u.2628} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(Submonoid.closure s)
Submonoid.subset_closure (M := M: Type ?u.2129
M)))
    (Submonoid.closure_le: ∀ {M : Type ?u.2680} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, Submonoid.closure s ≤ S ↔ s ⊆ ↑S
Submonoid.closure_le.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| AddSubmonoid.subset_closure: ∀ {M : Type ?u.2711} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(closure s)
AddSubmonoid.subset_closure (M := Additive: Type ?u.2712 → Type ?u.2712
Additive M: Type ?u.2129
M))
#align add_submonoid.to_submonoid'_closure AddSubmonoid.toSubmonoid'_closure: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set (Additive M)),
  ↑AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S) = Submonoid.closure (↑Multiplicative.ofAdd ⁻¹' S)
AddSubmonoid.toSubmonoid'_closure

end

section

variable {A: Type ?u.2784
A : Type _: Type (?u.2784+1)
Type _} [AddZeroClass: Type ?u.4122 → Type ?u.4122
AddZeroClass A: Type ?u.2784
A]

/-- Additive submonoids of an additive monoid `A` are isomorphic to
multiplicative submonoids of `Multiplicative A`. -/
@[simps: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Submonoid (Multiplicative A)),
  ↑(↑(RelIso.symm toSubmonoid) S) = ↑Multiplicative.ofAdd ⁻¹' ↑S
simps]
def AddSubmonoid.toSubmonoid: {A : Type u_1} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid : AddSubmonoid: (M : Type ?u.2825) → [inst : AddZeroClass M] → Type ?u.2825
AddSubmonoid A: Type ?u.2817
A ≃o Submonoid: (M : Type ?u.2831) → [inst : MulOneClass M] → Type ?u.2831
Submonoid (Multiplicative: Type ?u.2832 → Type ?u.2832
Multiplicative A: Type ?u.2817
A) where
  toFun S: ?m.2949
S :=
    { carrier := Multiplicative.toAdd: {α : Type ?u.2989} → Multiplicative α ≃ α
Multiplicative.toAdd ⁻¹' S: ?m.2949
S
      one_mem' := S: ?m.2949
S.zero_mem': ∀ {M : Type ?u.3217} [inst : AddZeroClass M] (self : AddSubmonoid M), 0 ∈ self.carrier
zero_mem'
      mul_mem' := fun ha: ?m.3160
ha hb: ?m.3163
hb => S: ?m.2949
S.add_mem': ∀ {M : Type ?u.3170} [inst : Add M] (self : AddSubsemigroup M) {a b : M},
  a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
add_mem' ha: ?m.3160
ha hb: ?m.3163
hb }
  invFun S: ?m.3225
S :=
    { carrier := Multiplicative.ofAdd: {α : Type ?u.3238} → α ≃ Multiplicative α
Multiplicative.ofAdd ⁻¹' S: ?m.3225
S
      zero_mem' := S: ?m.3225
S.one_mem': ∀ {M : Type ?u.3421} [inst : MulOneClass M] (self : Submonoid M), 1 ∈ self.carrier
one_mem'
      add_mem' := fun ha: ?m.3384
ha hb: ?m.3387
hb => S: ?m.3225
S.mul_mem': ∀ {M : Type ?u.3392} [inst : Mul M] (self : Subsemigroup M) {a b : M},
  a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
mul_mem' ha: ?m.3384
ha hb: ?m.3387
hb}
  left_inv x: ?m.3429
x := by
Goals accomplished! 🐙 M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

x: AddSubmonoid A

(fun S =>
      {
        toAddSubsemigroup :=
          { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S,
            add_mem' :=
              (_ :
                ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) },
        zero_mem' := (_ : 1 ∈ S.carrier) })
    ((fun S =>
        {
          toSubsemigroup :=
            { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S,
              mul_mem' :=
                (_ :
                  ∀ {a b : Multiplicative A},
                    a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                      b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                        ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) },
          one_mem' := (_ : 0 ∈ S.carrier) })
      x) =   xcases x: AddSubmonoid A
xM: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

toAddSubsemigroup✝: AddSubsemigroup A

zero_mem'✝: 0 ∈ toAddSubsemigroup✝.carrier

mk(fun S =>
      {
        toAddSubsemigroup :=
          { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S,
            add_mem' :=
              (_ :
                ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) },
        zero_mem' := (_ : 1 ∈ S.carrier) })
    ((fun S =>
        {
          toSubsemigroup :=
            { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S,
              mul_mem' :=
                (_ :
                  ∀ {a b : Multiplicative A},
                    a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                      b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                        ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) },
          one_mem' := (_ : 0 ∈ S.carrier) })
      { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =   { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ };M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

toAddSubsemigroup✝: AddSubsemigroup A

zero_mem'✝: 0 ∈ toAddSubsemigroup✝.carrier

mk(fun S =>
      {
        toAddSubsemigroup :=
          { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S,
            add_mem' :=
              (_ :
                ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) },
        zero_mem' := (_ : 1 ∈ S.carrier) })
    ((fun S =>
        {
          toSubsemigroup :=
            { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S,
              mul_mem' :=
                (_ :
                  ∀ {a b : Multiplicative A},
                    a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                      b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                        ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) },
          one_mem' := (_ : 0 ∈ S.carrier) })
      { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =   { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ } M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

x: AddSubmonoid A

(fun S =>
      {
        toAddSubsemigroup :=
          { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S,
            add_mem' :=
              (_ :
                ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) },
        zero_mem' := (_ : 1 ∈ S.carrier) })
    ((fun S =>
        {
          toSubsemigroup :=
            { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S,
              mul_mem' :=
                (_ :
                  ∀ {a b : Multiplicative A},
                    a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                      b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                        ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) },
          one_mem' := (_ : 0 ∈ S.carrier) })
      x) =   xrfl
Goals accomplished! 🐙
  right_inv x: ?m.3435
x := by
Goals accomplished! 🐙 M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

x: Submonoid (Multiplicative A)

(fun S =>
      {
        toSubsemigroup :=
          { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S,
            mul_mem' :=
              (_ :
                ∀ {a b : Multiplicative A},
                  a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                    b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) },
        one_mem' := (_ : 0 ∈ S.carrier) })
    ((fun S =>
        {
          toAddSubsemigroup :=
            { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S,
              add_mem' :=
                (_ :
                  ∀ {a b : A},
                    a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) },
          zero_mem' := (_ : 1 ∈ S.carrier) })
      x) =   xcases x: Submonoid (Multiplicative A)
xM: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

toSubsemigroup✝: Subsemigroup (Multiplicative A)

one_mem'✝: 1 ∈ toSubsemigroup✝.carrier

mk(fun S =>
      {
        toSubsemigroup :=
          { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S,
            mul_mem' :=
              (_ :
                ∀ {a b : Multiplicative A},
                  a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                    b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) },
        one_mem' := (_ : 0 ∈ S.carrier) })
    ((fun S =>
        {
          toAddSubsemigroup :=
            { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S,
              add_mem' :=
                (_ :
                  ∀ {a b : A},
                    a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) },
          zero_mem' := (_ : 1 ∈ S.carrier) })
      { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =   { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ };M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

toSubsemigroup✝: Subsemigroup (Multiplicative A)

one_mem'✝: 1 ∈ toSubsemigroup✝.carrier

mk(fun S =>
      {
        toSubsemigroup :=
          { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S,
            mul_mem' :=
              (_ :
                ∀ {a b : Multiplicative A},
                  a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                    b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) },
        one_mem' := (_ : 0 ∈ S.carrier) })
    ((fun S =>
        {
          toAddSubsemigroup :=
            { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S,
              add_mem' :=
                (_ :
                  ∀ {a b : A},
                    a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) },
          zero_mem' := (_ : 1 ∈ S.carrier) })
      { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =   { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ } M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

x: Submonoid (Multiplicative A)

(fun S =>
      {
        toSubsemigroup :=
          { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S,
            mul_mem' :=
              (_ :
                ∀ {a b : Multiplicative A},
                  a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S →
                    b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) },
        one_mem' := (_ : 0 ∈ S.carrier) })
    ((fun S =>
        {
          toAddSubsemigroup :=
            { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S,
              add_mem' :=
                (_ :
                  ∀ {a b : A},
                    a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) },
          zero_mem' := (_ : 1 ∈ S.carrier) })
      x) =   xrfl
Goals accomplished! 🐙
  map_rel_iff' := Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align add_submonoid.to_submonoid AddSubmonoid.toSubmonoid: {A : Type u_1} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid
#align add_submonoid.to_submonoid_symm_apply_coe AddSubmonoid.toSubmonoid_symm_apply_coe: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Submonoid (Multiplicative A)),
  ↑(↑(RelIso.symm AddSubmonoid.toSubmonoid) S) = ↑Multiplicative.ofAdd ⁻¹' ↑S
AddSubmonoid.toSubmonoid_symm_apply_coe
#align add_submonoid.to_submonoid_apply_coe AddSubmonoid.toSubmonoid_apply_coe: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : AddSubmonoid A),
  ↑(↑AddSubmonoid.toSubmonoid S) = ↑Multiplicative.toAdd ⁻¹' ↑S
AddSubmonoid.toSubmonoid_apply_coe

/-- Submonoids of a monoid `Multiplicative A` are isomorphic to additive submonoids of `A`. -/
abbrev Submonoid.toAddSubmonoid': Submonoid (Multiplicative A) ≃o AddSubmonoid A
Submonoid.toAddSubmonoid' : Submonoid: (M : Type ?u.3839) → [inst : MulOneClass M] → Type ?u.3839
Submonoid (Multiplicative: Type ?u.3840 → Type ?u.3840
Multiplicative A: Type ?u.3831
A) ≃o AddSubmonoid: (M : Type ?u.3855) → [inst : AddZeroClass M] → Type ?u.3855
AddSubmonoid A: Type ?u.3831
A :=
  AddSubmonoid.toSubmonoid: {A : Type ?u.3934} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid.symm: {α : Type ?u.3949} → {β : Type ?u.3948} → [inst : LE α] → [inst_1 : LE β] → α ≃o β → β ≃o α
symm
#align submonoid.to_add_submonoid' Submonoid.toAddSubmonoid': {A : Type u_1} → [inst : AddZeroClass A] → Submonoid (Multiplicative A) ≃o AddSubmonoid A
Submonoid.toAddSubmonoid'

theorem AddSubmonoid.toSubmonoid_closure: ∀ (S : Set A), ↑toSubmonoid (closure S) = Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
AddSubmonoid.toSubmonoid_closure (S: Set A
S : Set: Type ?u.4125 → Type ?u.4125
Set A: Type ?u.4119
A) :
    (AddSubmonoid.toSubmonoid: {A : Type ?u.4129} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid) (AddSubmonoid.closure: {M : Type ?u.4213} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
AddSubmonoid.closure S: Set A
S)
      = Submonoid.closure: {M : Type ?u.4239} → [inst : MulOneClass M] → Set M → Submonoid M
Submonoid.closure (Multiplicative.toAdd: {α : Type ?u.4248} → Multiplicative α ≃ α
Multiplicative.toAdd ⁻¹' S: Set A
S) :=
  le_antisymm: ∀ {α : Type ?u.4347} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
    (AddSubmonoid.toSubmonoid: {A : Type ?u.4380} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid.to_galoisConnection: ∀ {α : Type ?u.4395} {β : Type ?u.4394} [inst : Preorder α] [inst_1 : Preorder β] (oi : α ≃o β),
  GaloisConnection ↑oi ↑(OrderIso.symm oi)
to_galoisConnection.l_le: ∀ {α : Type ?u.4480} {β : Type ?u.4479} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α} {b : β}, a ≤ u b → l a ≤ b
l_le <|
      AddSubmonoid.closure_le: ∀ {M : Type ?u.4586} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, closure s ≤ S ↔ s ⊆ ↑S
AddSubmonoid.closure_le.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| Submonoid.subset_closure: ∀ {M : Type ?u.4619} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(Submonoid.closure s)
Submonoid.subset_closure (M := Multiplicative: Type ?u.4620 → Type ?u.4620
Multiplicative A: Type ?u.4119
A))
    (Submonoid.closure_le: ∀ {M : Type ?u.4678} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, Submonoid.closure s ≤ S ↔ s ⊆ ↑S
Submonoid.closure_le.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| AddSubmonoid.subset_closure: ∀ {M : Type ?u.4709} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(closure s)
AddSubmonoid.subset_closure (M := A: Type ?u.4119
A))
#align add_submonoid.to_submonoid_closure AddSubmonoid.toSubmonoid_closure: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Set A),
  ↑AddSubmonoid.toSubmonoid (AddSubmonoid.closure S) = Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
AddSubmonoid.toSubmonoid_closure

theorem Submonoid.toAddSubmonoid'_closure: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Set (Multiplicative A)),
  ↑toAddSubmonoid' (closure S) = AddSubmonoid.closure (↑Additive.ofMul ⁻¹' S)
Submonoid.toAddSubmonoid'_closure (S: Set (Multiplicative A)
S : Set: Type ?u.4780 → Type ?u.4780
Set (Multiplicative: Type ?u.4781 → Type ?u.4781
Multiplicative A: Type ?u.4774
A)) :
    Submonoid.toAddSubmonoid': {A : Type ?u.4785} → [inst : AddZeroClass A] → Submonoid (Multiplicative A) ≃o AddSubmonoid A
Submonoid.toAddSubmonoid' (Submonoid.closure: {M : Type ?u.4859} → [inst : MulOneClass M] → Set M → Submonoid M
Submonoid.closure S: Set (Multiplicative A)
S)
      = AddSubmonoid.closure: {M : Type ?u.4899} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
AddSubmonoid.closure (Additive.ofMul: {α : Type ?u.4908} → α ≃ Additive α
Additive.ofMul ⁻¹' S: Set (Multiplicative A)
S) :=
  le_antisymm: ∀ {α : Type ?u.4996} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
    (Submonoid.toAddSubmonoid': {A : Type ?u.5029} → [inst : AddZeroClass A] → Submonoid (Multiplicative A) ≃o AddSubmonoid A
Submonoid.toAddSubmonoid'.to_galoisConnection: ∀ {α : Type ?u.5044} {β : Type ?u.5043} [inst : Preorder α] [inst_1 : Preorder β] (oi : α ≃o β),
  GaloisConnection ↑oi ↑(OrderIso.symm oi)
to_galoisConnection.l_le: ∀ {α : Type ?u.5129} {β : Type ?u.5128} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α} {b : β}, a ≤ u b → l a ≤ b
l_le <|
      Submonoid.closure_le: ∀ {M : Type ?u.5234} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, closure s ≤ S ↔ s ⊆ ↑S
Submonoid.closure_le.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| AddSubmonoid.subset_closure: ∀ {M : Type ?u.5269} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(AddSubmonoid.closure s)
AddSubmonoid.subset_closure (M := A: Type ?u.4774
A))
    (AddSubmonoid.closure_le: ∀ {M : Type ?u.5320} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, AddSubmonoid.closure s ≤ S ↔ s ⊆ ↑S
AddSubmonoid.closure_le.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| Submonoid.subset_closure: ∀ {M : Type ?u.5350} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(closure s)
Submonoid.subset_closure (M := Multiplicative: Type ?u.5351 → Type ?u.5351
Multiplicative A: Type ?u.4774
A))
#align submonoid.to_add_submonoid'_closure Submonoid.toAddSubmonoid'_closure: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Set (Multiplicative A)),
  ↑Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (↑Additive.ofMul ⁻¹' S)
Submonoid.toAddSubmonoid'_closure

end

namespace Submonoid

variable {F: Type ?u.5465
F : Type _: Type (?u.23621+1)
Type _} [mc: MonoidHomClass F M N
mc : MonoidHomClass: Type ?u.20871 →
  (M : outParam (Type ?u.20870)) →
    (N : outParam (Type ?u.20869)) →
      [inst : MulOneClass M] → [inst : MulOneClass N] → Type (max(max?u.20871?u.20870)?u.20869)
MonoidHomClass F: Type ?u.22839
F M: Type ?u.21960
M N: Type ?u.5399
N]

open Set

/-!
### `comap` and `map`
-/

/-- The preimage of a submonoid along a monoid homomorphism is a submonoid. -/
@[to_additive: {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid N → AddSubmonoid M
to_additive
      "The preimage of an `AddSubmonoid` along an `AddMonoid` homomorphism is an `AddSubmonoid`."]
def comap: {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap (f: F
f : F: Type ?u.5465
F) (S: Submonoid N
S : Submonoid: (M : Type ?u.5482) → [inst : MulOneClass M] → Type ?u.5482
Submonoid N: Type ?u.5441
N) :
    Submonoid: (M : Type ?u.5491) → [inst : MulOneClass M] → Type ?u.5491
Submonoid M: Type ?u.5438
M where
  carrier := f: F
f ⁻¹' S: Submonoid N
S
  one_mem' := show f: F
f 1: ?m.6442
1 ∈ S: Submonoid N
S by rw [M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

↑f 1 ∈ Smap_one: ∀ {M : Type ?u.7134} {N : Type ?u.7135} {F : Type ?u.7133} [inst : One M] [inst_1 : One N] [inst_2 : OneHomClass F M N]
  (f : F), ↑f 1 = 1
map_oneM: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

1 ∈ S]M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

1 ∈ S;M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

1 ∈ S M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

↑f 1 ∈ Sexact S: Submonoid N
S.one_mem: ∀ {M : Type ?u.7853} [inst : MulOneClass M] (S : Submonoid M), 1 ∈ S
one_mem
Goals accomplished! 🐙
  mul_mem' ha: ?m.5861
ha hb: ?m.5864
hb := show f: F
f (_: ?m.6057
_ * _: ?m.6060
_) ∈ S: Submonoid N
S by rw [M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S

↑f (a✝ * b✝) ∈ Smap_mul: ∀ {M : Type ?u.6689} {N : Type ?u.6690} {F : Type ?u.6688} [inst : Mul M] [inst_1 : Mul N] [inst_2 : MulHomClass F M N]
  (f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f y
map_mulM: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S

↑f a✝ * ↑f b✝ ∈ S]M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S

↑f a✝ * ↑f b✝ ∈ S;M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S

↑f a✝ * ↑f b✝ ∈ S M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S

↑f (a✝ * b✝) ∈ Sexact S: Submonoid N
S.mul_mem: ∀ {M : Type ?u.7111} [inst : MulOneClass M] (S : Submonoid M) {x y : M}, x ∈ S → y ∈ S → x * y ∈ S
mul_mem ha: a✝ ∈ ↑f ⁻¹' ↑S
ha hb: b✝ ∈ ↑f ⁻¹' ↑S
hb
Goals accomplished! 🐙
#align submonoid.comap Submonoid.comap: {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
Submonoid.comap
#align add_submonoid.comap AddSubmonoid.comap: {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid N → AddSubmonoid M
AddSubmonoid.comap

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F), ↑(AddSubmonoid.comap f S) = ↑f ⁻¹' ↑S
to_additive (attr := simp)]
theorem coe_comap: ∀ (S : Submonoid N) (f : F), ↑(comap f S) = ↑f ⁻¹' ↑S
coe_comap (S: Submonoid N
S : Submonoid: (M : Type ?u.8191) → [inst : MulOneClass M] → Type ?u.8191
Submonoid N: Type ?u.8152
N) (f: F
f : F: Type ?u.8176
F) : (S: Submonoid N
S.comap: {M : Type ?u.8207} →
  {N : Type ?u.8206} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.8205} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f : Set: Type ?u.8204 → Type ?u.8204
Set M: Type ?u.8149
M) = f: F
f ⁻¹' S: Submonoid N
S :=
  rfl: ∀ {α : Sort ?u.8679} {a : α}, a = a
rfl
#align submonoid.coe_comap Submonoid.coe_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (S : Submonoid N) (f : F), ↑(comap f S) = ↑f ⁻¹' ↑S
Submonoid.coe_comap
#align add_submonoid.coe_comap AddSubmonoid.coe_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F), ↑(AddSubmonoid.comap f S) = ↑f ⁻¹' ↑S
AddSubmonoid.coe_comap

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M}, x ∈ AddSubmonoid.comap f S ↔ ↑f x ∈ S
to_additive (attr := simp)]
theorem mem_comap: ∀ {S : Submonoid N} {f : F} {x : M}, x ∈ comap f S ↔ ↑f x ∈ S
mem_comap {S: Submonoid N
S : Submonoid: (M : Type ?u.8832) → [inst : MulOneClass M] → Type ?u.8832
Submonoid N: Type ?u.8793
N} {f: F
f : F: Type ?u.8817
F} {x: M
x : M: Type ?u.8790
M} : x: M
x ∈ S: Submonoid N
S.comap: {M : Type ?u.8852} →
  {N : Type ?u.8851} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.8850} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f ↔ f: F
f x: M
x ∈ S: Submonoid N
S :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align submonoid.mem_comap Submonoid.mem_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M}, x ∈ comap f S ↔ ↑f x ∈ S
Submonoid.mem_comap
#align add_submonoid.mem_comap AddSubmonoid.mem_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M}, x ∈ AddSubmonoid.comap f S ↔ ↑f x ∈ S
AddSubmonoid.mem_comap

@[to_additive: ∀ {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (S : AddSubmonoid P) (g : N →+ P) (f : M →+ N),
  AddSubmonoid.comap f (AddSubmonoid.comap g S) = AddSubmonoid.comap (AddMonoidHom.comp g f) S
to_additive]
theorem comap_comap: ∀ (S : Submonoid P) (g : N →* P) (f : M →* N), comap f (comap g S) = comap (MonoidHom.comp g f) S
comap_comap (S: Submonoid P
S : Submonoid: (M : Type ?u.9377) → [inst : MulOneClass M] → Type ?u.9377
Submonoid P: Type ?u.9341
P) (g: N →* P
g : N: Type ?u.9338
N →* P: Type ?u.9341
P) (f: M →* N
f : M: Type ?u.9335
M →* N: Type ?u.9338
N) :
    (S: Submonoid P
S.comap: {M : Type ?u.9411} →
  {N : Type ?u.9410} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.9409} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap g: N →* P
g).comap: {M : Type ?u.9484} →
  {N : Type ?u.9483} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.9482} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: M →* N
f = S: Submonoid P
S.comap: {M : Type ?u.9556} →
  {N : Type ?u.9555} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.9554} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap (g: N →* P
g.comp: {M : Type ?u.9573} →
  {N : Type ?u.9572} →
    {P : Type ?u.9571} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp f: M →* N
f) :=
  rfl: ∀ {α : Sort ?u.9663} {a : α}, a = a
rfl
#align submonoid.comap_comap Submonoid.comap_comap: ∀ {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (S : Submonoid P) (g : N →* P) (f : M →* N), comap f (comap g S) = comap (MonoidHom.comp g f) S
Submonoid.comap_comap
#align add_submonoid.comap_comap AddSubmonoid.comap_comap: ∀ {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (S : AddSubmonoid P) (g : N →+ P) (f : M →+ N),
  AddSubmonoid.comap f (AddSubmonoid.comap g S) = AddSubmonoid.comap (AddMonoidHom.comp g f) S
AddSubmonoid.comap_comap

@[to_additive: ∀ {P : Type u_1} [inst : AddZeroClass P] (S : AddSubmonoid P), AddSubmonoid.comap (AddMonoidHom.id P) S = S
to_additive (attr := simp)]
theorem comap_id: ∀ (S : Submonoid P), comap (MonoidHom.id P) S = S
comap_id (S: Submonoid P
S : Submonoid: (M : Type ?u.9824) → [inst : MulOneClass M] → Type ?u.9824
Submonoid P: Type ?u.9788
P) : S: Submonoid P
S.comap: {M : Type ?u.9836} →
  {N : Type ?u.9835} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.9834} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap (MonoidHom.id: (M : Type ?u.9851) → [inst : MulOneClass M] → M →* M
MonoidHom.id P: Type ?u.9788
P) = S: Submonoid P
S :=
  ext: ∀ {M : Type ?u.9911} [inst : MulOneClass M] {S T : Submonoid M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
ext (by
Goals accomplished! 🐙 M: Type ?u.9782

N: Type ?u.9785

P: Type u_1

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.9809

mc: MonoidHomClass F M N

S: Submonoid P

∀ (x : P), x ∈ comap (MonoidHom.id P) S ↔ x ∈ Ssimp
Goals accomplished! 🐙)
#align submonoid.comap_id Submonoid.comap_id: ∀ {P : Type u_1} [inst : MulOneClass P] (S : Submonoid P), comap (MonoidHom.id P) S = S
Submonoid.comap_id
#align add_submonoid.comap_id AddSubmonoid.comap_id: ∀ {P : Type u_1} [inst : AddZeroClass P] (S : AddSubmonoid P), AddSubmonoid.comap (AddMonoidHom.id P) S = S
AddSubmonoid.comap_id

/-- The image of a submonoid along a monoid homomorphism is a submonoid. -/
@[to_additive: {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid M → AddSubmonoid N
to_additive
      "The image of an `AddSubmonoid` along an `AddMonoid` homomorphism is an `AddSubmonoid`."]
def map: {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map (f: F
f : F: Type ?u.10959
F) (S: Submonoid M
S : Submonoid: (M : Type ?u.10976) → [inst : MulOneClass M] → Type ?u.10976
Submonoid M: Type ?u.10932
M) :
    Submonoid: (M : Type ?u.10985) → [inst : MulOneClass M] → Type ?u.10985
Submonoid N: Type ?u.10935
N where
  carrier := f: F
f '' S: Submonoid M
S
  one_mem' := ⟨1: ?m.11366
1, S: Submonoid M
S.one_mem: ∀ {M : Type ?u.11601} [inst : MulOneClass M] (S : Submonoid M), 1 ∈ S
one_mem, map_one: ∀ {M : Type ?u.11610} {N : Type ?u.11611} {F : Type ?u.11609} [inst : One M] [inst_1 : One N]
  [inst_2 : OneHomClass F M N] (f : F), ↑f 1 = 1
map_one f: F
f⟩
  mul_mem' := by
Goals accomplished! 🐙
    M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a * b ∈ ↑f '' ↑Srintro _: N
_ _: N
_ ⟨x, hx, rfl⟩: x ∈ ↑S ∧ ↑f x = a✝
⟨x: M
x⟨x, hx, rfl⟩: x ∈ ↑S ∧ ↑f x = a✝
, hx: x ∈ ↑S
hx⟨x, hx, rfl⟩: x ∈ ↑S ∧ ↑f x = a✝
, rfl: ↑f x = a✝
rfl⟨x, hx, rfl⟩: x ∈ ↑S ∧ ↑f x = a✝
⟩ ⟨y, hy, rfl⟩: b✝ ∈ ↑f '' ↑S
⟨y: M
y⟨y, hy, rfl⟩: b✝ ∈ ↑f '' ↑S
, hy: y ∈ ↑S
hy⟨y, hy, rfl⟩: b✝ ∈ ↑f '' ↑S
, rfl: ↑f y = b✝
rfl⟨y, hy, rfl⟩: b✝ ∈ ↑f '' ↑S
⟩M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S

intro.intro.intro.intro↑f x * ↑f y ∈ ↑f '' ↑S;M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S

intro.intro.intro.intro↑f x * ↑f y ∈ ↑f '' ↑S
    M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a * b ∈ ↑f '' ↑Sexact ⟨x: M
x * y: M
y, S: Submonoid M
S.mul_mem: ∀ {M : Type ?u.12419} [inst : MulOneClass M] (S : Submonoid M) {x y : M}, x ∈ S → y ∈ S → x * y ∈ S
mul_mem hx: x ∈ ↑S
hx hy: y ∈ ↑S
hy, M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S

intro.intro.intro.intro↑f x * ↑f y ∈ ↑f '' ↑Sby
Goals accomplished! 🐙 M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S

↑f (x * y) = ↑f x * ↑f yrw [M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S

↑f (x * y) = ↑f x * ↑f ymap_mul: ∀ {M : Type ?u.12448} {N : Type ?u.12449} {F : Type ?u.12447} [inst : Mul M] [inst_1 : Mul N]
  [inst_2 : MulHomClass F M N] (f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f y
map_mulM: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S

↑f x * ↑f y = ↑f x * ↑f y]
Goals accomplished! 🐙⟩
Goals accomplished! 🐙
#align submonoid.map Submonoid.map: {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
Submonoid.map
#align add_submonoid.map AddSubmonoid.map: {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid M → AddSubmonoid N
AddSubmonoid.map

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M), ↑(AddSubmonoid.map f S) = ↑f '' ↑S
to_additive (attr := simp)]
theorem coe_map: ∀ (f : F) (S : Submonoid M), ↑(map f S) = ↑f '' ↑S
coe_map (f: F
f : F: Type ?u.13199
F) (S: Submonoid M
S : Submonoid: (M : Type ?u.13216) → [inst : MulOneClass M] → Type ?u.13216
Submonoid M: Type ?u.13172
M) : (S: Submonoid M
S.map: {M : Type ?u.13230} →
  {N : Type ?u.13229} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.13228} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f : Set: Type ?u.13227 → Type ?u.13227
Set N: Type ?u.13175
N) = f: F
f '' S: Submonoid M
S :=
  rfl: ∀ {α : Sort ?u.13702} {a : α}, a = a
rfl
#align submonoid.coe_map Submonoid.coe_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M), ↑(map f S) = ↑f '' ↑S
Submonoid.coe_map
#align add_submonoid.coe_map AddSubmonoid.coe_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M), ↑(AddSubmonoid.map f S) = ↑f '' ↑S
AddSubmonoid.coe_map

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N}, y ∈ AddSubmonoid.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
to_additive (attr := simp)]
theorem mem_map: ∀ {f : F} {S : Submonoid M} {y : N}, y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
mem_map {f: F
f : F: Type ?u.13840
F} {S: Submonoid M
S : Submonoid: (M : Type ?u.13857) → [inst : MulOneClass M] → Type ?u.13857
Submonoid M: Type ?u.13813
M} {y: N
y : N: Type ?u.13816
N} : y: N
y ∈ S: Submonoid M
S.map: {M : Type ?u.13875} →
  {N : Type ?u.13874} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.13873} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f ↔ ∃ x: ?m.14003
x ∈ S: Submonoid M
S, f: F
f x: ?m.14003
x = y: N
y := by
Goals accomplished! 🐙
  M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N

y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = yrw [M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N

y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y← bex_def: ∀ {α : Sort ?u.14222} {p q : α → Prop}, (∃ x x_1, q x) ↔ ∃ x, p x ∧ q x
bex_defM: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N

y ∈ map f S ↔ ∃ x x_1, ↑f x = y]M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N

y ∈ map f S ↔ ∃ x x_1, ↑f x = y
  M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N

y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = yexact mem_image_iff_bex: ∀ {α : Type ?u.14262} {β : Type ?u.14263} {f : α → β} {s : Set α} {y : β}, y ∈ f '' s ↔ ∃ x x_1, f x = y
mem_image_iff_bex
Goals accomplished! 🐙
#align submonoid.mem_map Submonoid.mem_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N}, y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
Submonoid.mem_map
#align add_submonoid.mem_map AddSubmonoid.mem_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N}, y ∈ AddSubmonoid.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
AddSubmonoid.mem_map

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F) {S : AddSubmonoid M} {x : M}, x ∈ S → ↑f x ∈ AddSubmonoid.map f S
to_additive]
theorem mem_map_of_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M}, x ∈ S → ↑f x ∈ map f S
mem_map_of_mem (f: F
f : F: Type ?u.14498
F) {S: Submonoid M
S : Submonoid: (M : Type ?u.14515) → [inst : MulOneClass M] → Type ?u.14515
Submonoid M: Type ?u.14471
M} {x: M
x : M: Type ?u.14471
M} (hx: x ∈ S
hx : x: M
x ∈ S: Submonoid M
S) : f: F
f x: M
x ∈ S: Submonoid M
S.map: {M : Type ?u.14771} →
  {N : Type ?u.14770} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.14769} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f :=
  mem_image_of_mem: ∀ {α : Type ?u.14896} {β : Type ?u.14897} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem f: F
f hx: x ∈ S
hx
#align submonoid.mem_map_of_mem Submonoid.mem_map_of_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M}, x ∈ S → ↑f x ∈ map f S
Submonoid.mem_map_of_mem
#align add_submonoid.mem_map_of_mem AddSubmonoid.mem_map_of_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F) {S : AddSubmonoid M} {x : M}, x ∈ S → ↑f x ∈ AddSubmonoid.map f S
AddSubmonoid.mem_map_of_mem

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : { x // x ∈ S }), ↑f ↑x ∈ AddSubmonoid.map f S
to_additive]
theorem apply_coe_mem_map: ∀ (f : F) (S : Submonoid M) (x : { x // x ∈ S }), ↑f ↑x ∈ map f S
apply_coe_mem_map (f: F
f : F: Type ?u.15208
F) (S: Submonoid M
S : Submonoid: (M : Type ?u.15225) → [inst : MulOneClass M] → Type ?u.15225
Submonoid M: Type ?u.15181
M) (x: { x // x ∈ S }
x : S: Submonoid M
S) : f: F
f x: { x // x ∈ S }
x ∈ S: Submonoid M
S.map: {M : Type ?u.15578} →
  {N : Type ?u.15577} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.15576} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f :=
  mem_map_of_mem: ∀ {M : Type ?u.15703} {N : Type ?u.15704} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.15705}
  [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M}, x ∈ S → ↑f x ∈ map f S
mem_map_of_mem f: F
f x: { x // x ∈ S }
x.2: ∀ {α : Sort ?u.15789} {p : α → Prop} (self : Subtype p), p ↑self
2
#align submonoid.apply_coe_mem_map Submonoid.apply_coe_mem_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) (x : { x // x ∈ S }), ↑f ↑x ∈ map f S
Submonoid.apply_coe_mem_map
#align add_submonoid.apply_coe_mem_map AddSubmonoid.apply_coe_mem_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : { x // x ∈ S }), ↑f ↑x ∈ AddSubmonoid.map f S
AddSubmonoid.apply_coe_mem_map

@[to_additive: ∀ {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (S : AddSubmonoid M) (g : N →+ P) (f : M →+ N),
  AddSubmonoid.map g (AddSubmonoid.map f S) = AddSubmonoid.map (AddMonoidHom.comp g f) S
to_additive]
theorem map_map: ∀ {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (S : Submonoid M) (g : N →* P) (f : M →* N), map g (map f S) = map (MonoidHom.comp g f) S
map_map (g: N →* P
g : N: Type ?u.15866
N →* P: Type ?u.15869
P) (f: M →* N
f : M: Type ?u.15863
M →* N: Type ?u.15866
N) : (S: Submonoid M
S.map: {M : Type ?u.15935} →
  {N : Type ?u.15934} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.15933} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: M →* N
f).map: {M : Type ?u.16008} →
  {N : Type ?u.16007} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.16006} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map g: N →* P
g = S: Submonoid M
S.map: {M : Type ?u.16080} →
  {N : Type ?u.16079} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.16078} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map (g: N →* P
g.comp: {M : Type ?u.16097} →
  {N : Type ?u.16096} →
    {P : Type ?u.16095} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp f: M →* N
f) :=
  SetLike.coe_injective: ∀ {A : Type ?u.16186} {B : Type ?u.16187} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective <| image_image: ∀ {α : Type ?u.16206} {β : Type ?u.16208} {γ : Type ?u.16207} (g : β → γ) (f : α → β) (s : Set α),
  g '' (f '' s) = (fun x => g (f x)) '' s
image_image _: ?m.16210 → ?m.16211
_ _: ?m.16209 → ?m.16210
_ _: Set ?m.16209
_
#align submonoid.map_map Submonoid.map_map: ∀ {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (S : Submonoid M) (g : N →* P) (f : M →* N), map g (map f S) = map (MonoidHom.comp g f) S
Submonoid.map_map
#align add_submonoid.map_map AddSubmonoid.map_map: ∀ {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (S : AddSubmonoid M) (g : N →+ P) (f : M →+ N),
  AddSubmonoid.map g (AddSubmonoid.map f S) = AddSubmonoid.map (AddMonoidHom.comp g f) S
AddSubmonoid.map_map

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ↑f → ∀ {S : AddSubmonoid M} {x : M}, ↑f x ∈ AddSubmonoid.map f S ↔ x ∈ S
to_additive]
theorem mem_map_iff_mem: ∀ {f : F}, Function.Injective ↑f → ∀ {S : Submonoid M} {x : M}, ↑f x ∈ map f S ↔ x ∈ S
mem_map_iff_mem {f: F
f : F: Type ?u.16377
F} (hf: Function.Injective ↑f
hf : Function.Injective: {α : Sort ?u.16395} → {β : Sort ?u.16394} → (α → β) → Prop
Function.Injective f: F
f) {S: Submonoid M
S : Submonoid: (M : Type ?u.16587) → [inst : MulOneClass M] → Type ?u.16587
Submonoid M: Type ?u.16350
M} {x: M
x : M: Type ?u.16350
M} :
    f: F
f x: M
x ∈ S: Submonoid M
S.map: {M : Type ?u.16774} →
  {N : Type ?u.16773} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.16772} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f ↔ x: M
x ∈ S: Submonoid M
S :=
  hf: Function.Injective ↑f
hf.mem_set_image: ∀ {α : Type ?u.16922} {β : Type ?u.16923} {f : α → β},
  Function.Injective f → ∀ {s : Set α} {a : α}, f a ∈ f '' s ↔ a ∈ s
mem_set_image
#align submonoid.mem_map_iff_mem Submonoid.mem_map_iff_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F}, Function.Injective ↑f → ∀ {S : Submonoid M} {x : M}, ↑f x ∈ map f S ↔ x ∈ S
Submonoid.mem_map_iff_mem
#align add_submonoid.mem_map_iff_mem AddSubmonoid.mem_map_iff_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ↑f → ∀ {S : AddSubmonoid M} {x : M}, ↑f x ∈ AddSubmonoid.map f S ↔ x ∈ S
AddSubmonoid.mem_map_iff_mem

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N},
  AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f T
to_additive]
theorem map_le_iff_le_comap: ∀ {f : F} {S : Submonoid M} {T : Submonoid N}, map f S ≤ T ↔ S ≤ comap f T
map_le_iff_le_comap {f: F
f : F: Type ?u.17062
F} {S: Submonoid M
S : Submonoid: (M : Type ?u.17079) → [inst : MulOneClass M] → Type ?u.17079
Submonoid M: Type ?u.17035
M} {T: Submonoid N
T : Submonoid: (M : Type ?u.17088) → [inst : MulOneClass M] → Type ?u.17088
Submonoid N: Type ?u.17038
N} :
    S: Submonoid M
S.map: {M : Type ?u.17100} →
  {N : Type ?u.17099} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.17098} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f ≤ T: Submonoid N
T ↔ S: Submonoid M
S ≤ T: Submonoid N
T.comap: {M : Type ?u.17204} →
  {N : Type ?u.17203} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.17202} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f :=
  image_subset_iff: ∀ {α : Type ?u.17300} {β : Type ?u.17301} {s : Set α} {t : Set β} {f : α → β}, f '' s ⊆ t ↔ s ⊆ f ⁻¹' t
image_subset_iff
#align submonoid.map_le_iff_le_comap Submonoid.map_le_iff_le_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N}, map f S ≤ T ↔ S ≤ comap f T
Submonoid.map_le_iff_le_comap
#align add_submonoid.map_le_iff_le_comap AddSubmonoid.map_le_iff_le_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N},
  AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f T
AddSubmonoid.map_le_iff_le_comap

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F), GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)
to_additive]
theorem gc_map_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap (f: F
f : F: Type ?u.17445
F) : GaloisConnection: {α : Type ?u.17463} → {β : Type ?u.17462} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection (map: {M : Type ?u.17500} →
  {N : Type ?u.17499} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.17498} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f) (comap: {M : Type ?u.17619} →
  {N : Type ?u.17618} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.17617} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f) := fun _: ?m.17768
_ _: ?m.17771
_ => map_le_iff_le_comap: ∀ {M : Type ?u.17773} {N : Type ?u.17774} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.17775}
  [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N}, map f S ≤ T ↔ S ≤ comap f T
map_le_iff_le_comap
#align submonoid.gc_map_comap Submonoid.gc_map_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
Submonoid.gc_map_comap
#align add_submonoid.gc_map_comap AddSubmonoid.gc_map_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F), GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)
AddSubmonoid.gc_map_comap

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F}, S ≤ AddSubmonoid.comap f T → AddSubmonoid.map f S ≤ T
to_additive]
theorem map_le_of_le_comap: ∀ {T : Submonoid N} {f : F}, S ≤ comap f T → map f S ≤ T
map_le_of_le_comap {T: Submonoid N
T : Submonoid: (M : Type ?u.17971) → [inst : MulOneClass M] → Type ?u.17971
Submonoid N: Type ?u.17932
N} {f: F
f : F: Type ?u.17956
F} : S: Submonoid M
S ≤ T: Submonoid N
T.comap: {M : Type ?u.17986} →
  {N : Type ?u.17985} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.17984} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f → S: Submonoid M
S.map: {M : Type ?u.18096} →
  {N : Type ?u.18095} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.18094} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f ≤ T: Submonoid N
T :=
  (gc_map_comap: ∀ {M : Type ?u.18194} {N : Type ?u.18195} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.18196}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).l_le: ∀ {α : Type ?u.18258} {β : Type ?u.18257} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α} {b : β}, a ≤ u b → l a ≤ b
l_le
#align submonoid.map_le_of_le_comap Submonoid.map_le_of_le_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3}
  [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F}, S ≤ comap f T → map f S ≤ T
Submonoid.map_le_of_le_comap
#align add_submonoid.map_le_of_le_comap AddSubmonoid.map_le_of_le_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F}, S ≤ AddSubmonoid.comap f T → AddSubmonoid.map f S ≤ T
AddSubmonoid.map_le_of_le_comap

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F}, AddSubmonoid.map f S ≤ T → S ≤ AddSubmonoid.comap f T
to_additive]
theorem le_comap_of_map_le: ∀ {T : Submonoid N} {f : F}, map f S ≤ T → S ≤ comap f T
le_comap_of_map_le {T: Submonoid N
T : Submonoid: (M : Type ?u.18482) → [inst : MulOneClass M] → Type ?u.18482
Submonoid N: Type ?u.18443
N} {f: F
f : F: Type ?u.18467
F} : S: Submonoid M
S.map: {M : Type ?u.18497} →
  {N : Type ?u.18496} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.18495} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f ≤ T: Submonoid N
T → S: Submonoid M
S ≤ T: Submonoid N
T.comap: {M : Type ?u.18607} →
  {N : Type ?u.18606} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.18605} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f :=
  (gc_map_comap: ∀ {M : Type ?u.18705} {N : Type ?u.18706} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.18707}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).le_u: ∀ {α : Type ?u.18769} {β : Type ?u.18768} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α} {b : β}, l a ≤ b → a ≤ u b
le_u
#align submonoid.le_comap_of_map_le Submonoid.le_comap_of_map_le: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3}
  [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F}, map f S ≤ T → S ≤ comap f T
Submonoid.le_comap_of_map_le
#align add_submonoid.le_comap_of_map_le AddSubmonoid.le_comap_of_map_le: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F}, AddSubmonoid.map f S ≤ T → S ≤ AddSubmonoid.comap f T
AddSubmonoid.le_comap_of_map_le

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F}, S ≤ AddSubmonoid.comap f (AddSubmonoid.map f S)
to_additive]
theorem le_comap_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F}, S ≤ comap f (map f S)
le_comap_map {f: F
f : F: Type ?u.18978
F} : S: Submonoid M
S ≤ (S: Submonoid M
S.map: {M : Type ?u.18998} →
  {N : Type ?u.18997} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.18996} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f).comap: {M : Type ?u.19061} →
  {N : Type ?u.19060} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.19059} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f :=
  (gc_map_comap: ∀ {M : Type ?u.19162} {N : Type ?u.19163} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.19164}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).le_u_l: ∀ {α : Type ?u.19226} {β : Type ?u.19225} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ (a : α), a ≤ u (l a)
le_u_l _: ?m.19235
_
#align submonoid.le_comap_map Submonoid.le_comap_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F}, S ≤ comap f (map f S)
Submonoid.le_comap_map
#align add_submonoid.le_comap_map AddSubmonoid.le_comap_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F}, S ≤ AddSubmonoid.comap f (AddSubmonoid.map f S)
AddSubmonoid.le_comap_map

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F}, AddSubmonoid.map f (AddSubmonoid.comap f S) ≤ S
to_additive]
theorem map_comap_le: ∀ {S : Submonoid N} {f : F}, map f (comap f S) ≤ S
map_comap_le {S: Submonoid N
S : Submonoid: (M : Type ?u.19433) → [inst : MulOneClass M] → Type ?u.19433
Submonoid N: Type ?u.19394
N} {f: F
f : F: Type ?u.19418
F} : (S: Submonoid N
S.comap: {M : Type ?u.19447} →
  {N : Type ?u.19446} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.19445} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f).map: {M : Type ?u.19505} →
  {N : Type ?u.19504} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.19503} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f ≤ S: Submonoid N
S :=
  (gc_map_comap: ∀ {M : Type ?u.19608} {N : Type ?u.19609} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.19610}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).l_u_le: ∀ {α : Type ?u.19672} {β : Type ?u.19671} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ (a : β), l (u a) ≤ a
l_u_le _: ?m.19682
_
#align submonoid.map_comap_le Submonoid.map_comap_le: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F}, map f (comap f S) ≤ S
Submonoid.map_comap_le
#align add_submonoid.map_comap_le AddSubmonoid.map_comap_le: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F}, AddSubmonoid.map f (AddSubmonoid.comap f S) ≤ S
AddSubmonoid.map_comap_le

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.map f)
to_additive]
theorem monotone_map: ∀ {f : F}, Monotone (map f)
monotone_map {f: F
f : F: Type ?u.19870
F} : Monotone: {α : Type ?u.19888} → {β : Type ?u.19887} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone (map: {M : Type ?u.19925} →
  {N : Type ?u.19924} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.19923} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f) :=
  (gc_map_comap: ∀ {M : Type ?u.20119} {N : Type ?u.20120} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.20121}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).monotone_l: ∀ {α : Type ?u.20183} {β : Type ?u.20182} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → Monotone l
monotone_l
#align submonoid.monotone_map Submonoid.monotone_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F}, Monotone (map f)
Submonoid.monotone_map
#align add_submonoid.monotone_map AddSubmonoid.monotone_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.map f)
AddSubmonoid.monotone_map

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.comap f)
to_additive]
theorem monotone_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F}, Monotone (comap f)
monotone_comap {f: F
f : F: Type ?u.20368
F} : Monotone: {α : Type ?u.20386} → {β : Type ?u.20385} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone (comap: {M : Type ?u.20423} →
  {N : Type ?u.20422} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.20421} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f) :=
  (gc_map_comap: ∀ {M : Type ?u.20617} {N : Type ?u.20618} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.20619}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).monotone_u: ∀ {α : Type ?u.20681} {β : Type ?u.20680} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → Monotone u
monotone_u
#align submonoid.monotone_comap Submonoid.monotone_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F}, Monotone (comap f)
Submonoid.monotone_comap
#align add_submonoid.monotone_comap AddSubmonoid.monotone_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.comap f)
AddSubmonoid.monotone_comap

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F},
  AddSubmonoid.map f (AddSubmonoid.comap f (AddSubmonoid.map f S)) = AddSubmonoid.map f S
to_additive (attr := simp)]
theorem map_comap_map: ∀ {f : F}, map f (comap f (map f S)) = map f S
map_comap_map {f: F
f : F: Type ?u.20866
F} : ((S: Submonoid M
S.map: {M : Type ?u.20886} →
  {N : Type ?u.20885} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.20884} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f).comap: {M : Type ?u.20949} →
  {N : Type ?u.20948} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.20947} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f).map: {M : Type ?u.21005} →
  {N : Type ?u.21004} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.21003} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f = S: Submonoid M
S.map: {M : Type ?u.21055} →
  {N : Type ?u.21054} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.21053} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f :=
  (gc_map_comap: ∀ {M : Type ?u.21106} {N : Type ?u.21107} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.21108}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).l_u_l_eq_l: ∀ {α : Type ?u.21170} {β : Type ?u.21169} [inst : Preorder α] [inst_1 : PartialOrder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ (a : α), l (u (l a)) = l a
l_u_l_eq_l _: ?m.21179
_
#align submonoid.map_comap_map Submonoid.map_comap_map: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F}, map f (comap f (map f S)) = map f S
Submonoid.map_comap_map
#align add_submonoid.map_comap_map AddSubmonoid.map_comap_map: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F},
  AddSubmonoid.map f (AddSubmonoid.comap f (AddSubmonoid.map f S)) = AddSubmonoid.map f S
AddSubmonoid.map_comap_map

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F},
  AddSubmonoid.comap f (AddSubmonoid.map f (AddSubmonoid.comap f S)) = AddSubmonoid.comap f S
to_additive (attr := simp)]
theorem comap_map_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F}, comap f (map f (comap f S)) = comap f S
comap_map_comap {S: Submonoid N
S : Submonoid: (M : Type ?u.21440) → [inst : MulOneClass M] → Type ?u.21440
Submonoid N: Type ?u.21401
N} {f: F
f : F: Type ?u.21425
F} : ((S: Submonoid N
S.comap: {M : Type ?u.21454} →
  {N : Type ?u.21453} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.21452} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f).map: {M : Type ?u.21512} →
  {N : Type ?u.21511} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.21510} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f).comap: {M : Type ?u.21568} →
  {N : Type ?u.21567} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.21566} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f = S: Submonoid N
S.comap: {M : Type ?u.21618} →
  {N : Type ?u.21617} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.21616} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f :=
  (gc_map_comap: ∀ {M : Type ?u.21670} {N : Type ?u.21671} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.21672}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).u_l_u_eq_u: ∀ {α : Type ?u.21734} {β : Type ?u.21733} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ (b : β), u (l (u b)) = u b
u_l_u_eq_u _: ?m.21744
_
#align submonoid.comap_map_comap Submonoid.comap_map_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F}, comap f (map f (comap f S)) = comap f S
Submonoid.comap_map_comap
#align add_submonoid.comap_map_comap AddSubmonoid.comap_map_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F},
  AddSubmonoid.comap f (AddSubmonoid.map f (AddSubmonoid.comap f S)) = AddSubmonoid.comap f S
AddSubmonoid.comap_map_comap

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid M) (f : F),
  AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f T
to_additive]
theorem map_sup: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (S T : Submonoid M) (f : F), map f (S ⊔ T) = map f S ⊔ map f T
map_sup (S: Submonoid M
S T: Submonoid M
T : Submonoid: (M : Type ?u.22011) → [inst : MulOneClass M] → Type ?u.22011
Submonoid M: Type ?u.21960
M) (f: F
f : F: Type ?u.21987
F) : (S: Submonoid M
S ⊔ T: Submonoid M
T).map: {M : Type ?u.22056} →
  {N : Type ?u.22055} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.22054} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f = S: Submonoid M
S.map: {M : Type ?u.22119} →
  {N : Type ?u.22118} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.22117} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f ⊔ T: Submonoid M
T.map: {M : Type ?u.22213} →
  {N : Type ?u.22212} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.22211} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f :=
  (gc_map_comap: ∀ {M : Type ?u.22626} {N : Type ?u.22627} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.22628}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f : GaloisConnection: {α : Type ?u.22325} → {β : Type ?u.22324} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection (map: {M : Type ?u.22362} →
  {N : Type ?u.22361} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.22360} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f) (comap: {M : Type ?u.22481} →
  {N : Type ?u.22480} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.22479} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f)).l_sup: ∀ {α : Type ?u.22691} {β : Type ?u.22690} {a₁ a₂ : α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {l : α → β}
  {u : β → α}, GaloisConnection l u → l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂
l_sup
#align submonoid.map_sup Submonoid.map_sup: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (S T : Submonoid M) (f : F), map f (S ⊔ T) = map f S ⊔ map f T
Submonoid.map_sup
#align add_submonoid.map_sup AddSubmonoid.map_sup: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid M) (f : F),
  AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f T
AddSubmonoid.map_sup

@[to_additive: ∀ {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid M),
  AddSubmonoid.map f (iSup s) = ⨆ i, AddSubmonoid.map f (s i)
to_additive]
theorem map_iSup: ∀ {M : Type u_2} {N : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4}
  [mc : MonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → Submonoid M), map f (iSup s) = ⨆ i, map f (s i)
map_iSup {ι: Sort u_1
ι : Sort _: Type ?u.22854
SortSort _: Type ?u.22854
 _} (f: F
f : F: Type ?u.22839
F) (s: ι → Submonoid M
s : ι: Sort ?u.22854
ι → Submonoid: (M : Type ?u.22861) → [inst : MulOneClass M] → Type ?u.22861
Submonoid M: Type ?u.22812
M) : (iSup: {α : Type ?u.22872} → [inst : SupSet α] → {ι : Sort ?u.22871} → (ι → α) → α
iSup s: ι → Submonoid M
s).map: {M : Type ?u.22904} →
  {N : Type ?u.22903} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.22902} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f = ⨆ i: ?m.22968
i, (s: ι → Submonoid M
s i: ?m.22968
i).map: {M : Type ?u.22972} →
  {N : Type ?u.22971} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.22970} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f :=
  (gc_map_comap: ∀ {M : Type ?u.23397} {N : Type ?u.23398} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.23399}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f : GaloisConnection: {α : Type ?u.23096} → {β : Type ?u.23095} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection (map: {M : Type ?u.23133} →
  {N : Type ?u.23132} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.23131} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f) (comap: {M : Type ?u.23252} →
  {N : Type ?u.23251} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.23250} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f)).l_iSup: ∀ {α : Type ?u.23463} {β : Type ?u.23462} {ι : Sort ?u.23461} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {f : ι → α}, l (iSup f) = ⨆ i, l (f i)
l_iSup
#align submonoid.map_supr Submonoid.map_iSup: ∀ {M : Type u_2} {N : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4}
  [mc : MonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → Submonoid M), map f (iSup s) = ⨆ i, map f (s i)
Submonoid.map_iSup
#align add_submonoid.map_supr AddSubmonoid.map_iSup: ∀ {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid M),
  AddSubmonoid.map f (iSup s) = ⨆ i, AddSubmonoid.map f (s i)
AddSubmonoid.map_iSup

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid N) (f : F),
  AddSubmonoid.comap f (S ⊓ T) = AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T
to_additive]
theorem comap_inf: ∀ (S T : Submonoid N) (f : F), comap f (S ⊓ T) = comap f S ⊓ comap f T
comap_inf (S: Submonoid N
S T: Submonoid N
T : Submonoid: (M : Type ?u.23645) → [inst : MulOneClass M] → Type ?u.23645
Submonoid N: Type ?u.23597
N) (f: F
f : F: Type ?u.23621
F) : (S: Submonoid N
S ⊓ T: Submonoid N
T).comap: {M : Type ?u.23670} →
  {N : Type ?u.23669} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.23668} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f = S: Submonoid N
S.comap: {M : Type ?u.23733} →
  {N : Type ?u.23732} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.23731} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f ⊓ T: Submonoid N
T.comap: {M : Type ?u.23827} →
  {N : Type ?u.23826} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.23825} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f :=
  (gc_map_comap: ∀ {M : Type ?u.24220} {N : Type ?u.24221} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.24222}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f : GaloisConnection: {α : Type ?u.23919} → {β : Type ?u.23918} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection (map: {M : Type ?u.23956} →
  {N : Type ?u.23955} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.23954} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f) (comap: {M : Type ?u.24075} →
  {N : Type ?u.24074} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.24073} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f)).u_inf: ∀ {α : Type ?u.24285} {β : Type ?u.24284} {b₁ b₂ : β} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {l : α → β}
  {u : β → α}, GaloisConnection l u → u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂
u_inf
#align submonoid.comap_inf Submonoid.comap_inf: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (S T : Submonoid N) (f : F), comap f (S ⊓ T) = comap f S ⊓ comap f T
Submonoid.comap_inf
#align add_submonoid.comap_inf AddSubmonoid.comap_inf: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid N) (f : F),
  AddSubmonoid.comap f (S ⊓ T) = AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T
AddSubmonoid.comap_inf

@[to_additive: ∀ {M : Type u_3} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid N),
  AddSubmonoid.comap f (iInf s) = ⨅ i, AddSubmonoid.comap f (s i)
to_additive]
theorem comap_iInf: ∀ {ι : Sort u_1} (f : F) (s : ι → Submonoid N), comap f (iInf s) = ⨅ i, comap f (s i)
comap_iInf {ι: Sort u_1
ι : Sort _: Type ?u.24454
SortSort _: Type ?u.24454
 _} (f: F
f : F: Type ?u.24439
F) (s: ι → Submonoid N
s : ι: Sort ?u.24454
ι → Submonoid: (M : Type ?u.24461) → [inst : MulOneClass M] → Type ?u.24461
Submonoid N: Type ?u.24415
N) :
    (iInf: {α : Type ?u.24472} → [inst : InfSet α] → {ι : Sort ?u.24471} → (ι → α) → α
iInf s: ι → Submonoid N
s).comap: {M : Type ?u.24495} →
  {N : Type ?u.24494} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.24493} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f = ⨅ i: ?m.24559
i, (s: ι → Submonoid N
s i: ?m.24559
i).comap: {M : Type ?u.24563} →
  {N : Type ?u.24562} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.24561} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f :=
  (gc_map_comap: ∀ {M : Type ?u.24979} {N : Type ?u.24980} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.24981}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f : GaloisConnection: {α : Type ?u.24678} → {β : Type ?u.24677} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection (map: {M : Type ?u.24715} →
  {N : Type ?u.24714} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.24713} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f) (comap: {M : Type ?u.24834} →
  {N : Type ?u.24833} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.24832} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f)).u_iInf: ∀ {α : Type ?u.25045} {β : Type ?u.25044} {ι : Sort ?u.25043} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {f : ι → β}, u (iInf f) = ⨅ i, u (f i)
u_iInf
#align submonoid.comap_infi Submonoid.comap_iInf: ∀ {M : Type u_3} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4}
  [mc : MonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → Submonoid N), comap f (iInf s) = ⨅ i, comap f (s i)
Submonoid.comap_iInf
#align add_submonoid.comap_infi AddSubmonoid.comap_iInf: ∀ {M : Type u_3} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid N),
  AddSubmonoid.comap f (iInf s) = ⨅ i, AddSubmonoid.comap f (s i)
AddSubmonoid.comap_iInf

@[to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.map f ⊥ = ⊥
to_additive (attr := simp)]
theorem map_bot: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F), map f ⊥ = ⊥
map_bot (f: F
f : F: Type ?u.25213
F) : (⊥: ?m.25240
⊥ : Submonoid: (M : Type ?u.25232) → [inst : MulOneClass M] → Type ?u.25232
Submonoid M: Type ?u.25186
M).map: {M : Type ?u.25281} →
  {N : Type ?u.25280} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.25279} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f = ⊥: ?m.25340
⊥ :=
  (gc_map_comap: ∀ {M : Type ?u.25399} {N : Type ?u.25400} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.25401}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).l_bot: ∀ {α : Type ?u.25463} {β : Type ?u.25462} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot β]
  [inst_3 : OrderBot α] {l : α → β} {u : β → α}, GaloisConnection l u → l ⊥ = ⊥
l_bot
#align submonoid.map_bot Submonoid.map_bot: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F), map f ⊥ = ⊥
Submonoid.map_bot
#align add_submonoid.map_bot AddSubmonoid.map_bot: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.map f ⊥ = ⊥
AddSubmonoid.map_bot

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.comap f ⊤ = ⊤
to_additive (attr := simp)]
theorem comap_top: ∀ (f : F), comap f ⊤ = ⊤
comap_top (f: F
f : F: Type ?u.25773
F) : (⊤: ?m.25800
⊤ : Submonoid: (M : Type ?u.25792) → [inst : MulOneClass M] → Type ?u.25792
Submonoid N: Type ?u.25749
N).comap: {M : Type ?u.25840} →
  {N : Type ?u.25839} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.25838} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f = ⊤: ?m.25899
⊤ :=
  (gc_map_comap: ∀ {M : Type ?u.25956} {N : Type ?u.25957} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.25958}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).u_top: ∀ {α : Type ?u.26020} {β : Type ?u.26019} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] {l : α → β} {u : β → α}, GaloisConnection l u → u ⊤ = ⊤
u_top
#align submonoid.comap_top Submonoid.comap_top: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] (f : F), comap f ⊤ = ⊤
Submonoid.comap_top
#align add_submonoid.comap_top AddSubmonoid.comap_top: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.comap f ⊤ = ⊤
AddSubmonoid.comap_top

@[to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), AddSubmonoid.map (AddMonoidHom.id M) S = S
to_additive (attr := simp)]
theorem map_id: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), map (MonoidHom.id M) S = S
map_id (S: Submonoid M
S : Submonoid: (M : Type ?u.26345) → [inst : MulOneClass M] → Type ?u.26345
Submonoid M: Type ?u.26303
M) : S: Submonoid M
S.map: {M : Type ?u.26357} →
  {N : Type ?u.26356} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.26355} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map (MonoidHom.id: (M : Type ?u.26372) → [inst : MulOneClass M] → M →* M
MonoidHom.id M: Type ?u.26303
M) = S: Submonoid M
S :=
  ext: ∀ {M : Type ?u.26432} [inst : MulOneClass M] {S T : Submonoid M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
ext fun _: ?m.26456
_ => ⟨fun ⟨_: ?m.26456
_, h: x✝¹ ∈ ↑S
h, rfl: ∀ {α : Sort ?u.26470} {a : α}, a = a
rfl⟩ => h: x✝¹ ∈ ↑S
h, fun h: ?m.26771
h => ⟨_: ?m.26778
_, h: ?m.26771
h, rfl: ∀ {α : Sort ?u.26803} {a : α}, a = a
rfl⟩⟩
#align submonoid.map_id Submonoid.map_id: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), map (MonoidHom.id M) S = S
Submonoid.map_id
#align add_submonoid.map_id AddSubmonoid.map_id: ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), AddSubmonoid.map (AddMonoidHom.id M) S = S
AddSubmonoid.map_id

section GaloisCoinsertion

variable {ι: Type ?u.29867
ι : Type _: Type (?u.27001+1)
Type _} {f: F
f : F: Type ?u.30432
F} (hf: Function.Injective ↑f
hf : Function.Injective: {α : Sort ?u.31031} → {β : Sort ?u.31030} → (α → β) → Prop
Function.Injective f: F
f)

/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. -/
@[to_additive: {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_3} →
          [mc : AddMonoidHomClass F M N] →
            {f : F} → Function.Injective ↑f → GaloisCoinsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)
to_additive " `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. "]
def gciMapComap: GaloisCoinsertion (map f) (comap f)
gciMapComap : GaloisCoinsertion: {α : Type ?u.27436} →
  {β : Type ?u.27435} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Type (max?u.27436?u.27435)
GaloisCoinsertion (map: {M : Type ?u.27473} →
  {N : Type ?u.27472} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.27471} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f) (comap: {M : Type ?u.27592} →
  {N : Type ?u.27591} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.27590} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f) :=
  (gc_map_comap: ∀ {M : Type ?u.27738} {N : Type ?u.27739} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.27740}
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap f: F
f).toGaloisCoinsertion: {α : Type ?u.27795} →
  {β : Type ?u.27794} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {l : α → β} → {u : β → α} → GaloisConnection l u → (∀ (a : α), u (l a) ≤ a) → GaloisCoinsertion l u
toGaloisCoinsertion fun S: ?m.27830
S x: ?m.27833
x => by
Goals accomplished! 🐙 M: Type ?u.27197

N: Type ?u.27200

P: Type ?u.27203

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.27224

mc: MonoidHomClass F M N

ι: Type ?u.27239

f: F

hf: Function.Injective ↑f

S: Submonoid M

x: M

x ∈ comap f (map f S) → x ∈ Ssimp [mem_comap: ∀ {M : Type ?u.27841} {N : Type ?u.27840} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.27842}
  [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M}, x ∈ comap f S ↔ ↑f x ∈ S
mem_comap, mem_map: ∀ {M : Type ?u.27890} {N : Type ?u.27891} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.27892}
  [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N}, y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
mem_map, hf: Function.Injective ↑f
hf.eq_iff: ∀ {α : Sort ?u.27932} {β : Sort ?u.27933} {f : α → β}, Function.Injective f → ∀ {a b : α}, f a = f b ↔ a = b
eq_iff]
Goals accomplished! 🐙
#align submonoid.gci_map_comap Submonoid.gciMapComap: {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {F : Type u_3} →
          [mc : MonoidHomClass F M N] → {f : F} → Function.Injective ↑f → GaloisCoinsertion (map f) (comap f)
Submonoid.gciMapComap
#align add_submonoid.gci_map_comap AddSubmonoid.gciMapComap: {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_3} →
          [mc : AddMonoidHomClass F M N] →
            {f : F} → Function.Injective ↑f → GaloisCoinsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)
AddSubmonoid.gciMapComap

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ↑f → ∀ (S : AddSubmonoid M), AddSubmonoid.comap f (AddSubmonoid.map f S) = S
to_additive]
theorem comap_map_eq_of_injective: ∀ (S : Submonoid M), comap f (map f S) = S
comap_map_eq_of_injective (S: Submonoid M
S : Submonoid: (M : Type ?u.29462) → [inst : MulOneClass M] → Type ?u.29462
Submonoid M: Type ?u.29224
M) : (S: Submonoid M
S.map: {M : Type ?u.29474} →
  {N : Type ?u.29473} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.29472} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map f: F
f).comap: {M : Type ?u.29532} →
  {N : Type ?u.29531} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → {F : Type ?u.29530} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap f: F
f = S: Submonoid M
S :=
  (gciMapComap: {M : Type ?u.29591} →
  {N : Type ?u.29590} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {F : Type ?u.29589} →
          [mc : MonoidHomClass F M N] → {f : F} → Function.Injective ↑f → GaloisCoinsertion (map f) (comap f)
gciMapComap hf: Function.Injective ↑f
hf).u_l_eq: ∀ {α : Type ?u.29657} {β : Type ?u.29656} {l : α → β} {u : β → α} [inst : PartialOrder α] [inst_1 : Preorder β],
  GaloisCoinsertion l u → ∀ (a : α), u (l a) = a
u_l_eq _: ?m.29666
_
#align submonoid.comap_map_eq_of_injective Submonoid.comap_map_eq_of_injective: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3}
  [mc : MonoidHomClass F M N] {f : F}, Function.Injective ↑f → ∀ (S : Submonoid M), comap f (map f S) = S
Submonoid.comap_map_eq_of_injective
#align add_submonoid.comap_map_eq_of_injective AddSubmonoid.comap_map_eq_of_injective: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3}
  [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ↑f → ∀ (S : AddSubmonoid M), AddSubmonoid.comap f (