Theorem: Real.exp_iff_expCone (CvxLean/Lib/Cones/ExpCone.lean)

State before:
t x : ℝ
⊢ x.exp ≤ t ↔ x.expCone 1 t
Tactic:
unfold expCone
State after:
t x : ℝ
⊢ x.exp ≤ t ↔ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0

State before:
t x : ℝ
⊢ x.exp ≤ t ↔ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
Tactic:
rw [iff_def]
State after:
t x : ℝ
⊢ (x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0) ∧
    (0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t)

State before:
t x : ℝ
⊢ (x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0) ∧
    (0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t)
Tactic:
split_ands
State after:
case refine_1
t x : ℝ
⊢ x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0

case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t

State before:
case refine_1
t x : ℝ
⊢ x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0

case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t
Tactic:
{ intro hexp
  apply Or.intro_left
  split_ands
  { apply Real.zero_lt_one }
  { rwa [div_one, one_mul] } }
State after:
case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t

State before:
case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t
Tactic:
{ intro h
  cases h with
  | inl h =>
      have h : 1 * exp (x / 1) ≤ t := h.2
      rwa [div_one, one_mul] at h
  | inr h =>
      exfalso
      exact zero_ne_one h.1.symm }
State after:
no goals

State before:
case refine_1
t x : ℝ
⊢ x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
Tactic:
intro hexp
State after:
case refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0

State before:
case refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
Tactic:
apply Or.intro_left
State after:
case refine_1.h
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t

State before:
case refine_1.h
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t
Tactic:
split_ands
State after:
case refine_1.h.refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1

case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t

State before:
case refine_1.h.refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1

case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t
Tactic:
{ apply Real.zero_lt_one }
State after:
case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t

State before:
case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t
Tactic:
{ rwa [div_one, one_mul] }
State after:
no goals

State before:
case refine_1.h.refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1
Tactic:
apply Real.zero_lt_one
State after:
no goals

State before:
case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t
Tactic:
rwa [div_one, one_mul]
State after:
no goals

State before:
case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t
Tactic:
intro h
State after:
case refine_2
t x : ℝ
h : 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ x.exp ≤ t

State before:
case refine_2
t x : ℝ
h : 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ x.exp ≤ t
Tactic:
cases h with
| inl h =>
    have h : 1 * exp (x / 1) ≤ t := h.2
    rwa [div_one, one_mul] at h
| inr h =>
    exfalso
    exact zero_ne_one h.1.symm
State after:
no goals

State before:
case refine_2.inl
t x : ℝ
h : 0 < 1 ∧ 1 * (x / 1).exp ≤ t
⊢ x.exp ≤ t
Tactic:
have h : 1 * exp (x / 1) ≤ t := h.2
State after:
case refine_2.inl
t x : ℝ
h✝ : 0 < 1 ∧ 1 * (x / 1).exp ≤ t
h : 1 * (x / 1).exp ≤ t
⊢ x.exp ≤ t

State before:
case refine_2.inl
t x : ℝ
h✝ : 0 < 1 ∧ 1 * (x / 1).exp ≤ t
h : 1 * (x / 1).exp ≤ t
⊢ x.exp ≤ t
Tactic:
rwa [div_one, one_mul] at h
State after:
no goals

State before:
case refine_2.inr
t x : ℝ
h : 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ x.exp ≤ t
Tactic:
exfalso
State after:
case refine_2.inr
t x : ℝ
h : 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ False

State before:
case refine_2.inr
t x : ℝ
h : 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ False
Tactic:
exact zero_ne_one h.1.symm
State after:
no goals