Theorem: Romania1998P12.romania1998_p12_mpr (Compfiles/Romania1998P12.lean)

State before:
u : ℝ → ℝ
⊢ (∃ k, ∀ (x : ℝ), u x = (k * x).exp) → ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
rintro ⟨k, hk⟩
State after:
case intro
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y

State before:
case intro
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
obtain rfl | hknz := eq_or_ne k 0
State after:
case intro.inl
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y

case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y

State before:
case intro.inl
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
use id
State after:
case h
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ (StrictMono id ∨ StrictAnti id) ∧ ∀ (x y : ℝ), id (x + y) = id x * u y + id y

State before:
case h
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ (StrictMono id ∨ StrictAnti id) ∧ ∀ (x y : ℝ), id (x + y) = id x * u y + id y
Tactic:
constructor
State after:
case h.left
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ StrictMono id ∨ StrictAnti id

case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∀ (x y : ℝ), id (x + y) = id x * u y + id y

State before:
case h.left
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ StrictMono id ∨ StrictAnti id
Tactic:
left
State after:
case h.left.h
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ StrictMono id

State before:
case h.left.h
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ StrictMono id
Tactic:
exact strictMono_id
State after:
no goals

State before:
case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∀ (x y : ℝ), id (x + y) = id x * u y + id y
Tactic:
intro x y
State after:
case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
x y : ℝ
⊢ id (x + y) = id x * u y + id y

State before:
case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
x y : ℝ
⊢ id (x + y) = id x * u y + id y
Tactic:
rw [hk y, zero_mul, Real.exp_zero, mul_one, id_def, id_def, id_def]
State after:
no goals

State before:
case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
let f : ℝ → ℝ := λ x ↦ Real.exp (k * x) - 1
State after:
case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y

State before:
case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
use f
State after:
case h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y

State before:
case h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
use hfm
State after:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ ∀ (x y : ℝ), f (x + y) = f x * u y + f y

State before:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
intro x y
State after:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * u y + f y

State before:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * u y + f y
Tactic:
rw [hk y]
State after:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * (k * y).exp + f y

State before:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * (k * y).exp + f y
Tactic:
calc Real.exp (k * (x + y)) - 1
         = Real.exp (k * x + k * y) - 1 := by rw [mul_add]
       _ = Real.exp (k * x) * Real.exp (k * y) - 1 := by rw [Real.exp_add]
       _ = (Real.exp (k * x) - 1) * Real.exp (k * y) +
              (Real.exp (k * y) - 1) := by ring
State after:
no goals

State before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
⊢ StrictMono f ∨ StrictAnti f
Tactic:
cases' Classical.em (0 < k) with hkp hkn
State after:
case inl
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
⊢ StrictMono f ∨ StrictAnti f

case inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
⊢ StrictMono f ∨ StrictAnti f

State before:
case inl
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
⊢ StrictMono f ∨ StrictAnti f
Tactic:
left
State after:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
⊢ StrictMono f

State before:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
⊢ StrictMono f
Tactic:
intro x y hxy
State after:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
x y : ℝ
hxy : x < y
⊢ f x < f y

State before:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
x y : ℝ
hxy : x < y
⊢ f x < f y
Tactic:
have := exp_strict_mono' k x y hkp hxy
State after:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
x y : ℝ
hxy : x < y
this : (k * x).exp < (k * y).exp
⊢ f x < f y

State before:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
x y : ℝ
hxy : x < y
this : (k * x).exp < (k * y).exp
⊢ f x < f y
Tactic:
exact sub_lt_sub_right this 1
State after:
no goals

State before:
case inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
⊢ StrictMono f ∨ StrictAnti f
Tactic:
right
State after:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
⊢ StrictAnti f

State before:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
⊢ StrictAnti f
Tactic:
intro x y hxy
State after:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
⊢ f y < f x

State before:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
⊢ f y < f x
Tactic:
have hkn' : k < 0 := by
  simp only [not_lt] at *
  exact Ne.lt_of_le hknz hkn
State after:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
⊢ f y < f x

State before:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
⊢ f y < f x
Tactic:
have := exp_strict_anti' k x y hkn' hxy
State after:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
this : (k * y).exp < (k * x).exp
⊢ f y < f x

State before:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
this : (k * y).exp < (k * x).exp
⊢ f y < f x
Tactic:
exact sub_lt_sub_right this 1
State after:
no goals

State before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
⊢ k < 0
Tactic:
simp only [not_lt] at *
State after:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
x y : ℝ
hxy : x < y
hkn : k ≤ 0
⊢ k < 0

State before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
x y : ℝ
hxy : x < y
hkn : k ≤ 0
⊢ k < 0
Tactic:
exact Ne.lt_of_le hknz hkn
State after:
no goals

State before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ (k * (x + y)).exp - 1 = (k * x + k * y).exp - 1
Tactic:
rw [mul_add]
State after:
no goals

State before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ (k * x + k * y).exp - 1 = (k * x).exp * (k * y).exp - 1
Tactic:
rw [Real.exp_add]
State after:
no goals

State before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ (k * x).exp * (k * y).exp - 1 = ((k * x).exp - 1) * (k * y).exp + ((k * y).exp - 1)
Tactic:
ring
State after:
no goals