internlm/Lean-Github huggingface dataset:
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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'
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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'
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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]
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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)
Proof 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
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
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
⊢ ∀ (x : ℝ), f x = f x * u 0 + f 0
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
x : ℝ
⊢ f x = f x * u 0 + f 0
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
x : ℝ
⊢ f x = f x * u 0 + f 0
Tactic:
have := hf x 0
Proof 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
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
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
Proof 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
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
x : ℝ
this : f x = f x * u 0 + f 0
⊢ f x = f x * u 0 + f 0
Tactic:
exact 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 * u 0 + f 0
⊢ u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
Tactic:
intro hu0 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 * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
⊢ f x = f 0 / (1 - u 0)
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 * 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
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 * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
⊢ f x = f 0 / (1 - u 0)
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 * 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]
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 * 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)
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 * 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
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 * 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)
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 * 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
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 * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
⊢ f x - f x * u 0 = f x * (1 - u 0)
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 * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
⊢ u 0 ≠ 1 → False
Tactic:
intro hu0
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 * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
hu0 : u 0 ≠ 1
⊢ False
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 * 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
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 * 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
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 * 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
Proof 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
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 * 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
Proof 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
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 * 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)
Proof 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
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 * 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
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof 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
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
⊢ f 0 = 0
Tactic:
have := hy0 0
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
this : f 0 = f 0 * 1 + f 0
⊢ f 0 = 0
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
this : f 0 = f 0 * 1 + f 0
⊢ f 0 = 0
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
⊢ ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
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
x : ℝ
hx : x ≠ 0
⊢ f x ≠ 0
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
x : ℝ
hx : x ≠ 0
⊢ f x ≠ 0
Tactic:
cases' hm with hm1 hm2
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
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