internlm/Lean-Github huggingface dataset:
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ
Tactic:
refine ⟨z, hz2, ?_⟩
Proof state after:
case intro.intro
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ dist (↑z) y < δ
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ dist (↑z) y < δ
Tactic:
. rw [Real.dist_eq, abs_sub_comm, abs_of_pos (sub_pos.mpr hz2)]
  exact sub_lt_comm.mp hz1
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ dist (↑z) y < δ
Tactic:
rw [Real.dist_eq, abs_sub_comm, abs_of_pos (sub_pos.mpr hz2)]
Proof state after:
case intro.intro
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ y - ↑z < δ
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ y - ↑z < δ
Tactic:
exact sub_lt_comm.mp hz1
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_anti
Proof state before:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : dist (u ↑z) (f y) < ε
⊢ u ↑z < u y
Tactic:
have hufp : 0 < u y - f y := by linarith
Proof state after:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : dist (u ↑z) (f y) < ε
hufp : 0 < u y - f y
⊢ u ↑z < u y
Theorem: Romania1998P12.extend_function_anti
Proof state before:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : dist (u ↑z) (f y) < ε
hufp : 0 < u y - f y
⊢ u ↑z < u y
Tactic:
have hua : ε = u y - f y := abs_of_pos hufp
Proof state after:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : dist (u ↑z) (f y) < ε
hufp : 0 < u y - f y
hua : ε = u y - f y
⊢ u ↑z < u y
Theorem: Romania1998P12.extend_function_anti
Proof state before:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : dist (u ↑z) (f y) < ε
hufp : 0 < u y - f y
hua : ε = u y - f y
⊢ u ↑z < u y
Tactic:
rw [hua, Real.dist_eq] at hbzb
Proof state after:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
⊢ u ↑z < u y
Theorem: Romania1998P12.extend_function_anti
Proof state before:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
⊢ u ↑z < u y
Tactic:
obtain h5 | h6 := em (f y < u z)
Proof state after:
case inl
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h5 : f y < u ↑z
⊢ u ↑z < u y

case inr
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h6 : ¬f y < u ↑z
⊢ u ↑z < u y
Theorem: Romania1998P12.extend_function_anti
Proof state before:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : dist (u ↑z) (f y) < ε
⊢ 0 < u y - f y
Tactic:
linarith
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case inl
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h5 : f y < u ↑z
⊢ u ↑z < u y
Tactic:
have : 0 ≤ u z - f y := by linarith
Proof state after:
case inl
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h5 : f y < u ↑z
this : 0 ≤ u ↑z - f y
⊢ u ↑z < u y
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case inl
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h5 : f y < u ↑z
this : 0 ≤ u ↑z - f y
⊢ u ↑z < u y
Tactic:
rw[abs_eq_self.mpr this] at hbzb
Proof state after:
case inl
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : u ↑z - f y < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h5 : f y < u ↑z
this : 0 ≤ u ↑z - f y
⊢ u ↑z < u y
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case inl
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : u ↑z - f y < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h5 : f y < u ↑z
this : 0 ≤ u ↑z - f y
⊢ u ↑z < u y
Tactic:
linarith
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_anti
Proof state before:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h5 : f y < u ↑z
⊢ 0 ≤ u ↑z - f y
Tactic:
linarith
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case inr
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h6 : ¬f y < u ↑z
⊢ u ↑z < u y
Tactic:
have : u z - f y ≤ 0 := by linarith
Proof state after:
case inr
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h6 : ¬f y < u ↑z
this : u ↑z - f y ≤ 0
⊢ u ↑z < u y
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case inr
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h6 : ¬f y < u ↑z
this : u ↑z - f y ≤ 0
⊢ u ↑z < u y
Tactic:
rw[abs_eq_neg_self.mpr this] at hbzb
Proof state after:
case inr
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : -(u ↑z - f y) < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h6 : ¬f y < u ↑z
this : u ↑z - f y ≤ 0
⊢ u ↑z < u y
Theorem: Romania1998P12.extend_function_anti
Proof state before:
case inr
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : -(u ↑z - f y) < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h6 : ¬f y < u ↑z
this : u ↑z - f y ≤ 0
⊢ u ↑z < u y
Tactic:
linarith
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_anti
Proof state before:
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h6 : ¬f y < u ↑z
⊢ u ↑z - f y ≤ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Romania1998P12.int_dichotomy
Proof state before:
z : ℤ
⊢ ∃ n, ↑n = z ∨ -↑n = z
Tactic:
cases' z with z z
Proof state after:
case ofNat
z : ℕ
⊢ ∃ n, ↑n = Int.ofNat z ∨ -↑n = Int.ofNat z

