α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : (0, 1) = 0 ∨ (1, 0) = 0
⊢ False
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ False
have :=
  NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
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
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : (0, 1) = 0 ∨ (1, 0) = 0
⊢ False
rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this
case inl.intro
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False

case inr.intro
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
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
rcases this with (⟨_, h⟩ | ⟨h, _⟩)
no goals
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ (0, 1) * (1, 0) = 0
simp
no goals
case inl.intro
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False
exact zero_ne_one h.symm
no goals
case inr.intro
α : Type ?u.54070
β : Type ?u.54073
R✝ : Type ?u.54076
R' : Type ?u.54079
S✝ : Type ?u.54082
S' : Type ?u.54085
T : Type ?u.54088
T' : Type ?u.54091
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False
exact zero_ne_one h.symm