[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
f✝ : R →ₙ+* S
g : R →ₙ+* T
f : R →ₙ+* S × T
x : R
⊢ ↑(NonUnitalRingHom.prod (comp (fst S T) f) (comp (snd S T) f)) x = ↑f x
[PROOFSTEP]
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
f✝ : R →+* S
g : R →+* T
f : R →+* S × T
x : R
⊢ ↑(RingHom.prod (comp (fst S T) f) (comp (snd S T) f)) x = ↑f x
[PROOFSTEP]
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
x : R × S
⊢ (fun x => (x, 0)) x.fst = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : R
snd✝ : S
⊢ (fun x => (x, 0)) (fst✝, snd✝).fst = (fst✝, snd✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun x => (x, 0), invFun := Prod.fst,
          left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
          right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
        (x * y) =
      Equiv.toFun
          { toFun := fun x => (x, 0), invFun := Prod.fst,
            left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
            right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
          x *
        Equiv.toFun
          { toFun := fun x => (x, 0), invFun := Prod.fst,
            left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
            right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
          y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun x => (x, 0), invFun := Prod.fst,
          left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
          right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
        (x + y) =
      Equiv.toFun
          { toFun := fun x => (x, 0), invFun := Prod.fst,
            left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
            right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
          x +
        Equiv.toFun
          { toFun := fun x => (x, 0), invFun := Prod.fst,
            left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
            right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
          y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
x : S × R
⊢ (fun x => (0, x)) x.snd = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : S
snd✝ : R
⊢ (fun x => (0, x)) (fst✝, snd✝).snd = (fst✝, snd✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun x => (0, x), invFun := Prod.snd,
          left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
          right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
        (x * y) =
      Equiv.toFun
          { toFun := fun x => (0, x), invFun := Prod.snd,
            left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
            right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
          x *
        Equiv.toFun
          { toFun := fun x => (0, x), invFun := Prod.snd,
            left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
            right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
          y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun x => (0, x), invFun := Prod.snd,
          left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
          right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
        (x + y) =
      Equiv.toFun
          { toFun := fun x => (0, x), invFun := Prod.snd,
            left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
            right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
          x +
        Equiv.toFun
          { toFun := fun x => (0, x), invFun := Prod.snd,
            left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
            right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
          y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ False
[PROOFSTEP]
have := NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ (0, 1) * (1, 0) = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : (0, 1) = 0 ∨ (1, 0) = 0
⊢ False
[PROOFSTEP]
rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this 
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : 0 = 0 ∧ 1 = 0 ∨ 1 = 0 ∧ 0 = 0
⊢ False
[PROOFSTEP]
rcases this with (⟨_, h⟩ | ⟨h, _⟩)
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False
[PROOFSTEP]
exact zero_ne_one h.symm
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False
[PROOFSTEP]
exact zero_ne_one h.symm
