Theorem: interval_induction_aux_int (PrimeNumberTheoremAnd/ZetaBounds.lean)

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
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

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
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

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⌋)]
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

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
State after:
no goals

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
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⌋

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
State after:
no goals

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
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

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)
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

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
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

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)
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

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
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

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)
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)

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
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)

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
State after:
no goals

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]
State after:
no goals

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
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

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)
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

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)
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
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⌋

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 ⊢
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals