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

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

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

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hy0 : ∀ x : ℝ, f x = f x * u 0 + f 0 := by
  intro x; have := hf x 0; rw [add_zero] at this; exact this
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h0 : (u 0 ≠ 1) → ∀ x : ℝ, f x = f 0 / (1 - u 0) := by
  intro hu0 x
  have hy0x1 :=
              calc f 0 = f x - f x * u 0 := (sub_eq_of_eq_add' (hy0 x)).symm
              _ = f x * (1 - u 0) := by ring
  rw[hy0x1]
  have : 1 - u 0 ≠ 0 := sub_ne_zero.mpr hu0.symm
  field_simp
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
h0' : u 0 ≠ 1 → False
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h00 : u 0 = 1 := not_not.mp h0'
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
h0' : u 0 ≠ 1 → False
h00 : u 0 = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
h0' : u 0 ≠ 1 → False
h00 : u 0 = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
clear h0 h0'
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h00 : u 0 = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h00 : u 0 = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
rw [h00] at hy0
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hf0 : f 0 = 0 := by have := hy0 0; linarith
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h1 : ∀ x y : ℝ, f x * u y + f y = f x + f y * u x := by
  intro x y
  rw [←hf, add_comm]
  linarith[hf y x]
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h2 : ∀ x y : ℝ, f x * (u y - 1) = f y * (u x - 1) := by
  intro x y; linarith [h1 x y]
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h3 : ∀ x y : ℝ, x ≠ 0 → y ≠ 0 → (u x - 1) / f x =  (u y - 1) / f y := by
  intro x y hx hy
  have hx1 := hfx0 x hx
  have hy1 := hfx0 y hy
  have := h2 x y
  field_simp
  linarith
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h4: ∃ C : ℝ, ∀ x : ℝ, x ≠ 0 → (u x - 1) / f x = C := by
  use (u 1 - 1) / f 1
  intro x hx
  exact h3 x 1 hx one_ne_zero
State after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
h4 : ∃ C, ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
h4 : ∃ C, ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
obtain ⟨C, hC⟩ := h4
State after:
case intro.intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h5 : ∀ x : ℝ, x ≠ 0 → u x = 1 + C * f x := by
  intro x hx
  have hc1 := hC x hx
  have hx1 := hfx0 x hx
  field_simp at hc1
  linarith
State after:
case intro.intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
cases' em (C = 0) with hCz hCnz
State after:
case intro.intro.intro.inl
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

case intro.intro.intro.inr
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro.intro.inr
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h7 : ∀ x y : ℝ, u (x + y) = u x * u y := by
  intro x y
  calc u (x + y) = 1 + C * f (x + y) := h6 (x + y)
       _         = 1 + C * (f x * u y  + f y) := by rw [hf x y]
       _         = u y + C * f x * u y := by rw [h6 y]; ring
       _         = u y * (1 + C * f x) := by ring
       _         = u y * u x := by rw [h6 x]
       _         = u x * u y := mul_comm (u y) (u x)
State after:
case intro.intro.intro.inr
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro.intro.intro.inr
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hum : StrictMono u ∨ StrictAnti u
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
exact exp_characterization u h7 h00 hum
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
⊢ ∀ (x : ℝ), f x = f x * u 0 + f 0
Tactic:
intro x
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
x : ℝ
⊢ f x = f x * u 0 + f 0

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
x : ℝ
⊢ f x = f x * u 0 + f 0
Tactic:
have := hf x 0
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
x : ℝ
this : f (x + 0) = f x * u 0 + f 0
⊢ f x = f x * u 0 + f 0

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
x : ℝ
this : f (x + 0) = f x * u 0 + f 0
⊢ f x = f x * u 0 + f 0
Tactic:
rw [add_zero] at this
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
x : ℝ
this : f x = f x * u 0 + f 0
⊢ f x = f x * u 0 + f 0

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
x : ℝ
this : f x = f x * u 0 + f 0
⊢ f x = f x * u 0 + f 0
Tactic:
exact this
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
⊢ u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
Tactic:
intro hu0 x
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
⊢ f x = f 0 / (1 - u 0)

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
⊢ f x = f 0 / (1 - u 0)
Tactic:
have hy0x1 :=
            calc f 0 = f x - f x * u 0 := (sub_eq_of_eq_add' (hy0 x)).symm
            _ = f x * (1 - u 0) := by ring
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
⊢ f x = f 0 / (1 - u 0)

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
⊢ f x = f 0 / (1 - u 0)
Tactic:
rw[hy0x1]
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
⊢ f x = f x * (1 - u 0) / (1 - u 0)

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
⊢ f x = f x * (1 - u 0) / (1 - u 0)
Tactic:
have : 1 - u 0 ≠ 0 := sub_ne_zero.mpr hu0.symm
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
this : 1 - u 0 ≠ 0
⊢ f x = f x * (1 - u 0) / (1 - u 0)

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
this : 1 - u 0 ≠ 0
⊢ f x = f x * (1 - u 0) / (1 - u 0)
Tactic:
field_simp
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
⊢ f x - f x * u 0 = f x * (1 - u 0)
Tactic:
ring
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
⊢ u 0 ≠ 1 → False
Tactic:
intro hu0
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
⊢ False

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
⊢ False
Tactic:
have hu0' := h0 hu0
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
⊢ False

State before:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hm : StrictAnti f
⊢ False
Tactic:
have hu00 := hu0' 0
State after:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hm : StrictAnti f
hu00 : f 0 = f 0 / (1 - u 0)
⊢ False

State before:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hm : StrictAnti f
hu00 : f 0 = f 0 / (1 - u 0)
⊢ False
Tactic:
have hu01 := hu0' 1
State after:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hm : StrictAnti f
hu00 : f 0 = f 0 / (1 - u 0)
hu01 : f 1 = f 0 / (1 - u 0)
⊢ False

State before:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hm : StrictAnti f
hu00 : f 0 = f 0 / (1 - u 0)
hu01 : f 1 = f 0 / (1 - u 0)
⊢ False
Tactic:
have hm0 := @hm 0 1 (by norm_num)
State after:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hm : StrictAnti f
hu00 : f 0 = f 0 / (1 - u 0)
hu01 : f 1 = f 0 / (1 - u 0)
hm0 : f 1 < f 0
⊢ False

State before:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hm : StrictAnti f
hu00 : f 0 = f 0 / (1 - u 0)
hu01 : f 1 = f 0 / (1 - u 0)
hm0 : f 1 < f 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
hu0' : ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hm : StrictAnti f
hu00 : f 0 = f 0 / (1 - u 0)
hu01 : f 1 = f 0 / (1 - u 0)
⊢ 0 < 1
Tactic:
norm_num
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
⊢ f 0 = 0
Tactic:
have := hy0 0
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
this : f 0 = f 0 * 1 + f 0
⊢ f 0 = 0

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
this : f 0 = f 0 * 1 + f 0
⊢ f 0 = 0
Tactic:
linarith
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
⊢ ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
Tactic:
intro x hx
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
⊢ f x ≠ 0

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
⊢ f x ≠ 0
Tactic:
cases' hm with hm1 hm2
State after:
case inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
⊢ f x ≠ 0

case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
⊢ f x ≠ 0

State before:
case inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
⊢ f x ≠ 0
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy x 0
State after:
case inl.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h1 : x < 0
⊢ f x ≠ 0

case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h2 : x = 0
⊢ f x ≠ 0

case inl.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h3 : 0 < x
⊢ f x ≠ 0

State before:
case inl.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h1 : x < 0
⊢ f x ≠ 0
Tactic:
rw [←hf0]
State after:
case inl.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h1 : x < 0
⊢ f x ≠ f 0

State before:
case inl.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h1 : x < 0
⊢ f x ≠ f 0
Tactic:
exact ne_of_lt (hm1 h1)
State after:
no goals

State before:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h2 : x = 0
⊢ f x ≠ 0
Tactic:
exfalso
State after:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h2 : x = 0
⊢ False

State before:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h2 : x = 0
⊢ False
Tactic:
exact hx h2
State after:
no goals

State before:
case inl.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h3 : 0 < x
⊢ f x ≠ 0
Tactic:
rw [←hf0]
State after:
case inl.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h3 : 0 < x
⊢ f x ≠ f 0

State before:
case inl.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h3 : 0 < x
⊢ f x ≠ f 0
Tactic:
exact (ne_of_lt (hm1 h3)).symm
State after:
no goals

State before:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
⊢ f x ≠ 0
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy x 0
State after:
case inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
⊢ f x ≠ 0

case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h2 : x = 0
⊢ f x ≠ 0

case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
⊢ f x ≠ 0

State before:
case inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
⊢ f x ≠ 0
Tactic:
have := hm2 h1
State after:
case inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
this : f 0 < f x
⊢ f x ≠ 0

State before:
case inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
this : f 0 < f x
⊢ f x ≠ 0
Tactic:
rw [hf0] at this
State after:
case inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
this : 0 < f x
⊢ f x ≠ 0

State before:
case inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
this : 0 < f x
⊢ f x ≠ 0
Tactic:
exact (ne_of_lt this).symm
State after:
no goals

State before:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h2 : x = 0
⊢ f x ≠ 0
Tactic:
exfalso
State after:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h2 : x = 0
⊢ False

State before:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h2 : x = 0
⊢ False
Tactic:
exact hx h2
State after:
no goals

State before:
case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
⊢ f x ≠ 0
Tactic:
have := hm2 h3
State after:
case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
this : f x < f 0
⊢ f x ≠ 0

State before:
case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
this : f x < f 0
⊢ f x ≠ 0
Tactic:
rw [hf0] at this
State after:
case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
this : f x < 0
⊢ f x ≠ 0

State before:
case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
this : f x < 0
⊢ f x ≠ 0
Tactic:
exact (ne_of_lt this)
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
⊢ ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
Tactic:
intro x y
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
x y : ℝ
⊢ f x * u y + f y = f x + f y * u x

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
x y : ℝ
⊢ f x * u y + f y = f x + f y * u x
Tactic:
rw [←hf, add_comm]
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
x y : ℝ
⊢ f (y + x) = f x + f y * u x

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
x y : ℝ
⊢ f (y + x) = f x + f y * u x
Tactic:
linarith[hf y x]
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
⊢ ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
Tactic:
intro x y
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
x y : ℝ
⊢ f x * (u y - 1) = f y * (u x - 1)

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
x y : ℝ
⊢ f x * (u y - 1) = f y * (u x - 1)
Tactic:
linarith [h1 x y]
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
⊢ ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
Tactic:
intro x y hx hy
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / f y

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / f y
Tactic:
have hx1 := hfx0 x hx
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / f y

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / f y
Tactic:
have hy1 := hfx0 y hy
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
hy1 : f y ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / f y

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
hy1 : f y ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / f y
Tactic:
have := h2 x y
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
hy1 : f y ≠ 0
this : f x * (u y - 1) = f y * (u x - 1)
⊢ (u x - 1) / f x = (u y - 1) / f y

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
hy1 : f y ≠ 0
this : f x * (u y - 1) = f y * (u x - 1)
⊢ (u x - 1) / f x = (u y - 1) / f y
Tactic:
field_simp
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
hy1 : f y ≠ 0
this : f x * (u y - 1) = f y * (u x - 1)
⊢ (u x - 1) * f y = (u y - 1) * f x

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
hy1 : f y ≠ 0
this : f x * (u y - 1) = f y * (u x - 1)
⊢ (u x - 1) * f y = (u y - 1) * f x
Tactic:
linarith
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
⊢ ∃ C, ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
Tactic:
use (u 1 - 1) / f 1
State after:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
⊢ ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = (u 1 - 1) / f 1

State before:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
⊢ ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = (u 1 - 1) / f 1
Tactic:
intro x hx
State after:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
x : ℝ
hx : x ≠ 0
⊢ (u x - 1) / f x = (u 1 - 1) / f 1

State before:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
x : ℝ
hx : x ≠ 0
⊢ (u x - 1) / f x = (u 1 - 1) / f 1
Tactic:
exact h3 x 1 hx one_ne_zero
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
⊢ ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
Tactic:
intro x hx
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
x : ℝ
hx : x ≠ 0
⊢ u x = 1 + C * f x

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
x : ℝ
hx : x ≠ 0
⊢ u x = 1 + C * f x
Tactic:
have hc1 := hC x hx
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
x : ℝ
hx : x ≠ 0
hc1 : (u x - 1) / f x = C
⊢ u x = 1 + C * f x

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
x : ℝ
hx : x ≠ 0
hc1 : (u x - 1) / f x = C
⊢ u x = 1 + C * f x
Tactic:
have hx1 := hfx0 x hx
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
x : ℝ
hx : x ≠ 0
hc1 : (u x - 1) / f x = C
hx1 : f x ≠ 0
⊢ u x = 1 + C * f x

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
x : ℝ
hx : x ≠ 0
hc1 : (u x - 1) / f x = C
hx1 : f x ≠ 0
⊢ u x = 1 + C * f x
Tactic:
field_simp at hc1
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
x : ℝ
hx : x ≠ 0
hx1 : f x ≠ 0
hc1 : u x - 1 = C * f x
⊢ u x = 1 + C * f x

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
x : ℝ
hx : x ≠ 0
hx1 : f x ≠ 0
hc1 : u x - 1 = C * f x
⊢ u x = 1 + C * f x
Tactic:
linarith
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
⊢ ∀ (x : ℝ), u x = 1 + C * f x
Tactic:
intro x
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
x : ℝ
⊢ u x = 1 + C * f x

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
x : ℝ
⊢ u x = 1 + C * f x
Tactic:
rcases em (x = 0) with rfl | hnz
State after:
case inl
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
⊢ u 0 = 1 + C * f 0

case inr
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
x : ℝ
hnz : ¬x = 0
⊢ u x = 1 + C * f x

State before:
case inl
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
⊢ u 0 = 1 + C * f 0
Tactic:
rw [hf0, h00]
State after:
case inl
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
⊢ 1 = 1 + C * 0

State before:
case inl
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
⊢ 1 = 1 + C * 0
Tactic:
ring
State after:
no goals

State before:
case inr
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
x : ℝ
hnz : ¬x = 0
⊢ u x = 1 + C * f x
Tactic:
exact h5 x hnz
State after:
no goals

State before:
case intro.intro.intro.inl
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
use 0
State after:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
⊢ ∀ (x : ℝ), u x = (0 * x).exp

State before:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
⊢ ∀ (x : ℝ), u x = (0 * x).exp
Tactic:
intro x
State after:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
x : ℝ
⊢ u x = (0 * x).exp

State before:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
x : ℝ
⊢ u x = (0 * x).exp
Tactic:
rw [zero_mul, Real.exp_zero]
State after:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
x : ℝ
⊢ u x = 1

State before:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
x : ℝ
⊢ u x = 1
Tactic:
have := h6 x
State after:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
x : ℝ
this : u x = 1 + C * f x
⊢ u x = 1

State before:
case h
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCz : C = 0
x : ℝ
this : u x = 1 + C * f x
⊢ u x = 1
Tactic:
rwa [hCz, zero_mul, add_zero] at this
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
⊢ ∀ (x y : ℝ), u (x + y) = u x * u y
Tactic:
intro x y
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
x y : ℝ
⊢ u (x + y) = u x * u y

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
x y : ℝ
⊢ u (x + y) = u x * u y
Tactic:
calc u (x + y) = 1 + C * f (x + y) := h6 (x + y)
     _         = 1 + C * (f x * u y  + f y) := by rw [hf x y]
     _         = u y + C * f x * u y := by rw [h6 y]; ring
     _         = u y * (1 + C * f x) := by ring
     _         = u y * u x := by rw [h6 x]
     _         = u x * u y := mul_comm (u y) (u x)
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
x y : ℝ
⊢ 1 + C * f (x + y) = 1 + C * (f x * u y + f y)
Tactic:
rw [hf x y]
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
x y : ℝ
⊢ 1 + C * (f x * u y + f y) = u y + C * f x * u y
Tactic:
rw [h6 y]
State after:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
x y : ℝ
⊢ 1 + C * (f x * (1 + C * f y) + f y) = 1 + C * f y + C * f x * (1 + C * f y)

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
x y : ℝ
⊢ 1 + C * (f x * (1 + C * f y) + f y) = 1 + C * f y + C * f x * (1 + C * f y)
Tactic:
ring
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
x y : ℝ
⊢ u y + C * f x * u y = u y * (1 + C * f x)
Tactic:
ring
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
x y : ℝ
⊢ u y * (1 + C * f x) = u y * u x
Tactic:
rw [h6 x]
State after:
no goals

State before:
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
⊢ StrictMono u ∨ StrictAnti u
Tactic:
cases' hm with hm hm
State after:
case inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
⊢ StrictMono u ∨ StrictAnti u

case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
⊢ StrictMono u ∨ StrictAnti u

State before:
case inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
⊢ StrictMono u ∨ StrictAnti u
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy C 0
State after:
case inl.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h1 : C < 0
⊢ StrictMono u ∨ StrictAnti u

case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u

case inl.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h3 : 0 < C
⊢ StrictMono u ∨ StrictAnti u

State before:
case inl.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h1 : C < 0
⊢ StrictMono u ∨ StrictAnti u
Tactic:
right
State after:
case inl.inl.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h1 : C < 0
⊢ StrictAnti u

State before:
case inl.inl.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h1 : C < 0
⊢ StrictAnti u
Tactic:
intro x y hxy
State after:
case inl.inl.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h1 : C < 0
x y : ℝ
hxy : x < y
⊢ u y < u x

State before:
case inl.inl.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h1 : C < 0
x y : ℝ
hxy : x < y
⊢ u y < u x
Tactic:
nlinarith [hm hxy, h6 x, h6 y]
State after:
no goals

State before:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u
Tactic:
rw [h2] at hCnz
State after:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u

State before:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u
Tactic:
exfalso
State after:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ False

State before:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ False
Tactic:
apply hCnz
State after:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ 0 = 0

State before:
case inl.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

State before:
case inl.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h3 : 0 < C
⊢ StrictMono u ∨ StrictAnti u
Tactic:
left
State after:
case inl.inr.inr.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h3 : 0 < C
⊢ StrictMono u

State before:
case inl.inr.inr.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h3 : 0 < C
⊢ StrictMono u
Tactic:
intro x y hxy
State after:
case inl.inr.inr.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h3 : 0 < C
x y : ℝ
hxy : x < y
⊢ u x < u y

State before:
case inl.inr.inr.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h3 : 0 < C
x y : ℝ
hxy : x < y
⊢ u x < u y
Tactic:
nlinarith [hm hxy, h6 x, h6 y]
State after:
no goals

State before:
case inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
⊢ StrictMono u ∨ StrictAnti u
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy C 0
State after:
case inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h1 : C < 0
⊢ StrictMono u ∨ StrictAnti u

case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u

case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h3 : 0 < C
⊢ StrictMono u ∨ StrictAnti u

State before:
case inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h1 : C < 0
⊢ StrictMono u ∨ StrictAnti u
Tactic:
left
State after:
case inr.inl.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h1 : C < 0
⊢ StrictMono u

State before:
case inr.inl.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h1 : C < 0
⊢ StrictMono u
Tactic:
intro x y hxy
State after:
case inr.inl.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h1 : C < 0
x y : ℝ
hxy : x < y
⊢ u x < u y

State before:
case inr.inl.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1✝ : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h1 : C < 0
x y : ℝ
hxy : x < y
⊢ u x < u y
Tactic:
nlinarith [hm hxy, h6 x, h6 y]
State after:
no goals

State before:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u
Tactic:
rw [h2] at hCnz
State after:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u

State before:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u
Tactic:
exfalso
State after:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h2 : C = 0
⊢ False

State before:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h2 : C = 0
⊢ False
Tactic:
apply hCnz
State after:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h2 : C = 0
⊢ 0 = 0

State before:
case inr.inr.inl
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2✝ : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h2 : C = 0
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

State before:
case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h3 : 0 < C
⊢ StrictMono u ∨ StrictAnti u
Tactic:
right
State after:
case inr.inr.inr.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h3 : 0 < C
⊢ StrictAnti u

State before:
case inr.inr.inr.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h3 : 0 < C
⊢ StrictAnti u
Tactic:
intro x y hxy
State after:
case inr.inr.inr.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h3 : 0 < C
x y : ℝ
hxy : x < y
⊢ u y < u x

State before:
case inr.inr.inr.h
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3✝ : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
C : ℝ
hC : ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
h5 : ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
h6 : ∀ (x : ℝ), u x = 1 + C * f x
hCnz : ¬C = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictAnti f
h3 : 0 < C
x y : ℝ
hxy : x < y
⊢ u y < u x
Tactic:
nlinarith [hm hxy, h6 x, h6 y]
State after:
no goals