case negSucc
z : ℕ
⊢ ∃ n, ↑n = Int.negSucc z ∨ -↑n = Int.negSucc z
Theorem: Romania1998P12.int_dichotomy
Proof state before:
case ofNat
z : ℕ
⊢ ∃ n, ↑n = Int.ofNat z ∨ -↑n = Int.ofNat z
Tactic:
use z
Proof state after:
case h
z : ℕ
⊢ ↑z = Int.ofNat z ∨ -↑z = Int.ofNat z
Theorem: Romania1998P12.int_dichotomy
Proof state before:
case h
z : ℕ
⊢ ↑z = Int.ofNat z ∨ -↑z = Int.ofNat z
Tactic:
left
Proof state after:
case h.h
z : ℕ
⊢ ↑z = Int.ofNat z
Theorem: Romania1998P12.int_dichotomy
Proof state before:
case h.h
z : ℕ
⊢ ↑z = Int.ofNat z
Tactic:
simp only [Int.ofNat_eq_coe]
Proof state after:
no goals
Theorem: Romania1998P12.int_dichotomy
Proof state before:
case negSucc
z : ℕ
⊢ ∃ n, ↑n = Int.negSucc z ∨ -↑n = Int.negSucc z
Tactic:
use z + 1
Proof state after:
case h
z : ℕ
⊢ ↑(z + 1) = Int.negSucc z ∨ -↑(z + 1) = Int.negSucc z
Theorem: Romania1998P12.int_dichotomy
Proof state before:
case h
z : ℕ
⊢ ↑(z + 1) = Int.negSucc z ∨ -↑(z + 1) = Int.negSucc z
Tactic:
right
Proof state after:
case h.h
z : ℕ
⊢ -↑(z + 1) = Int.negSucc z
Theorem: Romania1998P12.int_dichotomy
Proof state before:
case h.h
z : ℕ
⊢ -↑(z + 1) = Int.negSucc z
Tactic:
rfl
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof state before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h2 : ∀ x, (u x) * u (-x) = 1 := by
  intro x
  have := hu x (-x)
  rw [add_right_neg] at this
  rw [←this]
  exact hu0
Proof state after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.exp_characterization
Proof state before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h3 : ∀ x, u (-x) = 1 / (u x) :=
  fun x ↦ eq_one_div_of_mul_eq_one_right (h2 x)
Proof state after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.exp_characterization
Proof state before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
obtain ⟨k, hk⟩ : ∃ k, Real.exp k = u 1 := by
  use Real.log (u 1); exact Real.exp_log (hunz 1)
Proof state after:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.exp_characterization
Proof state before:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hnexp : ∀ n : ℕ, u n = Real.exp (k * n) := by
  intro n
  have h10 := h4 n 1
  rw [←hk, mul_one] at h10
  norm_cast at h10
  rw [h10, mul_comm]
  exact (Real.exp_nat_mul _ _).symm
Proof state after:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.exp_characterization
Proof state before:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hq : ∀ q : ℚ, u q = Real.exp (k * q) := fun q ↦ by
  rw [Rat.cast_def q, hp q.den q.pos q.num, hzexp q.num, ←Real.exp_mul]
  ring_nf
Proof state after:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.exp_characterization
Proof state before:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
use k
Proof state after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
⊢ ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.exp_characterization
Proof state before:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
let f := λ x ↦ Real.exp (k * x)
Proof state after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
f : ℝ → ℝ := fun x => (k * x).exp
⊢ ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.exp_characterization
Proof state before:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
f : ℝ → ℝ := fun x => (k * x).exp
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hf : ∀ q : ℚ, u q = f q := λ q ↦ hq q
Proof state after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
f : ℝ → ℝ := fun x => (k * x).exp
hf : ∀ (q : ℚ), u ↑q = f ↑q
⊢ ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.exp_characterization
Proof state before:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
f : ℝ → ℝ := fun x => (k * x).exp
hf : ∀ (q : ℚ), u ↑q = f ↑q
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hfm : Continuous f := by continuity
Proof state after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
f : ℝ → ℝ := fun x => (k * x).exp
hf : ∀ (q : ℚ), u ↑q = f ↑q
hfm : Continuous f
⊢ ∀ (x : ℝ), u x = (k * x).exp