awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : p a b + 1 < 0
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1) ≤ HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (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 (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 : p a b + 1 < 0
⊢ 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))
have 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)
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 : p a b + 1 < 0
⊢ 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))
have 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))
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 : 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))
⊢ 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))
have 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)))
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 : p a b + 1 < 0
⊢ 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))
have hbc : HPow.hPow (α := ℝ) (↑(r i n) : ℝ) (p a b + 1) ≤ (c₁ * (↑n : ℝ)) ^ (p a b + 1)
Tactic: gcongr n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / ?_)
-- 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 : p a b + 1 < 0
⊢ 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))
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 : p a b + 1 < 0
⊢ (↑(#(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 : p a b + 1 < 0
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)]
-- 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 : p a b + 1 < 0
⊢ 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))
have hbc : (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
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 : p a b + 1 < 0
⊢ 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)))
have 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)))
Tactic: rw [Real.mul_rpow (by positivity) (by positivity)]
-- 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 : p a b + 1 < 0
⊢ 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)
have 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)
Tactic: rw [← Real.rpow_add_one (by positivity) (p a b)]
-- 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 : p a b + 1 < 0
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) * (1 - c₃) * c₂ * g (↑n : ℝ) /
      c₁ ^ (p a b + 1) =
    (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g (↑n : ℝ)
have rw : (1 - c₃) * c₂ * g (↑n : ℝ) / c₁ ^ (p a b + 1) = (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g (↑n : ℝ)
Tactic: rw [div_self (by positivity), one_mul]
-- 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 : p a b + 1 < 0
⊢ (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g (↑n : ℝ) ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ)
have hbc : min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) ≤ (1 - c₃) * c₂ / c₁ ^ (p a b + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    Symbol.nonterminal r.input :: s = p ++ [Symbol.nonterminal r.input] ++ q ∧ r.output ++ s = p ++ r.output ++ q
have h : Symbol.nonterminal r.input :: s = HAppend.hAppend (α := List (Symbol T N)) [] [Symbol.nonterminal r.input] ++ s ∧
  r.output ++ s = [] ++ r.output ++ s
Tactic: use [], s
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
s₁ s₂ : List (Symbol T N)
hrs : r.Rewrites s₁ s₂
ih :
  ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    s₁ = p ++ [Symbol.nonterminal r.input] ++ q ∧ s₂ = p ++ r.output ++ q
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    x :: s₁ = p ++ [Symbol.nonterminal r.input] ++ q ∧ x :: s₂ = p ++ r.output ++ q
have cons : ∀ (p' q' : List (Symbol T N)),
  r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q') →
    ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
      x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = p ++ [Symbol.nonterminal r.input] ++ q ∧
        x :: (p' ++ r.output ++ q') = p ++ r.output ++ q
Tactic: rcases ih with ⟨p', q', rfl, rfl⟩
Cleared hypotheses: s₁, s₂, hrs, ih
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = p ++ [Symbol.nonterminal r.input] ++ q ∧
      x :: (p' ++ r.output ++ q') = p ++ r.output ++ q
have h : x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = x :: p' ++ [Symbol.nonterminal r.input] ++ q' ∧
  x :: (p' ++ r.output ++ q') = x :: p' ++ r.output ++ q'
Tactic: use x :: p', q'
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hr : r.Rewrites u v
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
have head : ∀ (s : List (Symbol T N)),
  ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    Symbol.nonterminal r.input :: s = p ++ [Symbol.nonterminal r.input] ++ q ∧ r.output ++ s = p ++ r.output ++ q
Tactic: induction hr with
  | head s =>
    use [], s
    simp
  | cons x _ ih =>
    rcases ih with ⟨p', q', rfl, rfl⟩
    use x :: p', q'
    simp
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hr : r.Rewrites u v
head :
  ∀ (s : List (Symbol T N)),
    ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
      Symbol.nonterminal r.input :: s = p ++ [Symbol.nonterminal r.input] ++ q ∧ r.output ++ s = p ++ r.output ++ q
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
have cons : ∀ (x : Symbol T N) {s₁ s₂ : List (Symbol T N)},
  r.Rewrites s₁ s₂ →
    ∀
      (ih :
        ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
          s₁ = p ++ [Symbol.nonterminal r.input] ++ q ∧ s₂ = p ++ r.output ++ q),
      ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
        x :: s₁ = p ++ [Symbol.nonterminal r.input] ++ q ∧ x :: s₂ = p ++ r.output ++ q
Tactic: induction hr with
  | head s =>
    use [], s
    simp
  | cons x _ ih =>
    rcases ih with ⟨p', q', rfl, rfl⟩
    use x :: p', q'
    simp
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)
have nil : r.Rewrites (HAppend.hAppend (α := List (Symbol T N)) [] [Symbol.nonterminal r.input] ++ q) ([] ++ r.output ++ q)
Tactic: induction p with
  | nil => exact Rewrites.head q
  | cons d l ih => exact Rewrites.cons d ih
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
nil : r.Rewrites (HAppend.hAppend (α := List (Symbol T N)) [] [Symbol.nonterminal r.input] ++ q) ([] ++ r.output ++ q)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)
have cons : ∀ (d : Symbol T N) (l : List (Symbol T N))
  (ih : r.Rewrites (l ++ [Symbol.nonterminal r.input] ++ q) (l ++ r.output ++ q)),
  r.Rewrites (d :: l ++ [Symbol.nonterminal r.input] ++ q) (d :: l ++ r.output ++ q)
Tactic: induction p with
  | nil => exact Rewrites.head q
  | cons d l ih => exact Rewrites.cons d ih
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : r.Rewrites u v
p : List (Symbol T N)
⊢ r.Rewrites (p ++ u) (p ++ v)
have rw : ∀
  (hvw :
    ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
      u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q)
  (p : List (Symbol T N)),
  ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
    p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q
Tactic: rw [rewrites_iff] at *
Cleared hypotheses: hvw, p
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw :
  ∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
    p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q
have rcases : ∀ (x y : List (Symbol T N)) (hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y),
  ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
    p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q
Tactic: rcases hvw with ⟨x, y, hxy⟩
Cleared hypotheses: hvw