R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a : ℤ
ha : a ∈ {0, 1, -1}
b : ℤ
hb : b ∈ {0, 1, -1}
h : ↑a = ↑b
⊢ a = b
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ Set.InjOn Int.cast {0, 1, -1}
intro a ha b hb h
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a : ℤ
ha : a ∈ {0, 1, -1}
b : ℤ
hb : b ∈ {0, 1, -1}
h : ↑a = ↑b
⊢ a - b = 0
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a : ℤ
ha : a ∈ {0, 1, -1}
b : ℤ
hb : b ∈ {0, 1, -1}
h : ↑a = ↑b
⊢ a = b
apply eq_of_sub_eq_zero
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a : ℤ
ha : a ∈ {0, 1, -1}
b : ℤ
hb : b ∈ {0, 1, -1}
h : ↑a = ↑b
hf : ¬a - b = 0
⊢ False
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a : ℤ
ha : a ∈ {0, 1, -1}
b : ℤ
hb : b ∈ {0, 1, -1}
h : ↑a = ↑b
⊢ a - b = 0
by_contra hf
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
hb : b ∈ {0, 1, -1}
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
⊢ False
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a : ℤ
ha : a ∈ {0, 1, -1}
b : ℤ
hb : b ∈ {0, 1, -1}
h : ↑a = ↑b
hf : ¬a - b = 0
⊢ False
replace ha : a = 0 ∨ a = 1 ∨ a = -1 := ha
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
⊢ False
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
hb : b ∈ {0, 1, -1}
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
⊢ False
replace hb : b = 0 ∨ b = 1 ∨ b = -1 := hb
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
⊢ False
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
⊢ False
have hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2 := by
  rcases ha with (ha | ha | ha) <;> rcases hb with (hb | hb | hb)
  pick_goal 5
  pick_goal 9
  iterate 3 rw [ha, hb, sub_self] at hf; tauto
  all_goals rw [ha, hb]; norm_num
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
h' : ↑(a - b) = 0
⊢ False
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
⊢ False
have h' : ((a - b : ℤ) : R) = 0 := by exact_mod_cast sub_eq_zero_of_eq h
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
⊢ False
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
h' : ↑(a - b) = 0
⊢ False
have h'' : ((b - a : ℤ) : R) = 0 := by exact_mod_cast sub_eq_zero_of_eq h.symm
case h.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
hh : a - b = 1
⊢ False

case h.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
hh : b - a = 1
⊢ False

case h.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
hh : a - b = 2
⊢ False

case h.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
hh : b - a = 2
⊢ False
case h
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
⊢ False
rcases hh with (hh | hh | hh | hh)
case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
rcases ha with (ha | ha | ha) <;> rcases hb with (hb | hb | hb)
case inr.inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
pick_goal 5
case inr.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
case inr.inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
pick_goal 9
case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
case inr.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
iterate 3 rw [ha, hb, sub_self] at hf; tauto
no goals
case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
all_goals rw [ha, hb]; norm_num
case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬0 = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
rw [ha, hb, sub_self] at hf
case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
case inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬0 = 0
ha : a = 0
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inl.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 1
hb : b = -1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 0
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2

case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
tauto
case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ -1 - 1 = 1 ∨ 1 - -1 = 1 ∨ -1 - 1 = 2 ∨ 1 - -1 = 2
case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
rw [ha, hb]
no goals
case inr.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = -1
hb : b = 1
⊢ -1 - 1 = 1 ∨ 1 - -1 = 1 ∨ -1 - 1 = 2 ∨ 1 - -1 = 2
norm_num
no goals
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
⊢ ↑(a - b) = 0
exact_mod_cast sub_eq_zero_of_eq h
no goals
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2
h' : ↑(a - b) = 0
⊢ ↑(b - a) = 0
exact_mod_cast sub_eq_zero_of_eq h.symm
case h.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : 1 = 0
h'' : ↑(b - a) = 0
hh : a - b = 1
⊢ False
case h.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
hh : a - b = 1
⊢ False
rw [hh, (by norm_cast : ((1 : ℤ) : R) = 1)] at h'
no goals
case h.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : 1 = 0
h'' : ↑(b - a) = 0
hh : a - b = 1
⊢ False
exact one_ne_zero h'
no goals
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑1 = 0
h'' : ↑(b - a) = 0
hh : a - b = 1
⊢ ↑1 = 1
norm_cast
case h.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : 1 = 0
hh : b - a = 1
⊢ False
case h.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
hh : b - a = 1
⊢ False
rw [hh, (by norm_cast : ((1 : ℤ) : R) = 1)] at h''
no goals
case h.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : 1 = 0
hh : b - a = 1
⊢ False
exact one_ne_zero h''
no goals
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑1 = 0
hh : b - a = 1
⊢ ↑1 = 1
norm_cast
case h.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : 2 = 0
h'' : ↑(b - a) = 0
hh : a - b = 2
⊢ False
case h.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
hh : a - b = 2
⊢ False
rw [hh, (by norm_cast : ((2 : ℤ) : R) = 2)] at h'
no goals
case h.inr.inr.inl
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : 2 = 0
h'' : ↑(b - a) = 0
hh : a - b = 2
⊢ False
exact Ring.two_ne_zero hR h'
no goals
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑2 = 0
h'' : ↑(b - a) = 0
hh : a - b = 2
⊢ ↑2 = 2
norm_cast
case h.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : 2 = 0
hh : b - a = 2
⊢ False
case h.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑(b - a) = 0
hh : b - a = 2
⊢ False
rw [hh, (by norm_cast : ((2 : ℤ) : R) = 2)] at h''
no goals
case h.inr.inr.inr
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : 2 = 0
hh : b - a = 2
⊢ False
exact Ring.two_ne_zero hR h''
no goals
R✝ : Type ?u.964532
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
a b : ℤ
h : ↑a = ↑b
hf : ¬a - b = 0
ha : a = 0 ∨ a = 1 ∨ a = -1
hb : b = 0 ∨ b = 1 ∨ b = -1
h' : ↑(a - b) = 0
h'' : ↑2 = 0
hh : b - a = 2
⊢ ↑2 = 2
norm_cast