internlm/Lean-Github huggingface dataset:
Theorem: Usa1985P1.nicomachus
Proof state before:
case zero
ih : ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2
h1 : (∑ x ∈ Finset.range 0, x + 0) ^ 2 = (∑ x ∈ Finset.range 0, x) ^ 2 + ((2 * ∑ x ∈ Finset.range 0, x) * 0 + 0 ^ 2)
h5 : 2 * ∑ x ∈ Finset.range 0, x = (∑ x ∈ Finset.range 0, x) * 2
⊢ 0 ^ 3 = 0 * (0 - 1) * 0 + 0 ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1985P1.nicomachus
Proof state before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
h1 :
  (∑ x ∈ Finset.range (n + 1), x + (n + 1)) ^ 2 =
    (∑ x ∈ Finset.range (n + 1), x) ^ 2 + ((2 * ∑ x ∈ Finset.range (n + 1), x) * (n + 1) + (n + 1) ^ 2)
h5 : 2 * ∑ x ∈ Finset.range (n + 1), x = (∑ x ∈ Finset.range (n + 1), x) * 2
⊢ (n + 1) ^ 3 = (n + 1) * (n + 1 - 1) * (n + 1) + (n + 1) ^ 2
Tactic:
simp only [Nat.succ_sub_succ_eq_sub, tsub_zero, Nat.succ_eq_add_one]
Proof state after:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
h1 :
  (∑ x ∈ Finset.range (n + 1), x + (n + 1)) ^ 2 =
    (∑ x ∈ Finset.range (n + 1), x) ^ 2 + ((2 * ∑ x ∈ Finset.range (n + 1), x) * (n + 1) + (n + 1) ^ 2)
h5 : 2 * ∑ x ∈ Finset.range (n + 1), x = (∑ x ∈ Finset.range (n + 1), x) * 2
⊢ (n + 1) ^ 3 = (n + 1) * n * (n + 1) + (n + 1) ^ 2
Theorem: Usa1985P1.nicomachus
Proof state before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
h1 :
  (∑ x ∈ Finset.range (n + 1), x + (n + 1)) ^ 2 =
    (∑ x ∈ Finset.range (n + 1), x) ^ 2 + ((2 * ∑ x ∈ Finset.range (n + 1), x) * (n + 1) + (n + 1) ^ 2)
