[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


[GOAL]
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#
[PROOFSTEP]
refine prod_congr ?_ fun _ _ ↦ rfl
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ filter Nat.Prime (range (n + 1 + 1)) = filter Nat.Prime (range (n + 1))
[PROOFSTEP]
rw [range_succ, filter_insert, if_neg fun h ↦ odd_iff_not_even.mp hn _]
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ Nat.Prime (n + 1) → Even n
[PROOFSTEP]
exact fun h ↦ h.even_sub_one <| mt succ.inj hn1
[GOAL]
m n : ℕ
⊢ (m + n)# = m# * ∏ p in filter Nat.Prime (Ico (m + 1) (m + n + 1)), p
[PROOFSTEP]
rw [primorial, primorial, ← Ico_zero_eq_range, ← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]
[GOAL]
case hab
m n : ℕ
⊢ 0 ≤ m + 1
case hbc
m n : ℕ
⊢ m + 1 ≤ m + n + 1
m n : ℕ ⊢ Disjoint (filter Nat.Prime (Ico 0 (m + 1))) (filter Nat.Prime (Ico (m + 1) (m + n + 1)))
[PROOFSTEP]
exacts [Nat.zero_le _, add_le_add_right (Nat.le_add_right _ _) _,
  disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _]
[GOAL]
m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ filter Nat.Prime (Ico (m + 1) (m + n + 1))
⊢ p ∣ Nat.choose (m + n) m
[PROOFSTEP]
rw [mem_filter, mem_Ico] at hp
[GOAL]
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ Nat.choose (m + n) m
[PROOFSTEP]
exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1)) (Nat.lt_succ_iff.1 hp.1.2)
[GOAL]
n : ℕ
⊢ n# ≤ 4 ^ n
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n ihn
[GOAL]
case h
n : ℕ
ihn : ∀ (m : ℕ), m < n → m# ≤ 4 ^ m
⊢ n# ≤ 4 ^ n
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
ihn : ∀ (m : ℕ), m < zero → m# ≤ 4 ^ m
⊢ zero# ≤ 4 ^ zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
⊢ succ n# ≤ 4 ^ succ n
[PROOFSTEP]
rcases n.even_or_odd with (⟨m, rfl⟩ | ho)
[GOAL]
case h.succ.inl.intro
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
⊢ succ (m + m)# ≤ 4 ^ succ (m + m)
[PROOFSTEP]
rcases m.eq_zero_or_pos with (rfl | hm)
[GOAL]
case h.succ.inl.intro.inl
ihn : ∀ (m : ℕ), m < succ (0 + 0) → m# ≤ 4 ^ m
⊢ succ (0 + 0)# ≤ 4 ^ succ (0 + 0)
[PROOFSTEP]
decide
[GOAL]
case h.succ.inl.intro.inr
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ succ (m + m)# ≤ 4 ^ succ (m + m)
[PROOFSTEP]
calc
  (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
  _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := (primorial_add_le m.le_succ)
  _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
  _ ≤ 4 ^ (m + 1) * 4 ^ m :=
    (mul_le_mul' (ihn _ <| succ_lt_succ <| (lt_add_iff_pos_left _).2 hm) (choose_middle_le_pow _))
  _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
[GOAL]
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + m + 1)# = (m + 1 + m)#
[PROOFSTEP]
rw [add_right_comm]
[GOAL]
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + 1)# * Nat.choose (m + 1 + m) (m + 1) = (m + 1)# * Nat.choose (2 * m + 1) m
[PROOFSTEP]
rw [choose_symm_add, two_mul, add_right_comm]
[GOAL]
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ 4 ^ (m + 1) * 4 ^ m ≤ 4 ^ (m + m + 1)
[PROOFSTEP]
rw [← pow_add, add_right_comm]
[GOAL]
case h.succ.inr
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
ho : Odd n
⊢ succ n# ≤ 4 ^ succ n
[PROOFSTEP]
rcases Decidable.eq_or_ne n 1 with (rfl | hn)
[GOAL]
case h.succ.inr.inl
ihn : ∀ (m : ℕ), m < succ 1 → m# ≤ 4 ^ m
ho : Odd 1
⊢ succ 1# ≤ 4 ^ succ 1
[PROOFSTEP]
decide
[GOAL]
case h.succ.inr.inr
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
ho : Odd n
hn : n ≠ 1
⊢ succ n# ≤ 4 ^ succ n
[PROOFSTEP]
calc
  (n + 1)# = n# := primorial_succ hn ho
  _ ≤ 4 ^ n := (ihn n n.lt_succ_self)
  _ ≤ 4 ^ (n + 1) := pow_le_pow_of_le_right four_pos n.le_succ


