Theorem: C03S05.MyAbs.abs_ltαα (MIL/C03_Logic/S05_Disjunction.lean)

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

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

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

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

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

State before:
case inl.mpr
x y : ℝ
h : 0 ≤ x
⊢ -y < x ∧ x < y → x < y
Tactic:
. intro h'
  rcases h' with ⟨h1, h2⟩
  exact h2
State after:
no goals

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

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

case inl.mp.right
x y : ℝ
h : 0 ≤ x
h' : x < y
⊢ x < y

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

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

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

State before:
case inl.mpr
x y : ℝ
h : 0 ≤ x
h' : -y < x ∧ x < y
⊢ x < y
Tactic:
rcases h' with ⟨h1, h2⟩
State after:
case inl.mpr.intro
x y : ℝ
h : 0 ≤ x
h1 : -y < x
h2 : x < y
⊢ x < y

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

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

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

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

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

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

State before:
case inr.mp
x y : ℝ
h : 0 > x
h' : -x < y
⊢ -y < x ∧ x < y
Tactic:
constructor
State after:
case inr.mp.left
x y : ℝ
h : 0 > x
h' : -x < y
⊢ -y < x

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

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

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

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

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

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