internlm/Lean-Github huggingface dataset:
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h.e'_3.h.e'_6
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
apply intervalIntegral.integral_congr_ae
Proof state after:
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
have : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume, x ≠ b := by
  convert Countable.ae_not_mem (s := {b}) (by simp) (μ := MeasureTheory.volume) using 1
Proof state after:
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
filter_upwards [this]
Proof state after:
case h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ (a_1 : ℝ), a_1 ≠ b → a_1 ∈ Ι a b → (↑⌊a_1⌋ + 1 / 2 - ↑a_1) * deriv φ a_1 = (↑k + 1 / 2 - ↑a_1) * deriv φ a_1
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ (a_1 : ℝ), a_1 ≠ b → a_1 ∈ Ι a b → (↑⌊a_1⌋ + 1 / 2 - ↑a_1) * deriv φ a_1 = (↑k + 1 / 2 - ↑a_1) * deriv φ a_1
Tactic:
intro x x_ne_b hx
Proof state after:
case h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : x ∈ Ι a b
⊢ (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : x ∈ Ι a b
⊢ (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
rw [uIoc_of_le ha.2.le, mem_Ioc] at hx
Proof state after:
case h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
congr
Proof state after:
case h.e_a.e_a.e_a.e_a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ ⌊x⌋ = k
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h.e_a.e_a.e_a.e_a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ ⌊x⌋ = k
Tactic:
exact Int.floor_eq_iff.mpr ⟨by linarith [ha.1], by have := Ne.lt_of_le x_ne_b hx.2; linarith⟩
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∀ᵐ (x : ℝ), x ≠ b
Tactic:
convert Countable.ae_not_mem (s := {b}) (by simp) (μ := MeasureTheory.volume) using 1
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ {b}.Countable
Tactic:
simp
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ ↑k ≤ x
Tactic:
linarith [ha.1]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ x < ↑k + 1
Tactic:
have := Ne.lt_of_le x_ne_b hx.2
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this✝ : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
this : x < b
⊢ x < ↑k + 1
Theorem: sum_eq_int_deriv_aux
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this✝ : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
this : x < b
⊢ x < ↑k + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_induction_aux_int
Proof state before:
case hz

⊢ ∀ (P : ℝ → ℝ → Prop),
    (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
      (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
        ∀ (a b : ℝ), a < b → ↑0 = ⌊b⌋ - ⌊a⌋ → P a b
Tactic:
intro P base _ a b hab hn
Proof state after:
case hz
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : ↑0 = ⌊b⌋ - ⌊a⌋
⊢ P a b
Theorem: interval_induction_aux_int
Proof state before:
case hz
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : ↑0 = ⌊b⌋ - ⌊a⌋
⊢ P a b
Tactic:
apply base a b ⌊a⌋ (Int.floor_le a) hab
Proof state after:
case hz
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : ↑0 = ⌊b⌋ - ⌊a⌋
⊢ b ≤ ↑⌊a⌋ + 1
Theorem: interval_induction_aux_int
Proof state before:
case hz
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : ↑0 = ⌊b⌋ - ⌊a⌋
⊢ b ≤ ↑⌊a⌋ + 1
Tactic:
rw [(by simp only [CharP.cast_eq_zero] at hn; linarith : ⌊a⌋ = ⌊b⌋)]
Proof state after:
case hz
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : ↑0 = ⌊b⌋ - ⌊a⌋
⊢ b ≤ ↑⌊b⌋ + 1
Theorem: interval_induction_aux_int
Proof state before:
case hz
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : ↑0 = ⌊b⌋ - ⌊a⌋
⊢ b ≤ ↑⌊b⌋ + 1
Tactic:
exact (Int.lt_floor_add_one b).le
Proof state after:
no goals
Theorem: interval_induction_aux_int
Proof state before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : ↑0 = ⌊b⌋ - ⌊a⌋
⊢ ⌊a⌋ = ⌊b⌋
Tactic:
simp only [CharP.cast_eq_zero] at hn
Proof state after:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : 0 = ⌊b⌋ - ⌊a⌋
⊢ ⌊a⌋ = ⌊b⌋
Theorem: interval_induction_aux_int
Proof state before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
x✝ : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
hab : a < b
hn : 0 = ⌊b⌋ - ⌊a⌋
⊢ ⌊a⌋ = ⌊b⌋
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_induction_aux_int
Proof state before:
case hi
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
⊢ ∀ (P : ℝ → ℝ → Prop),
    (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
      (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
        ∀ (a b : ℝ), a < b → ↑n.succ = ⌊b⌋ - ⌊a⌋ → P a b
Tactic:
intro P base step a b _ hn
Proof state after:
case hi
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
⊢ P a b
Theorem: interval_induction_aux_int
Proof state before:
case hi
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
⊢ P a b
Tactic:
have Pa : P a (⌊a⌋ + 1) :=
  base a (⌊a⌋ + 1) ⌊a⌋ (Int.floor_le a) (Int.lt_floor_add_one a) (le_of_eq rfl)
Proof state after:
case hi
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
⊢ P a b
Theorem: interval_induction_aux_int
Proof state before:
case hi
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
⊢ P a b
Tactic:
by_cases b_le_flaP1 : b = ⌊a⌋ + 1
Proof state after:
case pos
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : b = ↑⌊a⌋ + 1
⊢ P a b

case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
⊢ P a b
Theorem: interval_induction_aux_int
Proof state before:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
⊢ P a b
Tactic:
have flaP1_lt_b : ⌊a⌋ + 1 < b := by
  simp only [Nat.cast_succ] at hn
  have : (⌊a⌋ : ℝ) + 1 ≤ ⌊b⌋ := by exact_mod_cast (by linarith)
  exact Ne.lt_of_le (id (Ne.symm b_le_flaP1)) (by linarith [Int.floor_le b] : ⌊a⌋ + 1 ≤ b)
Proof state after:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
⊢ P a b
Theorem: interval_induction_aux_int
Proof state before:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
⊢ P a b
Tactic:
have Pfla_b : P (⌊a⌋ + 1) b := by
  apply ih n (le_of_eq rfl) P base step (⌊a⌋ + 1) b flaP1_lt_b
  simp only [Int.floor_add_one, Int.floor_intCast, Nat.cast_succ] at hn ⊢
  linarith
Proof state after:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
Pfla_b : P (↑⌊a⌋ + 1) b
⊢ P a b
Theorem: interval_induction_aux_int
Proof state before:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
Pfla_b : P (↑⌊a⌋ + 1) b
⊢ P a b
Tactic:
refine step a (⌊a⌋ + 1) b ?_ (by exact_mod_cast flaP1_lt_b) (by exact_mod_cast Pa)
  (by exact_mod_cast Pfla_b)
Proof state after:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
Pfla_b : P (↑⌊a⌋ + 1) b
⊢ a < ↑(⌊a⌋ + 1)
Theorem: interval_induction_aux_int
Proof state before:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
Pfla_b : P (↑⌊a⌋ + 1) b
⊢ a < ↑(⌊a⌋ + 1)
Tactic:
have := Int.lt_floor_add_one a
Proof state after:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
Pfla_b : P (↑⌊a⌋ + 1) b
this : a < ↑⌊a⌋ + 1
⊢ a < ↑(⌊a⌋ + 1)
Theorem: interval_induction_aux_int
Proof state before:
case neg
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
Pfla_b : P (↑⌊a⌋ + 1) b
this : a < ↑⌊a⌋ + 1
⊢ a < ↑(⌊a⌋ + 1)
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: interval_induction_aux_int
Proof state before:
case pos
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : b = ↑⌊a⌋ + 1
⊢ P a b
Tactic:
rwa [b_le_flaP1]
Proof state after:
no goals
Theorem: interval_induction_aux_int
Proof state before:
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
⊢ ↑⌊a⌋ + 1 < b
Tactic:
simp only [Nat.cast_succ] at hn
Proof state after:
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
hn : ↑n + 1 = ⌊b⌋ - ⌊a⌋
⊢ ↑⌊a⌋ + 1 < b
Theorem: interval_induction_aux_int
Proof state before:
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
hn : ↑n + 1 = ⌊b⌋ - ⌊a⌋
⊢ ↑⌊a⌋ + 1 < b
Tactic:
have : (⌊a⌋ : ℝ) + 1 ≤ ⌊b⌋ := by exact_mod_cast (by linarith)
Proof state after:
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
hn : ↑n + 1 = ⌊b⌋ - ⌊a⌋
this : ↑⌊a⌋ + 1 ≤ ↑⌊b⌋
⊢ ↑⌊a⌋ + 1 < b
Theorem: interval_induction_aux_int
Proof state before:
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
hn : ↑n + 1 = ⌊b⌋ - ⌊a⌋
this : ↑⌊a⌋ + 1 ≤ ↑⌊b⌋
⊢ ↑⌊a⌋ + 1 < b
Tactic:
exact Ne.lt_of_le (id (Ne.symm b_le_flaP1)) (by linarith [Int.floor_le b] : ⌊a⌋ + 1 ≤ b)
Proof state after:
no goals
Theorem: interval_induction_aux_int
Proof state before:
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
hn : ↑n + 1 = ⌊b⌋ - ⌊a⌋
⊢ ↑⌊a⌋ + 1 ≤ ↑⌊b⌋
Tactic:
exact_mod_cast (by linarith)
Proof state after:
no goals