awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1) ≤ HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)

Tactic:
exact rpow_le_rpow_of_nonpos (by positivity)
            (by exact_mod_cast hu.1) (le_of_lt hp)

Premises used: le_of_lt, Real.rpow_le_rpow_of_nonpos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
hbc :
  #(Ico (r i n) n) • (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)) ≤
    ∑ _u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      ∑ _u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1) ≥
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      #(Ico (r i n) n) • (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1))

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
x : ℕ
h : x ∈ Ico (r i n) n
⊢ c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1) ≤
    c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)

Tactic:
rfl
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ #(Ico (r i n) n) • (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)) ≤
    ∑ _u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)

Tactic:
exact Finset.card_nsmul_le_sum _ _ _ (fun x _ => by rfl)

Premises used: Finset.card_nsmul_le_sum
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
rw :
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      ((↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1))) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1))
rw₁ rw₂ :
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      ((↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1))) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      ((↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)))
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      #(Ico (r i n) n) • (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1))

Tactic:
rw [nsmul_eq_mul, mul_assoc]

Premises used: mul_assoc, nsmul_eq_mul
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
hbc : HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1) ≤ (c₁ * (↑n : ℝ)) ^ (p a b + 1)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1)) ≥
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / (c₁ * (↑n : ℝ)) ^ (p a b + 1))

Tactic:
gcongr n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / ?_)

Premises used: HMul.hMul, Finset.Ico, HDiv.hDiv, Nat.cast, AkraBazziRecurrence.p
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ 0 < c₁ * (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1) ≤ (c₁ * (↑n : ℝ)) ^ (p a b + 1)

Tactic:
exact rpow_le_rpow_of_nonpos (by positivity) (hn₁ i) (le_of_lt hp)

Premises used: le_of_lt, Real.rpow_le_rpow_of_nonpos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
e_a : (↑(#(Ico (r i n) n)) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) * (c₂ * g (↑n : ℝ) / (c₁ * (↑n : ℝ)) ^ (p a b + 1)) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) *
      (c₂ * g (↑n : ℝ) / (c₁ * (↑n : ℝ)) ^ (p a b + 1))

Tactic:
congr
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
e_a : (↑(n - r i n) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
e_a₁ e_a₂ : HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
⊢ (↑(#(Ico (r i n) n)) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)

Tactic:
rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]

Premises used: Nat.cast_sub, le_of_lt, Nat.card_Ico
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
hbc : (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) *
      (c₂ * g (↑n : ℝ) / (c₁ * (↑n : ℝ)) ^ (p a b + 1)) ≥
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ((↑n : ℝ) - c₃ * (↑n : ℝ)) * (c₂ * g (↑n : ℝ) / (c₁ * (↑n : ℝ)) ^ (p a b + 1))

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)

Tactic:
hn₃ i
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)

Tactic:
exact hn₃ i
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ((↑n : ℝ) - c₃ * (↑n : ℝ)) * (c₂ * g (↑n : ℝ) / (c₁ * (↑n : ℝ)) ^ (p a b + 1)) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑n : ℝ) * (1 - c₃) * (c₂ * g (↑n : ℝ) / (c₁ * (↑n : ℝ)) ^ (p a b + 1))

Tactic:
ring
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ 0 ≤ c₁

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
rw rw₁ :
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑n : ℝ) * (1 - c₃) *
      (c₂ * g (↑n : ℝ) / (c₁ ^ (p a b + 1) * HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑n : ℝ) * (1 - c₃) *
      (c₂ * g (↑n : ℝ) / (c₁ ^ (p a b + 1) * HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)))
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑n : ℝ) * (1 - c₃) * (c₂ * g (↑n : ℝ) / (c₁ * (↑n : ℝ)) ^ (p a b + 1)) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑n : ℝ) * (1 - c₃) *
      (c₂ * g (↑n : ℝ) / (c₁ ^ (p a b + 1) * HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)))

Tactic:
rw [Real.mul_rpow (by positivity) (by positivity)]

Premises used: Real.mul_rpow
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
rw :
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) * (1 - c₃) *
      (c₂ * g (↑n : ℝ) / (c₁ ^ (p a b + 1) * HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) * (1 - c₃) * c₂ * g (↑n : ℝ) /
      c₁ ^ (p a b + 1)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑n : ℝ) * (1 - c₃) *
      (c₂ * g (↑n : ℝ) / (c₁ ^ (p a b + 1) * HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) * (1 - c₃) * c₂ * g (↑n : ℝ) /
      c₁ ^ (p a b + 1)

Tactic:
rw [← Real.rpow_add_one (by positivity) (p a b)]

Premises used: Real.rpow_add_one, AkraBazziRecurrence.p
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : p a b + 1 < 0
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) * (1 - c₃) *
      (c₂ * g (↑n : ℝ) / (c₁ ^ (p a b + 1) * HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) * (1 - c₃) * c₂ * g (↑n : ℝ) /
      c₁ ^ (p a b + 1)

Tactic:
ring