-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma base_nonempty {n : ℕ} (hn : 0 < n) : (Finset.Ico (⌊b (min_bi b) / 2 * n⌋₊) n).Nonempty

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
⊢ (Ico ⌊b (min_bi b) / 2 * ↑n⌋₊ n).Nonempty

Tactic:
have hb_pos : 0 < b' := R.b_pos _

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ (Ico ⌊b (min_bi b) / 2 * ↑n⌋₊ n).Nonempty

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ 1 * ↑n = ↑n

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ 1 / 2 ≤ 1

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ (Ico ⌊b (min_bi b) / 2 * ↑n⌋₊ n).Nonempty

Tactic:
simp_rw [Finset.nonempty_Ico]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ ⌊b (min_bi b) / 2 * ↑n⌋₊ < n

Proof state:
case bc.h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ b' < 1

Tactic:
exact R.b_lt_one (min_bi b)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ (Ico ⌊b (min_bi b) / 2 * ↑n⌋₊ n).Nonempty

Tactic:
let b' := b (min_bi b)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
⊢ (Ico ⌊b (min_bi b) / 2 * ↑n⌋₊ n).Nonempty

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ 0 ≤ b' / 2 * ↑n

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ 1 / 2 * ↑n ≤ 1 * ↑n

Tactic:
gcongr

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ 1 / 2 ≤ 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ b' / 2 * ↑n < 1 / 2 * ↑n

Tactic:
gcongr

Result:
case bc.h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ b' < 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ ↑⌊b' / 2 * ↑n⌋₊ ≤ b' / 2 * ↑n

Tactic:
exact Nat.floor_le (by positivity)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
b' : ℝ := b (min_bi b)
hb_pos : 0 < b'
⊢ ⌊b (min_bi b) / 2 * ↑n⌋₊ < n

Tactic:
exact_mod_cast calc ⌊b' / 2 * n⌋₊ ≤ b' / 2 * n := by exact Nat.floor_le (by positivity)
                               _ < 1 / 2 * n   := by gcongr; exact R.b_lt_one (min_bi b)
                               _ ≤ 1 * n       := by gcongr; norm_num
                               _ = n           := by simp

Result:
no goals