internlm/Lean-Github huggingface dataset:
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 : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ StrictMono u ∨ StrictAnti u
Tactic:
exfalso
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
⊢ False
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 : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ False
Tactic:
apply 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
⊢ 0 = 0
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 : ¬0 = 0
h7 : ∀ (x y : ℝ), u (x + y) = u x * u y
hm : StrictMono f
h2 : C = 0
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
u : ℝ → ℝ
⊢ (∃ k, ∀ (x : ℝ), u x = (k * x).exp) → ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
rintro ⟨k, hk⟩
Proof state after:
case intro
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case intro
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
obtain rfl | hknz := eq_or_ne k 0
Proof state after:
case intro.inl
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y

case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case intro.inl
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
use id
Proof state after:
case h
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ (StrictMono id ∨ StrictAnti id) ∧ ∀ (x y : ℝ), id (x + y) = id x * u y + id y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case h
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ (StrictMono id ∨ StrictAnti id) ∧ ∀ (x y : ℝ), id (x + y) = id x * u y + id y
Tactic:
constructor
Proof state after:
case h.left
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ StrictMono id ∨ StrictAnti id

case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∀ (x y : ℝ), id (x + y) = id x * u y + id y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case h.left
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ StrictMono id ∨ StrictAnti id
Tactic:
left
Proof state after:
case h.left.h
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ StrictMono id
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case h.left.h
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ StrictMono id
Tactic:
exact strictMono_id
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∀ (x y : ℝ), id (x + y) = id x * u y + id y
Tactic:
intro x y
Proof state after:
case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
x y : ℝ
⊢ id (x + y) = id x * u y + id y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
x y : ℝ
⊢ id (x + y) = id x * u y + id y
Tactic:
rw [hk y, zero_mul, Real.exp_zero, mul_one, id_def, id_def, id_def]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
let f : ℝ → ℝ := λ x ↦ Real.exp (k * x) - 1
Proof state after:
case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
use f
Proof state after:
case h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
use hfm
Proof state after:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ ∀ (x y : ℝ), f (x + y) = f x * u y + f y