[GOAL]
u : ℤˣ
⊢ natAbs ↑u * natAbs ↑u⁻¹ = 1
[PROOFSTEP]
rw [← natAbs_mul, Units.mul_inv]
[GOAL]
u : ℤˣ
⊢ natAbs 1 = 1
[PROOFSTEP]
rfl
[GOAL]
u : ℤˣ
⊢ natAbs ↑u⁻¹ * natAbs ↑u = 1
[PROOFSTEP]
rw [← natAbs_mul, Units.inv_mul]
[GOAL]
u : ℤˣ
⊢ natAbs 1 = 1
[PROOFSTEP]
rfl
[GOAL]
u : ℤˣ
⊢ u = 1 ∨ u = -1
[PROOFSTEP]
simpa only [Units.ext_iff, units_natAbs] using natAbs_eq u
[GOAL]
a : ℤ
⊢ IsUnit a ↔ a = 1 ∨ a = -1
[PROOFSTEP]
refine' ⟨fun h => isUnit_eq_one_or h, fun h => _⟩
[GOAL]
a : ℤ
h : a = 1 ∨ a = -1
⊢ IsUnit a
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case inl
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
case inr
⊢ IsUnit (-1)
[PROOFSTEP]
exact isUnit_one.neg
[GOAL]
a b : ℤ
ha : IsUnit a
hb : IsUnit b
⊢ a = b ∨ a = -b
[PROOFSTEP]
rcases isUnit_eq_one_or hb with (rfl | rfl)
[GOAL]
case inl
a : ℤ
ha : IsUnit a
hb : IsUnit 1
⊢ a = 1 ∨ a = -1
[PROOFSTEP]
exact isUnit_eq_one_or ha
[GOAL]
case inr
a : ℤ
ha : IsUnit a
hb : IsUnit (-1)
⊢ a = -1 ∨ a = - -1
[PROOFSTEP]
rwa [or_comm, neg_neg, ← isUnit_iff]
[GOAL]
z w : ℤ
h : z * w = 1
⊢ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
[PROOFSTEP]
have h' : w * z = 1 := mul_comm z w ▸ h
[GOAL]
z w : ℤ
h : z * w = 1
h' : w * z = 1
⊢ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
[PROOFSTEP]
rcases eq_one_or_neg_one_of_mul_eq_one h with (rfl | rfl)
[GOAL]
case inl
w : ℤ
h : 1 * w = 1
h' : w * 1 = 1
⊢ 1 = 1 ∧ w = 1 ∨ 1 = -1 ∧ w = -1
[PROOFSTEP]
rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl)
[GOAL]
case inr
w : ℤ
h : -1 * w = 1
h' : w * -1 = 1
⊢ -1 = 1 ∧ w = 1 ∨ -1 = -1 ∧ w = -1
[PROOFSTEP]
rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl)
[GOAL]
case inl.inl
h h' : 1 * 1 = 1
⊢ 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
[PROOFSTEP]
tauto
[GOAL]
case inl.inr
h : 1 * -1 = 1
h' : -1 * 1 = 1
⊢ 1 = 1 ∧ -1 = 1 ∨ 1 = -1 ∧ -1 = -1
[PROOFSTEP]
tauto
[GOAL]
case inr.inl
h : -1 * 1 = 1
h' : 1 * -1 = 1
⊢ -1 = 1 ∧ 1 = 1 ∨ -1 = -1 ∧ 1 = -1
[PROOFSTEP]
tauto
[GOAL]
case inr.inr
h h' : -1 * -1 = 1
⊢ -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
[PROOFSTEP]
tauto
[GOAL]
z w : ℤ
⊢ z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
[PROOFSTEP]
refine' ⟨eq_one_or_neg_one_of_mul_eq_one', fun h => Or.elim h (fun H => _) fun H => _⟩
[GOAL]
case refine'_1
z w : ℤ
h : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
H : z = 1 ∧ w = 1
⊢ z * w = 1
[PROOFSTEP]
rcases H with ⟨rfl, rfl⟩
[GOAL]
case refine'_2
z w : ℤ
h : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
H : z = -1 ∧ w = -1
⊢ z * w = 1
[PROOFSTEP]
rcases H with ⟨rfl, rfl⟩
[GOAL]
case refine'_1.intro
h : 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
⊢ 1 * 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.intro
h : -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
⊢ -1 * -1 = 1
[PROOFSTEP]
rfl
[GOAL]
z w : ℤ
h : z * w = -1
⊢ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
[PROOFSTEP]
rcases isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1 with (rfl | rfl)
[GOAL]
case inl
w : ℤ
h : 1 * w = -1
⊢ 1 = 1 ∧ w = -1 ∨ 1 = -1 ∧ w = 1
[PROOFSTEP]
exact Or.inl ⟨rfl, one_mul w ▸ h⟩
[GOAL]
case inr
w : ℤ
h : -1 * w = -1
⊢ -1 = 1 ∧ w = -1 ∨ -1 = -1 ∧ w = 1
[PROOFSTEP]
exact Or.inr ⟨rfl, neg_inj.mp (neg_one_mul w ▸ h)⟩
[GOAL]
z w : ℤ
⊢ z * w = -1 ↔ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
[PROOFSTEP]
refine' ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h => Or.elim h (fun H => _) fun H => _⟩
[GOAL]
case refine'_1
z w : ℤ
h : z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
H : z = 1 ∧ w = -1
⊢ z * w = -1
[PROOFSTEP]
rcases H with ⟨rfl, rfl⟩
[GOAL]
case refine'_2
z w : ℤ
h : z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
H : z = -1 ∧ w = 1
⊢ z * w = -1
[PROOFSTEP]
rcases H with ⟨rfl, rfl⟩
[GOAL]
case refine'_1.intro
h : 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
⊢ 1 * -1 = -1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.intro
h : -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
⊢ -1 * 1 = -1
[PROOFSTEP]
rfl
[GOAL]
n : ℤ
⊢ IsUnit n ↔ natAbs n = 1
[PROOFSTEP]
simp [natAbs_eq_iff, isUnit_iff, Nat.cast_zero]
[GOAL]
n : ℕ
⊢ IsUnit ↑n ↔ IsUnit n
[PROOFSTEP]
simp [isUnit_iff_natAbs_eq]
[GOAL]
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
rw [isUnit_iff] at ha hb hc hd 
[GOAL]
a b c d : ℤ
ha : a = 1 ∨ a = -1
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases ha
[GOAL]
case inl
a b c d : ℤ
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝ : a = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hb
[GOAL]
case inr
a b c d : ℤ
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝ : a = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hb
[GOAL]
case inl.inl
a b c d : ℤ
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝¹ : a = 1
h✝ : b = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hc
[GOAL]
case inl.inr
a b c d : ℤ
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝¹ : a = 1
h✝ : b = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hc
[GOAL]
case inr.inl
a b c d : ℤ
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝¹ : a = -1
h✝ : b = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hc
[GOAL]
case inr.inr
a b c d : ℤ
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝¹ : a = -1
h✝ : b = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hc
[GOAL]
case inl.inl.inl
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = 1
h✝¹ : b = 1
h✝ : c = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inl.inl.inr
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = 1
h✝¹ : b = 1
h✝ : c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inl.inr.inl
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = 1
h✝¹ : b = -1
h✝ : c = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inl.inr.inr
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = 1
h✝¹ : b = -1
h✝ : c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inr.inl.inl
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = -1
h✝¹ : b = 1
h✝ : c = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inr.inl.inr
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = -1
h✝¹ : b = 1
h✝ : c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inr.inr.inl
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = -1
h✝¹ : b = -1
h✝ : c = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inr.inr.inr
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = -1
h✝¹ : b = -1
h✝ : c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inl.inl.inl.inl
a b c d : ℤ
h✝³ : a = 1
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inl.inl.inr
a b c d : ℤ
h✝³ : a = 1
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inl.inr.inl
a b c d : ℤ
h✝³ : a = 1
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inl.inr.inr
a b c d : ℤ
h✝³ : a = 1
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inr.inl.inl
a b c d : ℤ
h✝³ : a = 1
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inr.inl.inr
a b c d : ℤ
h✝³ : a = 1
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inr.inr.inl
a b c d : ℤ
h✝³ : a = 1
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inr.inr.inr
a b c d : ℤ
h✝³ : a = 1
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inl.inl.inl
a b c d : ℤ
h✝³ : a = -1
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inl.inl.inr
a b c d : ℤ
h✝³ : a = -1
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inl.inr.inl
a b c d : ℤ
h✝³ : a = -1
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inl.inr.inr
a b c d : ℤ
h✝³ : a = -1
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inr.inl.inl
a b c d : ℤ
h✝³ : a = -1
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inr.inl.inr
a b c d : ℤ
h✝³ : a = -1
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inr.inr.inl
a b c d : ℤ
h✝³ : a = -1
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inr.inr.inr
a b c d : ℤ
h✝³ : a = -1
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inl.inl.inl
b c d : ℤ
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = 1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inl.inl.inr
b c d : ℤ
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = -1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inl.inr.inl
b c d : ℤ
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = 1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inl.inr.inr
b c d : ℤ
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = -1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inr.inl.inl
b c d : ℤ
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = 1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inr.inl.inr
b c d : ℤ
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = -1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inr.inr.inl
b c d : ℤ
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = 1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inr.inr.inr
b c d : ℤ
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = -1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inl.inl.inl
b c d : ℤ
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = 1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inl.inl.inr
b c d : ℤ
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = -1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inl.inr.inl
b c d : ℤ
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = 1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inl.inr.inr
b c d : ℤ
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = -1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inr.inl.inl
b c d : ℤ
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = 1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inr.inl.inr
b c d : ℤ
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = -1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inr.inr.inl
b c d : ℤ
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = 1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inr.inr.inr
b c d : ℤ
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = -1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inl.inl.inl
c d : ℤ
h✝¹ : c = 1
h✝ : d = 1
⊢ 1 + 1 = c + d ↔ 1 = c ∧ 1 = d ∨ 1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inl.inl.inr
c d : ℤ
h✝¹ : c = 1
h✝ : d = -1
⊢ 1 + 1 = c + d ↔ 1 = c ∧ 1 = d ∨ 1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inl.inr.inl
c d : ℤ
h✝¹ : c = -1
h✝ : d = 1
⊢ 1 + 1 = c + d ↔ 1 = c ∧ 1 = d ∨ 1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inl.inr.inr
c d : ℤ
h✝¹ : c = -1
h✝ : d = -1
⊢ 1 + 1 = c + d ↔ 1 = c ∧ 1 = d ∨ 1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inr.inl.inl
c d : ℤ
h✝¹ : c = 1
h✝ : d = 1
⊢ 1 + -1 = c + d ↔ 1 = c ∧ -1 = d ∨ 1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inr.inl.inr
c d : ℤ
h✝¹ : c = 1
h✝ : d = -1
⊢ 1 + -1 = c + d ↔ 1 = c ∧ -1 = d ∨ 1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inr.inr.inl
c d : ℤ
h✝¹ : c = -1
h✝ : d = 1
⊢ 1 + -1 = c + d ↔ 1 = c ∧ -1 = d ∨ 1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inr.inr.inr
c d : ℤ
h✝¹ : c = -1
h✝ : d = -1
⊢ 1 + -1 = c + d ↔ 1 = c ∧ -1 = d ∨ 1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inl.inl.inl
c d : ℤ
h✝¹ : c = 1
h✝ : d = 1
⊢ -1 + 1 = c + d ↔ -1 = c ∧ 1 = d ∨ -1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inl.inl.inr
c d : ℤ
h✝¹ : c = 1
h✝ : d = -1
⊢ -1 + 1 = c + d ↔ -1 = c ∧ 1 = d ∨ -1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inl.inr.inl
c d : ℤ
h✝¹ : c = -1
h✝ : d = 1
⊢ -1 + 1 = c + d ↔ -1 = c ∧ 1 = d ∨ -1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inl.inr.inr
c d : ℤ
h✝¹ : c = -1
h✝ : d = -1
⊢ -1 + 1 = c + d ↔ -1 = c ∧ 1 = d ∨ -1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inr.inl.inl
c d : ℤ
h✝¹ : c = 1
h✝ : d = 1
⊢ -1 + -1 = c + d ↔ -1 = c ∧ -1 = d ∨ -1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inr.inl.inr
c d : ℤ
h✝¹ : c = 1
h✝ : d = -1
⊢ -1 + -1 = c + d ↔ -1 = c ∧ -1 = d ∨ -1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inr.inr.inl
c d : ℤ
h✝¹ : c = -1
h✝ : d = 1
⊢ -1 + -1 = c + d ↔ -1 = c ∧ -1 = d ∨ -1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inr.inr.inr
c d : ℤ
h✝¹ : c = -1
h✝ : d = -1
⊢ -1 + -1 = c + d ↔ -1 = c ∧ -1 = d ∨ -1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inl.inl.inl
d : ℤ
h✝ : d = 1
⊢ 1 + 1 = 1 + d ↔ 1 = 1 ∧ 1 = d ∨ 1 = d ∧ 1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inl.inl.inl.inr
d : ℤ
h✝ : d = -1
⊢ 1 + 1 = 1 + d ↔ 1 = 1 ∧ 1 = d ∨ 1 = d ∧ 1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inl.inl.inr.inl
d : ℤ
h✝ : d = 1
⊢ 1 + 1 = -1 + d ↔ 1 = -1 ∧ 1 = d ∨ 1 = d ∧ 1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inl.inl.inr.inr
d : ℤ
h✝ : d = -1
⊢ 1 + 1 = -1 + d ↔ 1 = -1 ∧ 1 = d ∨ 1 = d ∧ 1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inl.inr.inl.inl
d : ℤ
h✝ : d = 1
⊢ 1 + -1 = 1 + d ↔ 1 = 1 ∧ -1 = d ∨ 1 = d ∧ -1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inl.inr.inl.inr
d : ℤ
h✝ : d = -1
⊢ 1 + -1 = 1 + d ↔ 1 = 1 ∧ -1 = d ∨ 1 = d ∧ -1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inl.inr.inr.inl
d : ℤ
h✝ : d = 1
⊢ 1 + -1 = -1 + d ↔ 1 = -1 ∧ -1 = d ∨ 1 = d ∧ -1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inl.inr.inr.inr
d : ℤ
h✝ : d = -1
⊢ 1 + -1 = -1 + d ↔ 1 = -1 ∧ -1 = d ∨ 1 = d ∧ -1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inr.inl.inl.inl
d : ℤ
h✝ : d = 1
⊢ -1 + 1 = 1 + d ↔ -1 = 1 ∧ 1 = d ∨ -1 = d ∧ 1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inr.inl.inl.inr
d : ℤ
h✝ : d = -1
⊢ -1 + 1 = 1 + d ↔ -1 = 1 ∧ 1 = d ∨ -1 = d ∧ 1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inr.inl.inr.inl
d : ℤ
h✝ : d = 1
⊢ -1 + 1 = -1 + d ↔ -1 = -1 ∧ 1 = d ∨ -1 = d ∧ 1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inr.inl.inr.inr
d : ℤ
h✝ : d = -1
⊢ -1 + 1 = -1 + d ↔ -1 = -1 ∧ 1 = d ∨ -1 = d ∧ 1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inr.inr.inl.inl
d : ℤ
h✝ : d = 1
⊢ -1 + -1 = 1 + d ↔ -1 = 1 ∧ -1 = d ∨ -1 = d ∧ -1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inr.inr.inl.inr
d : ℤ
h✝ : d = -1
⊢ -1 + -1 = 1 + d ↔ -1 = 1 ∧ -1 = d ∨ -1 = d ∧ -1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inr.inr.inr.inl
d : ℤ
h✝ : d = 1
⊢ -1 + -1 = -1 + d ↔ -1 = -1 ∧ -1 = d ∨ -1 = d ∧ -1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inr.inr.inr.inr
d : ℤ
h✝ : d = -1
⊢ -1 + -1 = -1 + d ↔ -1 = -1 ∧ -1 = d ∨ -1 = d ∧ -1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inl.inl.inl.inl
⊢ 1 + 1 = 1 + 1 ↔ 1 = 1 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inl.inr
⊢ 1 + 1 = 1 + -1 ↔ 1 = 1 ∧ 1 = -1 ∨ 1 = -1 ∧ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr.inl
⊢ 1 + 1 = -1 + 1 ↔ 1 = -1 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = -1
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr.inr
⊢ 1 + 1 = -1 + -1 ↔ 1 = -1 ∧ 1 = -1 ∨ 1 = -1 ∧ 1 = -1
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl.inl
⊢ 1 + -1 = 1 + 1 ↔ 1 = 1 ∧ -1 = 1 ∨ 1 = 1 ∧ -1 = 1
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl.inr
⊢ 1 + -1 = 1 + -1 ↔ 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr.inl
⊢ 1 + -1 = -1 + 1 ↔ 1 = -1 ∧ -1 = 1 ∨ 1 = 1 ∧ -1 = -1
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr.inr
⊢ 1 + -1 = -1 + -1 ↔ 1 = -1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = -1
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl.inl
⊢ -1 + 1 = 1 + 1 ↔ -1 = 1 ∧ 1 = 1 ∨ -1 = 1 ∧ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl.inr
⊢ -1 + 1 = 1 + -1 ↔ -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr.inl
⊢ -1 + 1 = -1 + 1 ↔ -1 = -1 ∧ 1 = 1 ∨ -1 = 1 ∧ 1 = -1
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr.inr
⊢ -1 + 1 = -1 + -1 ↔ -1 = -1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = -1
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl.inl
⊢ -1 + -1 = 1 + 1 ↔ -1 = 1 ∧ -1 = 1 ∨ -1 = 1 ∧ -1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl.inr
⊢ -1 + -1 = 1 + -1 ↔ -1 = 1 ∧ -1 = -1 ∨ -1 = -1 ∧ -1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr.inl
⊢ -1 + -1 = -1 + 1 ↔ -1 = -1 ∧ -1 = 1 ∨ -1 = 1 ∧ -1 = -1
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr.inr
⊢ -1 + -1 = -1 + -1 ↔ -1 = -1 ∧ -1 = -1 ∨ -1 = -1 ∧ -1 = -1
[PROOFSTEP]
simp
