awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) ≠ 0
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
                        ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
                      ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
                    ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ *
                  ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
                Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) *
              (Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹ *
            ‖a + (↑n : 𝕂)‖⁻¹ *
          ‖b + (↑n : 𝕂)‖⁻¹ *
        ‖c + (↑n : 𝕂)‖ *
      ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖ =
    ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖
have a₂ : ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0
Tactic: repeat rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) ≠ 0
a₂ : ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
                        ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
                      ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
                    ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ *
                  ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
                Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) *
              (Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹ *
            ‖a + (↑n : 𝕂)‖⁻¹ *
          ‖b + (↑n : 𝕂)‖⁻¹ *
        ‖c + (↑n : 𝕂)‖ *
      ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖ =
    ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖
have a₃ : ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0
Tactic: repeat rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) ≠ 0
a₂ : ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0
a₃ : ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
                        ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
                      ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
                    ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ *
                  ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
                Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) *
              (Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹ *
            ‖a + (↑n : 𝕂)‖⁻¹ *
          ‖b + (↑n : 𝕂)‖⁻¹ *
        ‖c + (↑n : 𝕂)‖ *
      ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖ =
    ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖
have a₄ : ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0
Tactic: repeat rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) ≠ 0
have a₁ : Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
Tactic: rw [norm_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0
have a₁ : Polynomial.eval c (ascPochhammer 𝕂 n) ≠ 0
Tactic: rw [norm_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0
have a₁ : Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0
Tactic: rw [norm_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0
have a₁ : Polynomial.eval a (ascPochhammer 𝕂 n) ≠ 0
Tactic: rw [norm_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ Polynomial.eval c (ascPochhammer 𝕂 n) ≠ 0
have a₁ : ¬∃ k < n, (↑k : 𝕂) = -c
Tactic: apply (ascPochhammer_eval_eq_zero_iff n _).not.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ¬∃ k < n, (↑k : 𝕂) = -c
have a₁ : ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -c
Tactic: push Not
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0
have a₁ : ¬∃ k < n, (↑k : 𝕂) = -b
Tactic: apply (ascPochhammer_eval_eq_zero_iff n _).not.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ¬∃ k < n, (↑k : 𝕂) = -b
have a₁ : ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -b
Tactic: push Not
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ Polynomial.eval a (ascPochhammer 𝕂 n) ≠ 0
have a₁ : ¬∃ k < n, (↑k : 𝕂) = -a
Tactic: apply (ascPochhammer_eval_eq_zero_iff n _).not.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ¬∃ k < n, (↑k : 𝕂) = -a
have a₁ : ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -a
Tactic: push Not
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ (Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ *
          ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
        ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ /
      ((Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹ * ‖HAdd.hAdd (α := 𝕂) (↑n : 𝕂) 1‖⁻¹ *
            (‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖a + (↑n : 𝕂)‖) *
          (‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ * ‖b + (↑n : 𝕂)‖) *
        (‖c + (↑n : 𝕂)‖⁻¹ * ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹)) =
    ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖
have _ : (Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ *
        ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
      ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ /
    ((Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹ * ‖HAdd.hAdd (α := 𝕂) (↑n : 𝕂) 1‖⁻¹ *
          (‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖a + (↑n : 𝕂)‖) *
        (‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ * ‖b + (↑n : 𝕂)‖) *
      (‖c + (↑n : 𝕂)‖⁻¹ * ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹)) =
  ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
                      ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
                    ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
                  ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹⁻¹ *
                ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
              (Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹⁻¹ *
            (Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂))⁻¹ *
          ‖a + (↑n : 𝕂)‖⁻¹ *
        ‖b + (↑n : 𝕂)‖⁻¹ *
      ‖c + (↑n : 𝕂)‖⁻¹⁻¹ *
    ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖⁻¹⁻¹
Tactic: calc
    _ = ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
        ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
        ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹⁻¹ * ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
        ‖(n ! : 𝕂)‖⁻¹⁻¹ * ‖(n ! : 𝕂)‖⁻¹ * ‖a + n‖⁻¹ * ‖b + n‖⁻¹ * ‖c + n‖⁻¹⁻¹ *
        ‖1 + (n : 𝕂)‖⁻¹⁻¹ := by ring_nf
    _ = _ := by
      simp only [inv_inv]
      repeat rw [DivisionRing.mul_inv_cancel, one_mul]
      all_goals
        rw [norm_ne_zero_iff]
      any_goals
        apply (ascPochhammer_eval_eq_zero_iff n _).not.2
        push Not
        exact fun kn hkn ↦ by simp [habc kn hkn]
      exact cast_ne_zero.2 (factorial_ne_zero n)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c) = 1
have convert_5 : Tendsto (fun (n : ℕ) ↦ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖)
  atTop (𝓝 (↑1 : ℝ))
Tactic: convert! ofScalars_radius_eq_of_tendsto 𝔸 _ one_ne_zero ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂)) atTop (𝓝 1)
⊢ Tendsto (fun (n : ℕ) ↦ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖)
    atTop (𝓝 (↑1 : ℝ))
have simp_rw : Tendsto (fun (n : ℕ) ↦ ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖) atTop
  (𝓝 (↑1 : ℝ))
Tactic: simp_rw [ordinaryHypergeometricSeries_norm_div_succ_norm a b c _ (fun n _ ↦ habc n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂)) atTop (𝓝 1)
⊢ Tendsto (fun (n : ℕ) ↦ ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖) atTop
    (𝓝 (↑1 : ℝ))
have simp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖(a + (↑n : 𝕂))⁻¹ * (b + (↑n : 𝕂))⁻¹ * (c + (↑n : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖)
  atTop (𝓝 1)
Tactic: simp only [← norm_inv, ← norm_mul, NNReal.coe_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂)) atTop (𝓝 1)
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ‖(a + (↑n : 𝕂))⁻¹ * (b + (↑n : 𝕂))⁻¹ * (c + (↑n : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖) atTop (𝓝 1)
have h : 1 = Norm.norm.{u_1} (E := 𝕂) 1
Tactic: convert! Filter.Tendsto.norm this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ Tendsto (fun (n : ℕ) ↦ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖)
    atTop (𝓝 (↑1 : ℝ))
have convert_5 : Tendsto.{0, u_1} (β := 𝕂)
  (fun (k : ℕ) ↦ (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂)) atTop (𝓝 1)
Tactic: suffices Tendsto (fun k : ℕ ↦ (a + k)⁻¹ * (b + k)⁻¹ * (c + k) * ((1 : 𝕂) + k)) atTop (𝓝 1) by
    simp_rw [ordinaryHypergeometricSeries_norm_div_succ_norm a b c _ (fun n _ ↦ habc n)]
    simp only [← norm_inv, ← norm_mul, NNReal.coe_one]
    convert! Filter.Tendsto.norm this
    exact norm_one.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (hypothesis)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂)) atTop (𝓝 1)
have this : ∀ (k : ℕ),
  (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
    (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))
Tactic: have (k : ℕ) : (a + k)⁻¹ * (b + k)⁻¹ * (c + k) * ((1 : 𝕂) + k) =
        (c + k) / (a + k) * ((1 + k) / (b + k)) := by field
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  ∀ (k : ℕ),
    (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
      (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))
⊢ Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂)) atTop (𝓝 1)
have convert_5 : Tendsto.{0, u_1} (β := 𝕂)
  (fun (k : ℕ) ↦ (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))) atTop (𝓝 1)
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  ∀ (k : ℕ),
    (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
      (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))
⊢ Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))) atTop (𝓝 1)
have convert_5 : Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (c + (↑x : 𝕂)) / (a + (↑x : 𝕂))) atTop (𝓝 1)
Tactic: apply (mul_one (1 : 𝕂)) ▸ Filter.Tendsto.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  ∀ (k : ℕ),
    (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
      (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))
