Theorem: C03S05.MyAbs.lt_abs (LeanInRome/S3_Logic/solutions/Solutions_S05_Disjunction.lean)

State before:
x y : ℝ
⊢ x < |y| ↔ x < y ∨ x < -y
Tactic:
rcases le_or_gt 0 y with h | h
State after:
case inl
x y : ℝ
h : 0 ≤ y
⊢ x < |y| ↔ x < y ∨ x < -y

case inr
x y : ℝ
h : 0 > y
⊢ x < |y| ↔ x < y ∨ x < -y

State before:
case inr
x y : ℝ
h : 0 > y
⊢ x < |y| ↔ x < y ∨ x < -y
Tactic:
rw [abs_of_neg h]
State after:
case inr
x y : ℝ
h : 0 > y
⊢ x < -y ↔ x < y ∨ x < -y

State before:
case inr
x y : ℝ
h : 0 > y
⊢ x < -y ↔ x < y ∨ x < -y
Tactic:
constructor
State after:
case inr.mp
x y : ℝ
h : 0 > y
⊢ x < -y → x < y ∨ x < -y

case inr.mpr
x y : ℝ
h : 0 > y
⊢ x < y ∨ x < -y → x < -y

State before:
case inl
x y : ℝ
h : 0 ≤ y
⊢ x < |y| ↔ x < y ∨ x < -y
Tactic:
rw [abs_of_nonneg h]
State after:
case inl
x y : ℝ
h : 0 ≤ y
⊢ x < y ↔ x < y ∨ x < -y

State before:
case inl
x y : ℝ
h : 0 ≤ y
⊢ x < y ↔ x < y ∨ x < -y
Tactic:
constructor
State after:
case inl.mp
x y : ℝ
h : 0 ≤ y
⊢ x < y → x < y ∨ x < -y

case inl.mpr
x y : ℝ
h : 0 ≤ y
⊢ x < y ∨ x < -y → x < y

State before:
case inl.mp
x y : ℝ
h : 0 ≤ y
⊢ x < y → x < y ∨ x < -y
Tactic:
intro h'
State after:
case inl.mp
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y ∨ x < -y

State before:
case inl.mp
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y ∨ x < -y
Tactic:
left
State after:
case inl.mp.h
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y

State before:
case inl.mp.h
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y
Tactic:
exact h'
State after:
no goals

State before:
case inl.mpr
x y : ℝ
h : 0 ≤ y
⊢ x < y ∨ x < -y → x < y
Tactic:
intro h'
State after:
case inl.mpr
x y : ℝ
h : 0 ≤ y
h' : x < y ∨ x < -y
⊢ x < y

State before:
case inl.mpr
x y : ℝ
h : 0 ≤ y
h' : x < y ∨ x < -y
⊢ x < y
Tactic:
rcases h' with h' | h'
State after:
case inl.mpr.inl
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y

case inl.mpr.inr
x y : ℝ
h : 0 ≤ y
h' : x < -y
⊢ x < y

State before:
case inl.mpr.inr
x y : ℝ
h : 0 ≤ y
h' : x < -y
⊢ x < y
Tactic:
. linarith
State after:
no goals

State before:
case inl.mpr.inl
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y
Tactic:
exact h'
State after:
no goals

State before:
case inl.mpr.inr
x y : ℝ
h : 0 ≤ y
h' : x < -y
⊢ x < y
Tactic:
linarith
State after:
no goals

State before:
case inr.mp
x y : ℝ
h : 0 > y
⊢ x < -y → x < y ∨ x < -y
Tactic:
intro h'
State after:
case inr.mp
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < y ∨ x < -y

State before:
case inr.mp
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < y ∨ x < -y
Tactic:
right
State after:
case inr.mp.h
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y

State before:
case inr.mp.h
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y
Tactic:
exact h'
State after:
no goals

State before:
case inr.mpr
x y : ℝ
h : 0 > y
⊢ x < y ∨ x < -y → x < -y
Tactic:
intro h'
State after:
case inr.mpr
x y : ℝ
h : 0 > y
h' : x < y ∨ x < -y
⊢ x < -y

State before:
case inr.mpr
x y : ℝ
h : 0 > y
h' : x < y ∨ x < -y
⊢ x < -y
Tactic:
rcases h' with h' | h'
State after:
case inr.mpr.inl
x y : ℝ
h : 0 > y
h' : x < y
⊢ x < -y

case inr.mpr.inr
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y

State before:
case inr.mpr.inr
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y
Tactic:
. exact h'
State after:
no goals

State before:
case inr.mpr.inl
x y : ℝ
h : 0 > y
h' : x < y
⊢ x < -y
Tactic:
linarith
State after:
no goals

State before:
case inr.mpr.inr
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y
Tactic:
exact h'
State after:
no goals