internlm/Lean-Github huggingface dataset:
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:
linarith
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⌋
this : ↑⌊a⌋ + 1 ≤ ↑⌊b⌋
⊢ ↑⌊a⌋ + 1 ≤ b
Tactic:
linarith [Int.floor_le 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
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
⊢ P (↑⌊a⌋ + 1) b
Tactic:
apply ih n (le_of_eq rfl) P base step (⌊a⌋ + 1) b flaP1_lt_b
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
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
flaP1_lt_b : ↑⌊a⌋ + 1 < b
⊢ ↑n = ⌊b⌋ - ⌊↑⌊a⌋ + 1⌋
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
flaP1_lt_b : ↑⌊a⌋ + 1 < b
⊢ ↑n = ⌊b⌋ - ⌊↑⌊a⌋ + 1⌋
Tactic:
simp only [Int.floor_add_one, Int.floor_intCast, 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
flaP1_lt_b : ↑⌊a⌋ + 1 < b
hn : ↑n + 1 = ⌊b⌋ - ⌊a⌋
⊢ ↑n = ⌊b⌋ - (⌊a⌋ + 1)
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
flaP1_lt_b : ↑⌊a⌋ + 1 < b
hn : ↑n + 1 = ⌊b⌋ - ⌊a⌋
⊢ ↑n = ⌊b⌋ - (⌊a⌋ + 1)
Tactic:
linarith
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
flaP1_lt_b : ↑⌊a⌋ + 1 < b
Pfla_b : P (↑⌊a⌋ + 1) b
⊢ ↑(⌊a⌋ + 1) < b
Tactic:
exact_mod_cast flaP1_lt_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
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 ↑(⌊a⌋ + 1)
Tactic:
exact_mod_cast Pa
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
flaP1_lt_b : ↑⌊a⌋ + 1 < b
Pfla_b : P (↑⌊a⌋ + 1) b
⊢ P (↑(⌊a⌋ + 1)) b
Tactic:
exact_mod_cast Pfla_b
Proof state after:
no goals
Theorem: interval_induction
Proof state before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
⊢ P a b
Tactic:
set n := ⌊b⌋ - ⌊a⌋ with hn
Proof state after:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ := ⌊b⌋ - ⌊a⌋
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Theorem: interval_induction
Proof state before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ := ⌊b⌋ - ⌊a⌋
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Tactic:
clear_value n
Proof state after:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Theorem: interval_induction
Proof state before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Tactic:
have : 0 ≤ n := by simp only [hn, sub_nonneg, ge_iff_le, Int.floor_le_floor _ _ (hab.le)]
Proof state after:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
this : 0 ≤ n
⊢ P a b
Theorem: interval_induction
Proof state before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
this : 0 ≤ n
⊢ P a b
Tactic:
lift n to ℕ using this
Proof state after:
case intro
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℕ
hn : ↑n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Theorem: interval_induction
Proof state before:
case intro
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℕ
hn : ↑n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Tactic:
exact interval_induction_aux_int n P base step a b hab hn
Proof state after:
no goals
Theorem: interval_induction
Proof state before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
⊢ 0 ≤ n
Tactic:
simp only [hn, sub_nonneg, ge_iff_le, Int.floor_le_floor _ _ (hab.le)]
Proof state after:
no goals
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
⊢ Ioc a b = Ioc a c \ Ioc b c
Tactic:
ext x
Proof state after:
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ x ∈ Ioc a b ↔ x ∈ Ioc a c \ Ioc b c
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ x ∈ Ioc a b ↔ x ∈ Ioc a c \ Ioc b c
Tactic:
simp only [mem_Ioc, mem_sdiff, not_and, not_le]
Proof state after:
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b ↔ (a < x ∧ x ≤ c) ∧ (b < x → c < x)
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b ↔ (a < x ∧ x ≤ c) ∧ (b < x → c < x)
Tactic:
constructor
Proof state after:
case a.mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b → (a < x ∧ x ≤ c) ∧ (b < x → c < x)

case a.mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ (a < x ∧ x ≤ c) ∧ (b < x → c < x) → a < x ∧ x ≤ b
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
case a.mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b → (a < x ∧ x ≤ c) ∧ (b < x → c < x)
Tactic:
refine fun ⟨h₁, h₂⟩ ↦ ⟨⟨h₁, le_trans h₂ (mem_Icc.mp hb).2⟩, by contrapose! h₂; exact h₂.1⟩
Proof state after:
no goals
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : a < x ∧ x ≤ b
h₁ : a < x
h₂ : x ≤ b
⊢ b < x → c < x
Tactic:
contrapose! h₂
Proof state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : a < x ∧ x ≤ b
h₁ : a < x
h₂ : b < x ∧ x ≤ c
⊢ b < x
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : a < x ∧ x ≤ b
h₁ : a < x
h₂ : b < x ∧ x ≤ c
⊢ b < x
Tactic:
exact h₂.1
Proof state after:
no goals
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
case a.mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ (a < x ∧ x ≤ c) ∧ (b < x → c < x) → a < x ∧ x ≤ b
Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.1, by contrapose! h₂; exact ⟨h₂, h₁.2⟩⟩
Proof state after:
no goals
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : (a < x ∧ x ≤ c) ∧ (b < x → c < x)
h₁ : a < x ∧ x ≤ c
h₂ : b < x → c < x
⊢ x ≤ b
Tactic:
contrapose! h₂
Proof state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : (a < x ∧ x ≤ c) ∧ (b < x → c < x)
h₁ : a < x ∧ x ≤ c
h₂ : b < x
⊢ b < x ∧ x ≤ c
Theorem: Finset.Ioc_diff_Ioc
Proof state before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : (a < x ∧ x ≤ c) ∧ (b < x → c < x)
h₁ : a < x ∧ x ≤ c
h₂ : b < x
⊢ b < x ∧ x ≤ c
Tactic:
exact ⟨h₂, h₁.2⟩
Proof state after:
no goals
Theorem: Finset.sum_Ioc_add_sum_Ioc
Proof state before:
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ ∑ n ∈ Ioc a b, f n + ∑ n ∈ Ioc b c, f n = ∑ n ∈ Ioc a c, f n
Tactic:
convert Finset.sum_sdiff (s₁ := Finset.Ioc b c) (s₂ := Finset.Ioc a c) ?_
Proof state after:
case h.e'_2.h.e'_5.h
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ Ioc a b = Ioc a c \ Ioc b c

case convert_4
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ Ioc b c ⊆ Ioc a c
Theorem: Finset.sum_Ioc_add_sum_Ioc
Proof state before:
case h.e'_2.h.e'_5.h
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ Ioc a b = Ioc a c \ Ioc b c
Tactic:
exact Finset.Ioc_diff_Ioc hb
Proof state after:
no goals
Theorem: Finset.sum_Ioc_add_sum_Ioc
Proof state before:
case convert_4
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ Ioc b c ⊆ Ioc a c
Tactic:
exact Finset.Ioc_subset_Ioc (mem_Icc.mp hb).1 (by rfl)
Proof state after:
no goals
Theorem: Finset.sum_Ioc_add_sum_Ioc
Proof state before:
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ c ≤ c
Tactic:
rfl
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
a b : ℝ
⊢ ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict [[a, b]], ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Tactic:
apply (MeasureTheory.ae_restrict_iff' measurableSet_Icc).mpr
Proof state after:
a b : ℝ
⊢ ∀ᵐ (x : ℝ), x ∈ Icc (a ⊓ b) (a ⊔ b) → ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Theorem: integrability_aux₀
Proof state before:
a b : ℝ
⊢ ∀ᵐ (x : ℝ), x ∈ Icc (a ⊓ b) (a ⊔ b) → ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Tactic:
refine MeasureTheory.ae_of_all _ (fun x hx ↦ ?_)
Proof state after:
a b x : ℝ
hx : x ∈ Icc (a ⊓ b) (a ⊔ b)
⊢ ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx : x ∈ Icc (a ⊓ b) (a ⊔ b)
⊢ ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Tactic:
simp only [inf_le_iff, le_sup_iff, mem_Icc] at hx
Proof state after:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Tactic:
simp only [norm_int, Real.norm_eq_abs]
Proof state after:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1
Tactic:
cases' abs_cases x with hx hx
Proof state after:
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1

case inr
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ |x| ≤ max |a| |b|
Tactic:
cases' hx.1 with x_ge_a x_ge_b <;> cases' hx.2 with x_le_a x_le_b
Proof state after:
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|

case inl.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|

case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|

case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|
Theorem: integrability_aux₀
Proof state before:
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|
Tactic:
rw [(by linarith : x = a)]
Proof state after:
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |a| ≤ max |a| |b|
Theorem: integrability_aux₀
Proof state before:
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |a| ≤ max |a| |b|
Tactic:
apply le_max_left
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ x = a
Tactic:
linarith
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
case inl.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|
Tactic:
apply abs_le_max_abs_abs x_ge_a x_le_b
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|
Tactic:
rw [max_comm]
Proof state after:
case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |b| |a|
Theorem: integrability_aux₀
Proof state before:
case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |b| |a|
Tactic:
apply abs_le_max_abs_abs x_ge_b x_le_a
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|
Tactic:
rw [(by linarith : x = b)]
Proof state after:
case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |b| ≤ max |a| |b|
Theorem: integrability_aux₀
Proof state before:
case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |b| ≤ max |a| |b|
Tactic:
apply le_max_right
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ x = b
Tactic:
linarith
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1
Tactic:
rw [_root_.abs_of_nonneg <| by exact_mod_cast Int.floor_nonneg.mpr hx.2]
Proof state after:
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ ↑⌊x⌋ ≤ max |a| |b| + 1
Theorem: integrability_aux₀
Proof state before:
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ ↑⌊x⌋ ≤ max |a| |b| + 1
Tactic:
apply le_trans (Int.floor_le x) <| le_trans (hx.1 ▸ this) (by simp)
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ 0 ≤ ↑⌊x⌋
Tactic:
exact_mod_cast Int.floor_nonneg.mpr hx.2
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ max |a| |b| ≤ max |a| |b| + 1
Tactic:
simp
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
case inr
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1
Tactic:
rw [_root_.abs_of_nonpos <| by exact_mod_cast Int.floor_nonpos hx.2.le]
Proof state after:
case inr
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ -↑⌊x⌋ ≤ max |a| |b| + 1
Theorem: integrability_aux₀
Proof state before:
case inr
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ -↑⌊x⌋ ≤ max |a| |b| + 1
Tactic:
linarith [(Int.lt_floor_add_one x).le]
Proof state after:
no goals
Theorem: integrability_aux₀
Proof state before:
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ ↑⌊x⌋ ≤ 0
Tactic:
exact_mod_cast Int.floor_nonpos hx.2.le
Proof state after:
no goals
Theorem: integrability_aux₁
Proof state before:
a b : ℝ
⊢ IntervalIntegrable (fun x => ↑⌊x⌋) MeasureTheory.volume a b
Tactic:
rw [intervalIntegrable_iff']
Proof state after:
a b : ℝ
⊢ MeasureTheory.IntegrableOn (fun x => ↑⌊x⌋) [[a, b]] MeasureTheory.volume
Theorem: integrability_aux₁
Proof state before:
a b : ℝ
⊢ MeasureTheory.IntegrableOn (fun x => ↑⌊x⌋) [[a, b]] MeasureTheory.volume
Tactic:
apply MeasureTheory.Measure.integrableOn_of_bounded ?_ ?_ integrability_aux₀
Proof state after:
a b : ℝ
⊢ MeasureTheory.volume [[a, b]] ≠ ⊤

a b : ℝ
⊢ MeasureTheory.AEStronglyMeasurable (fun a => ↑⌊a⌋) MeasureTheory.volume
Theorem: integrability_aux₁
Proof state before:
a b : ℝ
⊢ MeasureTheory.volume [[a, b]] ≠ ⊤
Tactic:
simp only [Real.volume_interval, ne_eq, ENNReal.ofReal_ne_top, not_false_eq_true]
Proof state after:
no goals
Theorem: integrability_aux₁
Proof state before:
a b : ℝ
⊢ MeasureTheory.AEStronglyMeasurable (fun a => ↑⌊a⌋) MeasureTheory.volume
Tactic:
apply Measurable.aestronglyMeasurable
Proof state after:
case hf
a b : ℝ
⊢ Measurable fun a => ↑⌊a⌋
Theorem: integrability_aux₁
Proof state before:
case hf
a b : ℝ
⊢ Measurable fun a => ↑⌊a⌋
Tactic:
apply Measurable.comp (by exact fun ⦃t⦄ _ ↦ trivial) Int.measurable_floor
Proof state after:
no goals
Theorem: integrability_aux₁
Proof state before:
a b : ℝ
⊢ Measurable IntCast.intCast
Tactic:
exact fun ⦃t⦄ _ ↦ trivial
Proof state after:
no goals
Theorem: integrability_aux₂
Proof state before:
a b : ℝ
⊢ Continuous fun x => 1 / 2 - ↑x
Tactic:
continuity
Proof state after:
no goals
Theorem: integrability_aux
Proof state before:
a b : ℝ
⊢ IntervalIntegrable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) MeasureTheory.volume a b
Tactic:
convert integrability_aux₁.add integrability_aux₂ using 2
Proof state after:
case h.e'_3.h
a b x✝ : ℝ
⊢ ↑⌊x✝⌋ + 1 / 2 - ↑x✝ = ↑⌊x✝⌋ + (1 / 2 - ↑x✝)
Theorem: integrability_aux
Proof state before:
case h.e'_3.h
a b x✝ : ℝ
⊢ ↑⌊x✝⌋ + 1 / 2 - ↑x✝ = ↑⌊x✝⌋ + (1 / 2 - ↑x✝)
Tactic:
ring
Proof state after:
no goals
Theorem: uIcc_subsets
Proof state before:
a b c : ℝ
hc : c ∈ Icc a b
⊢ [[a, c]] ⊆ [[a, b]] ∧ [[c, b]] ⊆ [[a, b]]
Tactic:
constructor <;> rw [uIcc_of_le ?_, uIcc_of_le ?_]
Proof state after:
case left
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc a c ⊆ Icc a b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc c b ⊆ Icc a b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b
Theorem: uIcc_subsets
Proof state before:
case left
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc a c ⊆ Icc a b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc c b ⊆ Icc a b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b
Tactic:
any_goals apply Icc_subset_Icc
Proof state after:
case left.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ a

case left.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ b ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b
Theorem: uIcc_subsets
Proof state before:
case left.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ a

case left.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ b ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b
Tactic:
all_goals linarith [hc.1, hc.2]
Proof state after:
no goals
Theorem: uIcc_subsets
Proof state before:
case right
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc c b ⊆ Icc a b
Tactic:
apply Icc_subset_Icc
Proof state after:
case right.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ b ≤ b