internlm/Lean-Github huggingface dataset:
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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
⊢ f x ≠ 0
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy x 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
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
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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h1 : x < 0
⊢ f x ≠ 0
Tactic:
rw [←hf0]
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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h1 : x < 0
⊢ f x ≠ f 0
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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h1 : x < 0
⊢ f x ≠ f 0
Tactic:
exact ne_of_lt (hm1 h1)
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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h2 : x = 0
⊢ f x ≠ 0
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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h2 : x = 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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h2 : x = 0
⊢ False
Tactic:
exact hx h2
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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h3 : 0 < x
⊢ f x ≠ 0
Tactic:
rw [←hf0]
Proof 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
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
x : ℝ
hx : x ≠ 0
hm1 : StrictMono f
h3 : 0 < x
⊢ f x ≠ f 0
Tactic:
exact (ne_of_lt (hm1 h3)).symm
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
⊢ f x ≠ 0
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy x 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
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
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
⊢ f x ≠ 0
Tactic:
have := hm2 h1
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
this : f 0 < f x
⊢ f x ≠ 0
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
this : f 0 < f x
⊢ f x ≠ 0
Tactic:
rw [hf0] at this
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
this : 0 < f x
⊢ f x ≠ 0
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h1 : x < 0
this : 0 < f x
⊢ f x ≠ 0
Tactic:
exact (ne_of_lt this).symm
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h2 : x = 0
⊢ f x ≠ 0
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h2 : x = 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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h2 : x = 0
⊢ False
Tactic:
exact hx h2
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
⊢ f x ≠ 0
Tactic:
have := hm2 h3
Proof 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
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
this : f x < f 0
⊢ f x ≠ 0
Tactic:
rw [hf0] at this
Proof 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
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
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
this : f x < 0
⊢ f x ≠ 0
Tactic:
exact (ne_of_lt 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
⊢ ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
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
x y : ℝ
⊢ f x * u y + f y = f x + f y * u x
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
x y : ℝ
⊢ f x * u y + f y = f x + f y * u x
Tactic:
rw [←hf, add_comm]
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
x y : ℝ
⊢ f (y + x) = f x + f y * u x
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
x y : ℝ
⊢ f (y + x) = f x + f y * u x
Tactic:
linarith[hf y 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
⊢ ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
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
x y : ℝ
⊢ f x * (u y - 1) = f y * (u x - 1)
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
x y : ℝ
⊢ f x * (u y - 1) = f y * (u x - 1)
Tactic:
linarith [h1 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)
⊢ ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
Tactic:
intro x y hx hy
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)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / 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)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / f y
Tactic:
have hx1 := hfx0 x hx
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)
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
hx1 : f x ≠ 0
⊢ (u x - 1) / f x = (u y - 1) / 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)
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
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)
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
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)
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
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)
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
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)
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
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)
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
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)
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
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, ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = C
Tactic:
use (u 1 - 1) / f 1
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
⊢ ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = (u 1 - 1) / f 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
⊢ ∀ (x : ℝ), x ≠ 0 → (u x - 1) / f x = (u 1 - 1) / f 1
Tactic:
intro x hx
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
x : ℝ
hx : x ≠ 0
⊢ (u x - 1) / f x = (u 1 - 1) / f 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
x : ℝ
hx : x ≠ 0
⊢ (u x - 1) / f x = (u 1 - 1) / f 1
Tactic:
exact h3 x 1 hx one_ne_zero
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
⊢ ∀ (x : ℝ), x ≠ 0 → u x = 1 + C * f x
Tactic:
intro x hx
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
x : ℝ
hx : x ≠ 0
⊢ u x = 1 + C * f x
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
x : ℝ
hx : x ≠ 0
⊢ u x = 1 + C * f x
Tactic:
have hc1 := hC x hx
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
x : ℝ
hx : x ≠ 0
hc1 : (u x - 1) / f x = C
⊢ u x = 1 + C * f x
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
x : ℝ
hx : x ≠ 0
hc1 : (u x - 1) / f x = C
⊢ u x = 1 + C * f x
Tactic:
have hx1 := hfx0 x hx
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
x : ℝ
hx : x ≠ 0
hc1 : (u x - 1) / f x = C
hx1 : f x ≠ 0
⊢ u x = 1 + C * f x
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
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
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
x : ℝ
hx : x ≠ 0
hx1 : f x ≠ 0
hc1 : u x - 1 = C * f x
⊢ u x = 1 + C * f x
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
x : ℝ
hx : x ≠ 0
hx1 : f x ≠ 0
hc1 : u x - 1 = C * f x
⊢ u x = 1 + C * f x
Tactic:
linarith
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
⊢ ∀ (x : ℝ), u x = 1 + C * f x
Tactic:
intro x
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
x : ℝ
⊢ u x = 1 + C * f x