convert_5 : Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (c + (↑x : 𝕂)) / (a + (↑x : 𝕂))) atTop (𝓝 1)
⊢ Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))) atTop (𝓝 1)
have convert_5₁ : Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ HAdd.hAdd (α := 𝕂) 1 (↑x : 𝕂) / (b + (↑x : 𝕂))) atTop (𝓝 1)
Tactic: apply (mul_one (1 : 𝕂)) ▸ Filter.Tendsto.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  ∀ (k : ℕ),
    (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
      (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (c + (↑x : 𝕂)) / (a + (↑x : 𝕂))) atTop (𝓝 1)
have h : ∀ (x : ℕ), (↑x : 𝕂) = HMul.hMul (α := 𝕂) 1 (↑x : 𝕂)
Tactic: convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  ∀ (k : ℕ),
    (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
      (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))
h h₁ : ∀ (x : ℕ), (↑x : 𝕂) = HMul.hMul (α := 𝕂) 1 (↑x : 𝕂)
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (c + (↑x : 𝕂)) / (a + (↑x : 𝕂))) atTop (𝓝 1)
have h₂ : 1 = 1 / 1
Tactic: convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  ∀ (k : ℕ),
    (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
      (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ HAdd.hAdd (α := 𝕂) 1 (↑x : 𝕂) / (b + (↑x : 𝕂))) atTop (𝓝 1)
have h : ∀ (x : ℕ), (↑x : 𝕂) = HMul.hMul (α := 𝕂) 1 (↑x : 𝕂)
Tactic: convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
this :
  ∀ (k : ℕ),
    (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
      (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))
h h₁ : ∀ (x : ℕ), (↑x : 𝕂) = HMul.hMul (α := 𝕂) 1 (↑x : 𝕂)
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ HAdd.hAdd (α := 𝕂) 1 (↑x : 𝕂) / (b + (↑x : 𝕂))) atTop (𝓝 1)
have h₂ : 1 = 1 / 1
Tactic: convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
ih :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
a : ℝ
ha : a ∈ Set.Ioi (HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1)
b : ℝ
hb : b ∈ Set.Ioi (HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1)
hab : a ≤ b
⊢ LE.le (α := ℝ) (deriv (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a)
    (deriv (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b)
have succ : ∀ (ha : (↑n : ℝ) < a) ⦃b : ℝ⦄ (hb : (↑n : ℝ) < b) (hab : a ≤ b),
  LE.le (α := ℝ) (deriv (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a)
    (deriv (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b)
Tactic: rw [Set.mem_Ioi, Nat.cast_add_one, add_sub_cancel_right] at ha hb
Cleared hypotheses: ha, b, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
ih :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
a : ℝ
ha : (↑n : ℝ) < a
b : ℝ
hb : (↑n : ℝ) < b
hab : a ≤ b
⊢ LE.le (α := ℝ) (deriv (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a)
    (deriv (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b)
have succ : LE.le (α := ℝ) (∑ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, (a - (↑j : ℝ)))
  (∑ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, (b - (↑j : ℝ)))
Tactic: simp_rw [deriv_descPochhammer_eval_eq_sum_prod_range_erase]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
ih :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
a : ℝ
ha : (↑n : ℝ) < a
b : ℝ
hb : (↑n : ℝ) < b
hab : a ≤ b
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, (a - (↑j : ℝ)))
    (∑ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, (b - (↑j : ℝ)))
have succ : ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)), ∀ i_1 ∈ (Finset.range (n + 1)).erase i, 0 ≤ a - (↑i_1 : ℝ)
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (hypothesis)
Goal:
n : ℕ
ih :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
a : ℝ
ha : (↑n : ℝ) < a
b : ℝ
hb : (↑n : ℝ) < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ∈ (Finset.range (n + 1)).erase i
⊢ 0 ≤ a - (↑j : ℝ)
have hj₁ : j ≠ i ∧ j < n + 1
Tactic: rw [Finset.mem_erase, Finset.mem_range] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
ih :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
a : ℝ
ha : (↑n : ℝ) < a
b : ℝ
hb : (↑n : ℝ) < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ≠ i ∧ j < n + 1
⊢ 0 ≤ a - (↑j : ℝ)
have succ : (↑j : ℝ) ≤ a
Tactic: apply sub_nonneg_of_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
⊢ MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
have zero : MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ 0))
  (Set.Ioi (HSub.hSub (α := ℝ) (↑0 : ℝ) 1))
Tactic: induction n with
  | zero => simp [monotoneOn_const]
  | succ n ih =>
    intro a ha b hb hab
    rw [Set.mem_Ioi, Nat.cast_add_one, add_sub_cancel_right] at ha hb
    simp_rw [deriv_descPochhammer_eval_eq_sum_prod_range_erase]
    gcongr with i hi
    intro j hj
    rw [Finset.mem_erase, Finset.mem_range] at hj
    apply sub_nonneg_of_le
    exact ha.le.trans' (mod_cast Nat.le_pred_of_lt hj.2)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
zero :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ 0))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑0 : ℝ) 1))
⊢ MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
have succ : ∀ (n : ℕ)
  (ih :
    MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
      (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))),
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1)))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1))
Tactic: induction n with
  | zero => simp [monotoneOn_const]
  | succ n ih =>
    intro a ha b hb hab
    rw [Set.mem_Ioi, Nat.cast_add_one, add_sub_cancel_right] at ha hb
    simp_rw [deriv_descPochhammer_eval_eq_sum_prod_range_erase]
    gcongr with i hi
    intro j hj
    rw [Finset.mem_erase, Finset.mem_range] at hj
    apply sub_nonneg_of_le
    exact ha.le.trans' (mod_cast Nat.le_pred_of_lt hj.2)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
⊢ ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)
have inl : ∀ (h_eq : n = 0),
  ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)
Tactic: rcases n.eq_zero_or_pos with h_eq | _