internlm/Lean-Github huggingface dataset:
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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)
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof 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)
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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