[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ∃ a b, a ^ 2 + b ^ 2 = p
[PROOFSTEP]
apply sq_add_sq_of_nat_prime_of_not_irreducible p
[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬Irreducible ↑p
[PROOFSTEP]
rwa [PrincipalIdealRing.irreducible_iff_prime, prime_iff_mod_four_eq_three_of_nat_prime p]
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ a * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2
[PROOFSTEP]
rw [ha, hb]
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ (x ^ 2 + y ^ 2) * (u ^ 2 + v ^ 2) = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2
[PROOFSTEP]
ring
[GOAL]
a b x y u v : ℕ
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ ∃ r s, a * b = r ^ 2 + s ^ 2
[PROOFSTEP]
zify at ha hb ⊢
[GOAL]
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2
[PROOFSTEP]
obtain ⟨r, s, h⟩ := _root_.sq_add_sq_mul ha hb
[GOAL]
case intro.intro
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2
[PROOFSTEP]
refine' ⟨r.natAbs, s.natAbs, _⟩
[GOAL]
case intro.intro
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ↑a * ↑b = ↑(Int.natAbs r) ^ 2 + ↑(Int.natAbs s) ^ 2
[PROOFSTEP]
simpa only [Int.coe_natAbs, sq_abs]
[GOAL]
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
let f : ZMod n →+* ZMod m := ZMod.castHom hd _
[GOAL]
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (-1)
[PROOFSTEP]
rw [← RingHom.map_one f, ← RingHom.map_neg]
[GOAL]
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (↑f (-1))
[PROOFSTEP]
exact hs.map f
[GOAL]
m n : ℕ
hc : Nat.coprime m n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
have : IsSquare (-1 : ZMod m × ZMod n) :=
  by
  rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
  obtain ⟨x, hx⟩ := hm
  obtain ⟨y, hy⟩ := hn
  rw [hx, hy]
  exact ⟨(x, y), rfl⟩
[GOAL]
m n : ℕ
hc : Nat.coprime m n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
[GOAL]
m n : ℕ
hc : Nat.coprime m n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1, -1)
[PROOFSTEP]
obtain ⟨x, hx⟩ := hm
[GOAL]
case intro
m n : ℕ
hc : Nat.coprime m n
hn : IsSquare (-1)
x : ZMod m
hx : -1 = x * x
⊢ IsSquare (-1, -1)
[PROOFSTEP]
obtain ⟨y, hy⟩ := hn
[GOAL]
case intro.intro
m n : ℕ
hc : Nat.coprime m n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (-1, -1)
[PROOFSTEP]
rw [hx, hy]
[GOAL]
case intro.intro
m n : ℕ
hc : Nat.coprime m n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (x * x, y * y)
[PROOFSTEP]
exact ⟨(x, y), rfl⟩
[GOAL]
m n : ℕ
hc : Nat.coprime m n
hm : IsSquare (-1)
hn : IsSquare (-1)
this : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
simpa only [RingEquiv.map_neg_one] using this.map (ZMod.chineseRemainder hc).symm
[GOAL]
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
⊢ p % 4 ≠ 3
[PROOFSTEP]
obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd hp hs
[GOAL]
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : -1 = y * y
⊢ p % 4 ≠ 3
[PROOFSTEP]
rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h
[GOAL]
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1
⊢ -1 = -1 ^ 2
[PROOFSTEP]
ring
[GOAL]
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
⊢ p % 4 ≠ 3
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hpp⟩
[GOAL]
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
this : Fact (Prime p)
⊢ p % 4 ≠ 3
[PROOFSTEP]
exact ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h
[GOAL]
n : ℕ
hn : Squarefree n
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
refine' ⟨fun H q hqp hqd => hqp.mod_four_ne_three_of_dvd_isSquare_neg_one hqd H, fun H => _⟩
[GOAL]
n : ℕ
hn : Squarefree n
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ IsSquare (-1)
[PROOFSTEP]
induction' n using induction_on_primes with p n hpp ih
[GOAL]
case h₀
n : ℕ
hn✝ : Squarefree n
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
hn : Squarefree 0
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 0 → q % 4 ≠ 3
⊢ IsSquare (-1)
[PROOFSTEP]
exact False.elim (hn.ne_zero rfl)
[GOAL]
case h₁
n : ℕ
hn✝ : Squarefree n
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
hn : Squarefree 1
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 1 → q % 4 ≠ 3
⊢ IsSquare (-1)
[PROOFSTEP]
exact ⟨0, by simp only [Fin.zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩
[GOAL]
n : ℕ
hn✝ : Squarefree n
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
hn : Squarefree 1
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 1 → q % 4 ≠ 3
⊢ -1 = 0 * 0
[PROOFSTEP]
simp only [Fin.zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]
[GOAL]
case h
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
⊢ IsSquare (-1)
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hpp⟩
[GOAL]
case h
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ IsSquare (-1)
[PROOFSTEP]
have hcp : p.coprime n := by
  by_contra hc
  exact hpp.not_unit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
[GOAL]
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ Nat.coprime p n
[PROOFSTEP]
by_contra hc
[GOAL]
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hc : ¬Nat.coprime p n
⊢ False
[PROOFSTEP]
exact hpp.not_unit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
[GOAL]
case h
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : Nat.coprime p n
⊢ IsSquare (-1)
[PROOFSTEP]
have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr (H hpp (dvd_mul_right p n))
[GOAL]
case h
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : Nat.coprime p n
hp₁ : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
exact ZMod.isSquare_neg_one_mul hcp hp₁ (ih hn.of_mul_right fun hqp hqd => H hqp <| dvd_mul_of_dvd_right hqd _)
[GOAL]
n : ℕ
hn : Squarefree n
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
have help : ∀ a b : ZMod 4, a ≠ 3 → b ≠ 3 → a * b ≠ 3 := by decide
[GOAL]
n : ℕ
hn : Squarefree n
⊢ ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
[PROOFSTEP]
decide
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
rw [ZMod.isSquare_neg_one_iff hn]
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
refine' ⟨_, fun H q _ => H⟩
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
intro H
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
refine' @induction_on_primes _ _ _ (fun p q hp hq hpq => _)
[GOAL]
case refine'_1
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ 0 ∣ n → 0 % 4 ≠ 3
[PROOFSTEP]
exact fun _ => by norm_num
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
x✝ : 0 ∣ n
⊢ 0 % 4 ≠ 3
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ 1 ∣ n → 1 % 4 ≠ 3
[PROOFSTEP]
exact fun _ => by norm_num
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
x✝ : 1 ∣ n
⊢ 1 % 4 ≠ 3
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3
[PROOFSTEP]
replace hp := H hp (dvd_of_mul_right_dvd hpq)
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
hp : p % 4 ≠ 3
⊢ p * q % 4 ≠ 3
[PROOFSTEP]
replace hq := hq (dvd_of_mul_left_dvd hpq)
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ p * q % 4 ≠ 3
[PROOFSTEP]
rw [show 3 = 3 % 4 by norm_num, Ne.def, ← ZMod.nat_cast_eq_nat_cast_iff'] at hp hq ⊢
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ 3 = 3 % 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3 % 4
hq : q % 4 ≠ 3
⊢ 3 = 3 % 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3 % 4
hq : q % 4 ≠ 3 % 4
⊢ 3 = 3 % 4
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑(p * q) = ↑3
[PROOFSTEP]
rw [Nat.cast_mul]
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑p * ↑q = ↑3
[PROOFSTEP]
exact help p q hp hq
[GOAL]
n : ℕ
h : IsSquare (-1)
⊢ ∃ x y, n = x ^ 2 + y ^ 2
[PROOFSTEP]
induction' n using induction_on_primes with p n hpp ih
[GOAL]
case h₀
n : ℕ
h✝ : IsSquare (-1)
h : IsSquare (-1)
⊢ ∃ x y, 0 = x ^ 2 + y ^ 2
[PROOFSTEP]
exact ⟨0, 0, rfl⟩
[GOAL]
case h₁
n : ℕ
h✝ : IsSquare (-1)
h : IsSquare (-1)
⊢ ∃ x y, 1 = x ^ 2 + y ^ 2
[PROOFSTEP]
exact ⟨0, 1, rfl⟩
[GOAL]
case h
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hpp⟩
[GOAL]
case h
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
[GOAL]
case h
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)
[GOAL]
case h.intro.intro
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)
[GOAL]
case h.intro.intro.intro.intro
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
x y : ℕ
hxy : n = x ^ 2 + y ^ 2
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
exact Nat.sq_add_sq_mul huv.symm hxy
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
⊢ IsSquare (-1)
[PROOFSTEP]
obtain ⟨u, v, huv⟩ : IsCoprime x n :=
  by
  have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
  rw [show y ^ 2 = n + -1 * x ^ 2 by rw [h]; ring] at hc2
  exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
⊢ IsCoprime x n
[PROOFSTEP]
have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ IsCoprime x n
[PROOFSTEP]
rw [show y ^ 2 = n + -1 * x ^ 2 by rw [h]; ring] at hc2
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ y ^ 2 = n + -1 * x ^ 2
[PROOFSTEP]
rw [h]
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ y ^ 2 = x ^ 2 + y ^ 2 + -1 * x ^ 2
[PROOFSTEP]
ring
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (n + -1 * x ^ 2)
⊢ IsCoprime x n
[PROOFSTEP]
exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ IsSquare (-1)
[PROOFSTEP]
have H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v) := by
  linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
