case mp
a b : Int
h : natAbs a = natAbs b
⊢ a = b ∨ a = -b

case mpr
a b : Int
h : a = b ∨ a = -b
⊢ natAbs a = natAbs b
a b : Int
⊢ natAbs a = natAbs b ↔ a = b ∨ a = -b
constructor <;> intro h
no goals
case mp
a b : Int
h : natAbs a = natAbs b
⊢ a = b ∨ a = -b
cases Int.natAbs_eq a with
| inl h₁ | inr h₁ =>
  cases Int.natAbs_eq b with
  | inl h₂ | inr h₂ => rw [h₁, h₂]; simp [h]
no goals
case mp.inr
a b : Int
h : natAbs a = natAbs b
h₁ : a = -↑(natAbs a)
⊢ a = b ∨ a = -b
cases Int.natAbs_eq b with
| inl h₂ | inr h₂ => rw [h₁, h₂]; simp [h]
case mp.inr.inr
a b : Int
h : natAbs a = natAbs b
h₁ : a = -↑(natAbs a)
h₂ : b = -↑(natAbs b)
⊢ -↑(natAbs a) = -↑(natAbs b) ∨ -↑(natAbs a) = - -↑(natAbs b)
case mp.inr.inr
a b : Int
h : natAbs a = natAbs b
h₁ : a = -↑(natAbs a)
h₂ : b = -↑(natAbs b)
⊢ a = b ∨ a = -b
rw [h₁, h₂]
no goals
case mp.inr.inr
a b : Int
h : natAbs a = natAbs b
h₁ : a = -↑(natAbs a)
h₂ : b = -↑(natAbs b)
⊢ -↑(natAbs a) = -↑(natAbs b) ∨ -↑(natAbs a) = - -↑(natAbs b)
simp [h]
no goals
case mpr
a b : Int
h : a = b ∨ a = -b
⊢ natAbs a = natAbs b
cases h with (subst a; try rfl)
| inr h => rw [Int.natAbs_neg]
case mpr.inl
b : Int
⊢ natAbs b = natAbs b
case mpr.inl
a b : Int
h✝ : a = b
⊢ natAbs a = natAbs b
subst a
no goals
case mpr.inl
b : Int
⊢ natAbs b = natAbs b
try rfl
no goals
case mpr.inl
b : Int
⊢ natAbs b = natAbs b
rfl
no goals
case mpr.inr
b : Int
⊢ natAbs (-b) = natAbs b
rw [Int.natAbs_neg]