awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ∑ u ∈ Ico (r i n) n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1) ≥
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ∑ u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1)
have hbc : ∀ (u : ℕ) (hu : u ∈ Ico (r i n) n), c₂ * g (↑n : ℝ) ≤ g (↑u : ℝ)
Tactic: gcongr with u hu
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ c₂ * g (↑n : ℝ) ≤ g (↑u : ℝ)
have hu₁ : r i n ≤ u ∧ u < n
Tactic: rw [Finset.mem_Ico] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ c₂ * g (↑n : ℝ) ≤ g (↑u : ℝ)
have hu' : u ∈ Set.Icc (r i n) n
Tactic: have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by lia⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ c₂ * g (↑n : ℝ) ≤ g (↑u : ℝ)
have hbc : (↑u : ℝ) ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ)
Tactic: refine hn₂ u ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ LE.le (α := ℝ) (↑u : ℝ) (↑n : ℝ)
have norm_cast : u ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ c₁ * (↑n : ℝ) ≤ (↑u : ℝ) ∧ LE.le (α := ℝ) (↑u : ℝ) (↑n : ℝ)
have hbc : c₁ * (↑n : ℝ) ≤ (↑u : ℝ)
Tactic: refine ⟨?_, by norm_cast; lia⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ c₁ * (↑n : ℝ) ≤ (↑u : ℝ)
have calc : c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
Tactic: calc c₁ * n ≤ r i n := by exact hn₁ i
                  _ ≤ u := by exact_mod_cast hu'.1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
calc : c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
⊢ c₁ * (↑n : ℝ) ≤ (↑u : ℝ)
have calc₁ : LE.le (α := ℝ) (↑(r i n) : ℝ) (↑u : ℝ)
Tactic: calc c₁ * n ≤ r i n := by exact hn₁ i
                  _ ≤ u := by exact_mod_cast hu'.1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ∑ u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1) ≥
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      ∑ _u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)
have hbc : ∀ (u : ℕ) (hu : u ∈ Ico (r i n) n), 0 < HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1)
Tactic: gcongr with u hu
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
hbc : ∀ (u : ℕ) (hu : u ∈ Ico (r i n) n), 0 < HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ∑ u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1) ≥
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      ∑ _u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)
have hbc₁ : ∀ (u : ℕ) (hu : u ∈ Ico (r i n) n), u ≤ n
Tactic: gcongr with u hu
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ 0 < HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1)
have hu₁ : r i n ≤ u ∧ u < n
Tactic: rw [Finset.mem_Ico] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ 0 < HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1)
have this : 0 < u
Tactic: have := calc 0 < r i n := hrpos_i
                      _ ≤ u := hu.1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ u ≤ n
have hu₁ : r i n ≤ u ∧ u < n
Tactic: rw [Finset.mem_Ico] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      ∑ _u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) ≥
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * #(Ico (r i n) n) • (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))
have hbc : #(Ico (r i n) n) • (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) ≤
  ∑ _u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * #(Ico (r i n) n) • (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))
have rw : HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
    ((↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))) =
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
    (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))
Tactic: rw [nsmul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
rw :
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      ((↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * #(Ico (r i n) n) • (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))
have rw₁ : HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
    ((↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))) =
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
    ((↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)))
Tactic: rw [nsmul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))
have e_a : (↑(#(Ico (r i n) n)) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
⊢ (↑(#(Ico (r i n) n)) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
have e_a : (↑(n - r i n) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
Tactic: rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : 0 ≤ p a b + 1
e_a : (↑(n - r i n) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
⊢ (↑(#(Ico (r i n) n)) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
have e_a₁ : HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
Tactic: rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]