[PROOFSTEP]
linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ IsSquare (-1)
[PROOFSTEP]
refine' ⟨u * y, _⟩
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑u * ↑y * (↑u * ↑y)
[PROOFSTEP]
conv_rhs => tactic => norm_cast
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
| ↑u * ↑y * (↑u * ↑y)
[PROOFSTEP]
tactic => norm_cast
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
| ↑u * ↑y * (↑u * ↑y)
[PROOFSTEP]
tactic => norm_cast
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
| ↑u * ↑y * (↑u * ↑y)
[PROOFSTEP]
tactic => norm_cast
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑u * ↑y * (↑u * ↑y) = ?m.37150
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(u * y * (u * y))
[PROOFSTEP]
rw [(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))]
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(-1)
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑(-1) = ↑(u * y * (u * y))
[PROOFSTEP]
exact (ZMod.int_cast_eq_int_cast_iff_dvd_sub _ _ _).mpr (Int.natAbs_dvd.mpr ⟨_, H⟩)
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hc : Nat.coprime x y
⊢ IsSquare (-1)
[PROOFSTEP]
zify at h
[GOAL]
n x y : ℕ
hc : Nat.coprime x y
h : ↑n = ↑x ^ 2 + ↑y ^ 2
⊢ IsSquare (-1)
[PROOFSTEP]
exact ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime h hc.isCoprime
[GOAL]
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) → ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
rintro ⟨x, y, h⟩
[GOAL]
case mp.intro.intro
n x y : ℕ
h : n = x ^ 2 + y ^ 2
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
by_cases hxy : x = 0 ∧ y = 0
[GOAL]
case pos
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
exact
  ⟨0, 1, by rw [h, hxy.1, hxy.2, zero_pow zero_lt_two, add_zero, zero_mul],
    ⟨0, by rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩⟩
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ n = 0 ^ 2 * 1
[PROOFSTEP]
rw [h, hxy.1, hxy.2, zero_pow zero_lt_two, add_zero, zero_mul]
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ -1 = 0 * 0
[PROOFSTEP]
rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]
[GOAL]
case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)
[GOAL]
case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < gcd x y
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
obtain ⟨g, x₁, y₁, _, h₂, h₃, h₄⟩ := Nat.exists_coprime' hg
[GOAL]
case neg.intro.intro.intro.intro.intro.intro
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < gcd x y
g : ℕ
x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : coprime x₁ y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
exact ⟨g, x₁ ^ 2 + y₁ ^ 2, by rw [h, h₃, h₄]; ring, ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime rfl h₂⟩
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < gcd x y
g : ℕ
x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : coprime x₁ y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ n = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)
[PROOFSTEP]
rw [h, h₃, h₄]
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < gcd x y
g : ℕ
x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : coprime x₁ y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ (x₁ * g) ^ 2 + (y₁ * g) ^ 2 = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)
[PROOFSTEP]
ring
[GOAL]
case mpr
n : ℕ
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) → ∃ x y, n = x ^ 2 + y ^ 2
[PROOFSTEP]
rintro ⟨a, b, h₁, h₂⟩
[GOAL]
case mpr.intro.intro.intro
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ ∃ x y, n = x ^ 2 + y ^ 2
[PROOFSTEP]
obtain ⟨x', y', h⟩ := Nat.eq_sq_add_sq_of_isSquare_mod_neg_one h₂
[GOAL]
case mpr.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ ∃ x y, n = x ^ 2 + y ^ 2
[PROOFSTEP]
exact ⟨a * x', a * y', by rw [h₁, h]; ring⟩
[GOAL]
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ n = (a * x') ^ 2 + (a * y') ^ 2
[PROOFSTEP]
rw [h₁, h]
[GOAL]
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ a ^ 2 * (x' ^ 2 + y' ^ 2) = (a * x') ^ 2 + (a * y') ^ 2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn₀)
[GOAL]
case inl
⊢ (∃ x y, 0 = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q 0)
[PROOFSTEP]
exact
  ⟨fun _ q _ _ => (@padicValNat.zero q).symm ▸ even_zero, fun _ => ⟨0, 0, rfl⟩⟩
    -- now `0 < n`
