[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
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) =
    x
[PROOFSTEP]
cases x
[GOAL]
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.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) })
      ((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'✝ }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
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) =
    x
[PROOFSTEP]
cases x
[GOAL]
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toAddSubsemigroup✝ : AddSubsemigroup (Additive M)
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.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) })
      ((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'✝ }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
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) =
    x
[PROOFSTEP]
cases x
[GOAL]
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toAddSubsemigroup✝ : AddSubsemigroup A
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.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) })
      ((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'✝ }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
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) =
    x
[PROOFSTEP]
cases x
[GOAL]
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toSubsemigroup✝ : Subsemigroup (Multiplicative A)
one_mem'✝ : 1 ∈ toSubsemigroup✝.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) })
      ((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'✝ }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a✝ b✝ : M
ha : a✝ ∈ ↑f ⁻¹' ↑S
hb : b✝ ∈ ↑f ⁻¹' ↑S
⊢ ↑f (a✝ * b✝) ∈ S
[PROOFSTEP]
rw [map_mul]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
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
[PROOFSTEP]
exact S.mul_mem ha hb
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ ↑f 1 ∈ S
[PROOFSTEP]
rw [map_one]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ 1 ∈ S
[PROOFSTEP]
exact S.one_mem
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
S : Submonoid P
⊢ ∀ (x : P), x ∈ comap (MonoidHom.id P) S ↔ x ∈ S
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
f : F
S : Submonoid M
⊢ ∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a * b ∈ ↑f '' ↑S
[PROOFSTEP]
rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
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 '' ↑S
[PROOFSTEP]
exact ⟨x * y, S.mul_mem hx hy, by rw [map_mul]⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
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 y
[PROOFSTEP]
rw [map_mul]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
f : F
S : Submonoid M
y : N
⊢ y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
[PROOFSTEP]
rw [← bex_def]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
f : F
S : Submonoid M
y : N
⊢ y ∈ map f S ↔ ∃ x x_1, ↑f x = y
[PROOFSTEP]
exact mem_image_iff_bex
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Function.Injective ↑f
S : Submonoid M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S
[PROOFSTEP]
simp [mem_comap, mem_map, hf.eq_iff]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Function.Surjective ↑f
S : Submonoid N
x : N
h : x ∈ S
y : M
hy : ↑f y = x
⊢ y ∈ comap f S ∧ ↑f y = x
[PROOFSTEP]
simp [hy, h]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ ∀ (x y : { x // x ∈ S' }),
    OneHom.toFun { toFun := Subtype.val, map_one' := (_ : ↑1 = ↑1) } (x * y) =
      OneHom.toFun { toFun := Subtype.val, map_one' := (_ : ↑1 = ↑1) } x *
        OneHom.toFun { toFun := Subtype.val, map_one' := (_ : ↑1 = ↑1) } y
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ ∀ (x y : { x // x ∈ S }),
    OneHom.toFun { toFun := Subtype.val, map_one' := (_ : ↑1 = ↑1) } (x * y) =
      OneHom.toFun { toFun := Subtype.val, map_one' := (_ : ↑1 = ↑1) } x *
        OneHom.toFun { toFun := Subtype.val, map_one' := (_ : ↑1 = ↑1) } y
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Set M
x✝¹ : { x // x ∈ ↑(closure s) }
x : M
hx : x ∈ ↑(closure s)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := x, property := hx } ∈ closure (Subtype.val ⁻¹' s)
[PROOFSTEP]
refine' closure_induction' _ (fun g hg => subset_closure hg) _ (fun g₁ g₂ hg₁ hg₂ => _) hx
[GOAL]
case refine'_1
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Set M
x✝¹ : { x // x ∈ ↑(closure s) }
x : M
hx : x ∈ ↑(closure s)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := 1, property := (_ : 1 ∈ closure s) } ∈ closure (Subtype.val ⁻¹' s)
[PROOFSTEP]
exact Submonoid.one_mem _
[GOAL]
case refine'_2
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Set M
x✝¹ : { x // x ∈ ↑(closure s) }
x : M
hx : x ∈ ↑(closure s)
x✝ : { val := x, property := hx } ∈ ⊤
g₁ : M
g₂ : g₁ ∈ closure s
hg₁ : M
hg₂ : hg₁ ∈ closure s
⊢ { val := g₁, property := g₂ } ∈ closure (Subtype.val ⁻¹' s) →
    { val := hg₁, property := hg₂ } ∈ closure (Subtype.val ⁻¹' s) →
      { val := g₁ * hg₁, property := (_ : g₁ * hg₁ ∈ closure s) } ∈ closure (Subtype.val ⁻¹' s)
[PROOFSTEP]
exact Submonoid.mul_mem _
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
x : M × N
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (MonoidHom.fst M N) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_fst]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid N
x : M × N
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (MonoidHom.snd M N) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_snd]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ ↑(prod ⊥ ⊥) = ↑⊥
[PROOFSTEP]
simp [coe_prod, Prod.one_eq_mk]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ prod s t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ prod s t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
intro h
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ prod s t
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
constructor
[GOAL]
case mp.left
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ prod s t
⊢ map (fst M N) u ≤ s
[PROOFSTEP]
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
[GOAL]
case mp.left.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ prod s t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ ↑(fst M N) (y1, y2) ∈ s
[PROOFSTEP]
exact (h hy1).1
[GOAL]
case mp.right
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ prod s t
⊢ map (snd M N) u ≤ t
[PROOFSTEP]
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
[GOAL]
case mp.right.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ prod s t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ ↑(snd M N) (y1, y2) ∈ t
[PROOFSTEP]
exact (h hy1).2
[GOAL]
case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ prod s t
[PROOFSTEP]
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
[GOAL]
case mpr.intro.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (fst M N) u ≤ s
hK : map (snd M N) u ≤ t
x1 : M
x2 : N
h : (x1, x2) ∈ u
⊢ (x1, x2) ∈ prod s t
[PROOFSTEP]
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ prod s t ≤ u ↔ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ prod s t ≤ u → map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u
[PROOFSTEP]
intro h
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u
[PROOFSTEP]
constructor
[GOAL]
case mp.left
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inl M N) s ≤ u
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case mp.left.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : M
hx : x ∈ ↑s
⊢ ↑(inl M N) x ∈ u
[PROOFSTEP]
apply h
[GOAL]
case mp.left.intro.intro.a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : M
hx : x ∈ ↑s
⊢ ↑(inl M N) x ∈ prod s t
[PROOFSTEP]
exact ⟨hx, Submonoid.one_mem _⟩
[GOAL]
case mp.right
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inr M N) t ≤ u
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case mp.right.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : N
hx : x ∈ ↑t
⊢ ↑(inr M N) x ∈ u
[PROOFSTEP]
apply h
[GOAL]
case mp.right.intro.intro.a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : N
hx : x ∈ ↑t
⊢ ↑(inr M N) x ∈ prod s t
[PROOFSTEP]
exact ⟨Submonoid.one_mem _, hx⟩
[GOAL]
case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u → prod s t ≤ u
[PROOFSTEP]
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
[GOAL]
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
⊢ (x1, x2) ∈ u
[PROOFSTEP]
have h1' : inl M N x1 ∈ u := by
  apply hH
  simpa using h1
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
⊢ ↑(inl M N) x1 ∈ u
[PROOFSTEP]
apply hH
[GOAL]
case a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
⊢ ↑(inl M N) x1 ∈ map (inl M N) s
[PROOFSTEP]
simpa using h1
[GOAL]
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
⊢ (x1, x2) ∈ u
[PROOFSTEP]
have h2' : inr M N x2 ∈ u := by
  apply hK
  simpa using h2
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
⊢ ↑(inr M N) x2 ∈ u
[PROOFSTEP]
apply hK
[GOAL]
case a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
⊢ ↑(inr M N) x2 ∈ map (inr M N) t
[PROOFSTEP]
simpa using h2
[GOAL]
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
h2' : ↑(inr M N) x2 ∈ u
⊢ (x1, x2) ∈ u
[PROOFSTEP]
simpa using Submonoid.mul_mem _ h1' h2'
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
g : N →* P
f : M →* N
⊢ map g (mrange f) = mrange (comp g f)
[PROOFSTEP]
simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
f : F
⊢ ↑(mrange f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_mrange, coe_top]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
f : M →* N
⊢ mrange (restrict f S) = map f S
[PROOFSTEP]
simp [SetLike.ext_iff]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
f : M →* N
⊢ mker (mrangeRestrict f) = mker f
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
f : M →* N
x : M
⊢ x ∈ mker (mrangeRestrict f) ↔ x ∈ mker f
[PROOFSTEP]
change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1
[GOAL]
case h
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
f : M →* N
x : M
⊢ { val := ↑f x, property := (_ : ∃ y, ↑f y = ↑f x) } = { val := 1, property := (_ : 1 ∈ mrange f) } ↔ ↑f x = 1
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
⊢ mker 1 = ⊤
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
x✝ : M
⊢ x✝ ∈ mker 1 ↔ x✝ ∈ ⊤
[PROOFSTEP]
simp [mem_mker]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁵ : MulOneClass M
inst✝⁴ : MulOneClass N
inst✝³ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝² : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
M' : Type u_6
N' : Type u_7
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ mker (prodMap f g) = prod (mker f) (mker g)
[PROOFSTEP]
rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_bot]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
⊢ mker (inl M N) = ⊥
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
x : M
⊢ x ∈ mker (inl M N) ↔ x ∈ ⊥
[PROOFSTEP]
simp [mem_mker]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
⊢ mker (inr M N) = ⊥
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
x : N
⊢ x ∈ mker (inr M N) ↔ x ∈ ⊥
[PROOFSTEP]
simp [mem_mker]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
f : M →* N
M' : Submonoid M
⊢ Function.Surjective ↑(submonoidMap f M')
[PROOFSTEP]
rintro ⟨_, x, hx, rfl⟩
[GOAL]
case mk.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_5
mc : MonoidHomClass F M N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, ↑(submonoidMap f M') a = { val := ↑f x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f x) }
[PROOFSTEP]
exact ⟨⟨x, hx⟩, rfl⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ mrange (inl M N) = prod ⊤ ⊥
[PROOFSTEP]
simpa only [mrange_eq_map] using map_inl ⊤
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ mrange (inr M N) = prod ⊥ ⊤
[PROOFSTEP]
simpa only [mrange_eq_map] using map_inr ⊤
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
⊢ prod s t = ⊥ ↔ s = ⊥ ∧ t = ⊥
[PROOFSTEP]
simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot', mker_inl, mker_inr]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
⊢ prod s t = ⊤ ↔ s = ⊤ ∧ t = ⊤
[PROOFSTEP]
simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← mrange_eq_map, mrange_fst, mrange_snd]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ mrange (inl M N) ⊔ mrange (inr M N) = ⊤
[PROOFSTEP]
simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ (∀ (x : M), x ∈ S ↔ x ∈ ⊥) ↔ ∀ (x : M), x ∈ S → x = 1
[PROOFSTEP]
simp (config := { contextual := true }) [iff_def, S.one_mem]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
S : Submonoid M
⊢ (∃ x hx, { val := x, property := hx } ≠ { val := 1, property := (_ : 1 ∈ S) }) ↔ ∃ x, x ∈ S ∧ x ≠ 1
[PROOFSTEP]
simp [Ne.def]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
S : Submonoid M
⊢ S = ⊥ ∨ Nontrivial { x // x ∈ S }
[PROOFSTEP]
simp only [eq_bot_iff_forall, nontrivial_iff_exists_ne_one, ← not_forall, ← not_imp, Classical.em]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
T : Submonoid M
f : M →* N
g : N → M
h : Function.LeftInverse g ↑f
src✝ : M →* { x // x ∈ MonoidHom.mrange f } := MonoidHom.mrangeRestrict f
x : { x // x ∈ MonoidHom.mrange f }
x' : M
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
e : M ≃* N
⊢ equivMapOfInjective S ↑e (_ : Function.Injective ↑e) = MulEquiv.submonoidMap e S
[PROOFSTEP]
ext
[GOAL]
case h.a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
e : M ≃* N
x✝ : { x // x ∈ S }
⊢ ↑(↑(equivMapOfInjective S ↑e (_ : Function.Injective ↑e)) x✝) = ↑(↑(MulEquiv.submonoidMap e S) x✝)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass P
S✝ : Submonoid M
A : Type u_4
inst✝¹ : SetLike A M
hA : SubmonoidClass A M
S' : A
M' : Type u_5
α : Type u_6
β : Type u_7
inst✝ : Monoid M'
S : Submonoid M'
⊢ IsScalarTower { x // x ∈ S } M' M'
[PROOFSTEP]
infer_instance