h5 : 2 * ∑ x ∈ Finset.range (n + 1), x = (∑ x ∈ Finset.range (n + 1), x) * 2
⊢ (n + 1) ^ 3 = (n + 1) * n * (n + 1) + (n + 1) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Usa1985P1.nicomachus'
Proof state before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, (↑i + 1) ^ 3 = (∑ i ∈ Finset.range n, (↑i + 1)) ^ 2
Tactic:
norm_cast
Proof state after:
n : ℕ
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Theorem: Usa1985P1.nicomachus'
Proof state before:
n : ℕ
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Tactic:
have h1 := nicomachus (n + 1)
Proof state after:
n : ℕ
h1 : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Theorem: Usa1985P1.nicomachus'
Proof state before:
n : ℕ
h1 : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Tactic:
simp only [Finset.sum_range_succ', zero_pow, add_zero] at h1
Proof state after:
n : ℕ
h1 : ∑ k ∈ Finset.range n, (k + 1) ^ 3 + 0 ^ 3 = (∑ k ∈ Finset.range n, (k + 1)) ^ 2
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Theorem: Usa1985P1.nicomachus'
Proof state before:
n : ℕ
h1 : ∑ k ∈ Finset.range n, (k + 1) ^ 3 + 0 ^ 3 = (∑ k ∈ Finset.range n, (k + 1)) ^ 2
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Tactic:
exact h1
Proof state after:
no goals
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p ≠ 2
hp3 : p ≠ 3
⊢ ↑p ∣ a (p - 2)
Tactic:
rw [Ne, ← Nat.prime_dvd_prime_iff_eq hp (by decide), ← Nat.Prime.coprime_iff_not_dvd hp]
  at hp2 hp3
Proof state after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
⊢ ↑p ∣ a (p - 2)
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
⊢ ↑p ∣ a (p - 2)
Tactic:
have : Int.gcd p 6 = 1 := Nat.coprime_mul_iff_right.2 ⟨hp2, hp3⟩
Proof state after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
⊢ ↑p ∣ a (p - 2)
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
⊢ ↑p ∣ a (p - 2)
Tactic:
have hp' : p - 1 = p - 2 + 1 := Eq.symm <| Nat.succ_pred <| (tsub_pos_of_lt hp.one_lt).ne'
Proof state after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ ↑p ∣ a (p - 2)
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ ↑p ∣ a (p - 2)
Tactic:
rw [← Int.modEq_zero_iff_dvd, ← Int.ediv_one p, ← Nat.cast_one, ← this]
Proof state after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ a (p - 2) ≡ 0 [ZMOD ↑p / ↑((↑p).gcd 6)]
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ a (p - 2) ≡ 0 [ZMOD ↑p / ↑((↑p).gcd 6)]
Tactic:
refine Int.ModEq.cancel_left_div_gcd (Nat.cast_pos.2 hp.pos) ?_
Proof state after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * a (p - 2) ≡ 6 * 0 [ZMOD ↑p]
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * a (p - 2) ≡ 6 * 0 [ZMOD ↑p]
Tactic:
calc
  6 * a (p - 2) = 3 * 2 ^ (p - 1) + 2 * 3 ^ (p - 1) + (2 * 3) ^ (p - 1) - 6 := by
    simp only [a, hp', pow_succ']; ring
  _ ≡ 3 * 1 + 2 * 1 + 1 - 6 [ZMOD p] := by
    gcongr <;> apply Int.ModEq.pow_card_sub_one_eq_one hp <;>
      rwa [Int.isCoprime_iff_gcd_eq_one, Int.gcd_comm]
  _ = 0 := rfl
Proof state after:
no goals
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : ¬p ∣ 2
hp3 : ¬p = 3
⊢ Nat.Prime 3
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * a (p - 2) = 3 * 2 ^ (p - 1) + 2 * 3 ^ (p - 1) + (2 * 3) ^ (p - 1) - 6
Tactic:
simp only [a, hp', pow_succ']
Proof state after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * (2 ^ (p - 2) + 3 ^ (p - 2) + 6 ^ (p - 2) - 1) =
    3 * (2 * 2 ^ (p - 2)) + 2 * (3 * 3 ^ (p - 2)) + 2 * 3 * (2 * 3) ^ (p - 2) - 6
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * (2 ^ (p - 2) + 3 ^ (p - 2) + 6 ^ (p - 2) - 1) =
    3 * (2 * 2 ^ (p - 2)) + 2 * (3 * 3 ^ (p - 2)) + 2 * 3 * (2 * 3) ^ (p - 2) - 6
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2005P4.find_specified_factor
Proof state before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 3 * 2 ^ (p - 1) + 2 * 3 ^ (p - 1) + (2 * 3) ^ (p - 1) - 6 ≡ 3 * 1 + 2 * 1 + 1 - 6 [ZMOD ↑p]
Tactic:
gcongr <;> apply Int.ModEq.pow_card_sub_one_eq_one hp <;>
  rwa [Int.isCoprime_iff_gcd_eq_one, Int.gcd_comm]
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
⊢ ∀ (x : ℝ), u x = f x
Tactic:
by_contra! hn
Proof state after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
hn : ∃ x, u x ≠ f x
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
hn : ∃ x, u x ≠ f x
⊢ False
Tactic:
obtain ⟨y, hy⟩ := hn
Proof state after:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
⊢ False
Tactic:
let ε : ℝ := |u y - f y|
Proof state after:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
⊢ False
Tactic:
have hε : 0 < ε := abs_sub_pos.mpr hy
Proof state after:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
⊢ False
Tactic:
obtain ⟨δ, hδ0, hδ⟩ := Metric.continuous_iff.mp f_cont y ε hε
Proof state after:
case intro.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
⊢ False
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy (u y) (f y)
Proof state after:
case intro.intro.intro.inl
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
⊢ False

case intro.intro.intro.inr.inl
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h2 : u y = f y
⊢ False

case intro.intro.intro.inr.inr
u f : ℝ → ℝ
u_mono : Monotone 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
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro.intro.inl
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
⊢ False
Tactic:
have : ∃ z : ℚ, (z:ℝ) < y ∧ dist (z:ℝ) y < δ := by
  have hyδ : y - δ < y := sub_lt_self y hδ0
  obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hyδ
  refine ⟨z, hz2, ?_⟩
  . rw [Real.dist_eq, abs_sub_comm, abs_of_pos (sub_pos.mpr hz2)]
    exact sub_lt_comm.mp hz1
Proof state after:
case intro.intro.intro.inl
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
this : ∃ z, ↑z < y ∧ dist (↑z) y < δ
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro.intro.inl
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
this : ∃ z, ↑z < y ∧ dist (↑z) y < δ
⊢ False
Tactic:
obtain ⟨z, h_z_lt_y, hyz⟩ := this
Proof state after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
⊢ False
Tactic:
have hbzb := hδ z hyz
Proof state after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (f ↑z) (f y) < ε
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (f ↑z) (f y) < ε
⊢ False
Tactic:
rw [←h z] at hbzb
Proof state after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
⊢ False
Tactic:
have h_y_le_z := le_of_lt  h_z_lt_y
Proof state after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
h_y_le_z : ↑z ≤ y
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
h_y_le_z : ↑z ≤ y
⊢ False
Tactic:
have := u_mono h_y_le_z
Proof state after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
h_y_le_z : ↑z ≤ y
this : u ↑z ≤ u y
⊢ False
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
h_y_le_z : ↑z ≤ y
this : u ↑z ≤ u y
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ
Tactic:
have hyδ : y - δ < y := sub_lt_self y hδ0
Proof state after:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
hyδ : y - δ < y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ
Theorem: Romania1998P12.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
hyδ : y - δ < y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ
Tactic:
obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hyδ
Proof state after:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f 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_mono : Monotone 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) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ dist (↑z) y < δ
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f 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_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f 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_mono : Monotone 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) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ y - ↑z < δ
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f 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_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ u y < u ↑z
Tactic:
have hufp : u y - f y < 0 := by linarith
Proof state after:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : u y - f y < 0
⊢ u y < u ↑z
Theorem: Romania1998P12.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : u y - f y < 0
⊢ u y < u ↑z
Tactic:
have hua : ε = -(u y - f y) := abs_of_neg hufp
Proof state after:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z
Theorem: Romania1998P12.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z
Tactic:
rw [hua, Real.dist_eq] at hbzb
Proof state after:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z
Theorem: Romania1998P12.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z
Tactic:
obtain h5 | h6 := em (f y < u z)
Proof state after:
case inl
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h5 : f y < u ↑z
⊢ u y < u ↑z

case inr
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
⊢ u y < u ↑z
Theorem: Romania1998P12.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ u y - f y < 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Romania1998P12.extend_function_mono
Proof state before:
case inl
u f : ℝ → ℝ
u_mono : Monotone 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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h5 : f y < u ↑z
⊢ u y < u ↑z
Tactic:
linarith
Proof state after:
no goals