[GOAL]
case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
[PROOFSTEP]
rw [Nat.eq_sq_add_sq_iff_eq_sq_mul]
[GOAL]
case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
[PROOFSTEP]
refine' ⟨fun H q hq h => _, fun H => _⟩
[GOAL]
case inr.refine'_1
n : ℕ
hn₀ : n > 0
H : ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
q : ℕ
hq : Prime q
h : q % 4 = 3
⊢ Even (padicValNat q n)
[PROOFSTEP]
obtain ⟨a, b, h₁, h₂⟩ := H
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ Even (padicValNat q n)
[PROOFSTEP]
have hqb := padicValNat.eq_zero_of_not_dvd fun hf => (hq.mod_four_ne_three_of_dvd_isSquare_neg_one hf h₂) h
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
have hab : a ^ 2 * b ≠ 0 := h₁ ▸ hn₀.ne'
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
have ha₂ := left_ne_zero_of_mul hab
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
have ha := mt sq_eq_zero_iff.mpr ha₂
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
have hb := right_ne_zero_of_mul hab
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
haveI hqi : Fact q.Prime := ⟨hq⟩
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
hqi : Fact (Prime q)
⊢ Even (padicValNat q n)
[PROOFSTEP]
simp_rw [h₁, padicValNat.mul ha₂ hb, padicValNat.pow 2 ha, hqb, add_zero]
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
hqi : Fact (Prime q)
⊢ Even (2 * padicValNat q a)
[PROOFSTEP]
exact even_two_mul _
[GOAL]
case inr.refine'_2
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := Nat.sq_mul_squarefree_of_pos hn₀
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
refine' ⟨a, b, hab.symm, (ZMod.isSquare_neg_one_iff hb).mpr fun {q} hqp hqb hq4 => _⟩
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
⊢ False
[PROOFSTEP]
refine' Nat.odd_iff_not_even.mp _ (H hqp hq4)
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
⊢ Odd (padicValNat q n)
[PROOFSTEP]
have hqb' : padicValNat q b = 1 :=
  b.factorization_def hqp ▸
    le_antisymm (Nat.Squarefree.factorization_le_one _ hb) ((hqp.dvd_iff_one_le_factorization hb₀.ne').mp hqb)
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
⊢ Odd (padicValNat q n)
[PROOFSTEP]
haveI hqi : Fact q.Prime := ⟨hqp⟩
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
hqi : Fact (Prime q)
⊢ Odd (padicValNat q n)
[PROOFSTEP]
simp_rw [← hab, padicValNat.mul (pow_ne_zero 2 ha₀.ne') hb₀.ne', hqb', padicValNat.pow 2 ha₀.ne']
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
hqi : Fact (Prime q)
⊢ Odd (2 * padicValNat q a + 1)
[PROOFSTEP]
exact odd_two_mul_add_one _