awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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)
simp_rw :
  Tendsto (fun (n : ℕ) ↦ ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖) atTop
    (𝓝 (↑1 : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖)
    atTop (𝓝 (↑1 : ℝ))

Tactic:
simp_rw [ordinaryHypergeometricSeries_norm_div_succ_norm a b c _ (fun n _ ↦ habc n)]

Premises used: ordinaryHypergeometricSeries_norm_div_succ_norm
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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)
simp :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ‖(a + (↑n : 𝕂))⁻¹ * (b + (↑n : 𝕂))⁻¹ * (c + (↑n : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖) atTop (𝓝 1)
⊢ 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]

Premises used: norm_mul, norm_inv, NNReal.coe_one
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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 (x : ℕ) ↦ ‖(a + (↑x : 𝕂))⁻¹ * (b + (↑x : 𝕂))⁻¹ * (c + (↑x : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑x : 𝕂)‖) atTop
    (𝓝 (Norm.norm.{u_1} (E := 𝕂) 1))

Tactic:
Filter.Tendsto.norm this

Premises used: Filter.Tendsto.norm
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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)
h : 1 = Norm.norm.{u_1} (E := 𝕂) 1
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ‖(a + (↑n : 𝕂))⁻¹ * (b + (↑n : 𝕂))⁻¹ * (c + (↑n : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖) atTop (𝓝 1)

Tactic:
convert! Filter.Tendsto.norm this

Premises used: Filter.Tendsto.norm
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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)
⊢ 1 = Norm.norm.{u_1} (E := 𝕂) 1

Tactic:
norm_one.symm

Premises used: NormOneClass.norm_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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)
⊢ 1 = Norm.norm.{u_1} (E := 𝕂) 1

Tactic:
exact norm_one.symm

Premises used: NormOneClass.norm_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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
convert_5 :
  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 : ℝ))

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
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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
k : ℕ
⊢ (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) =
    (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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
⊢ ∀ (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
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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 (k : ℕ) ↦ (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))) atTop (𝓝 1)
⊢ Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (a + (↑k : 𝕂))⁻¹ * (b + (↑k : 𝕂))⁻¹ * (c + (↑k : 𝕂)) * HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂)) atTop (𝓝 1)

Tactic:
simp_rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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)
convert_5₁ : Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ HAdd.hAdd (α := 𝕂) 1 (↑x : 𝕂) / (b + (↑x : 𝕂))) atTop (𝓝 1)
⊢ Tendsto.{0, u_1} (β := 𝕂)
    (fun (k : ℕ) ↦ (c + (↑k : 𝕂)) / (a + (↑k : 𝕂)) * (HAdd.hAdd (α := 𝕂) 1 (↑k : 𝕂) / (b + (↑k : 𝕂)))) atTop (𝓝 1)

Tactic:
apply (mul_one (1 : 𝕂)) ▸ Filter.Tendsto.mul
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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 (fun (k : ℕ) ↦ (c + HMul.hMul (α := 𝕂) 1 (↑k : 𝕂)) / (a + HMul.hMul (α := 𝕂) 1 (↑k : 𝕂))) atTop (𝓝 (1 / 1))

Tactic:
tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero

Premises used: tendsto_add_mul_div_add_mul_atTop_nhds, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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 : 𝕂)
h₂ : 1 = 1 / 1
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (c + (↑x : 𝕂)) / (a + (↑x : 𝕂))) atTop (𝓝 1)

Tactic:
convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero

Premises used: tendsto_add_mul_div_add_mul_atTop_nhds, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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 (fun (k : ℕ) ↦ (1 + HMul.hMul (α := 𝕂) 1 (↑k : 𝕂)) / (b + HMul.hMul (α := 𝕂) 1 (↑k : 𝕂))) atTop (𝓝 (1 / 1))

Tactic:
tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero

Premises used: tendsto_add_mul_div_add_mul_atTop_nhds, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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 : 𝕂)
h₂ : 1 = 1 / 1
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ HAdd.hAdd (α := 𝕂) 1 (↑x : 𝕂) / (b + (↑x : 𝕂))) atTop (𝓝 1)

Tactic:
convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero

Premises used: tendsto_add_mul_div_add_mul_atTop_nhds, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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 : 𝕂)))
x : ℕ
⊢ (↑x : 𝕂) = HMul.hMul (α := 𝕂) 1 (↑x : 𝕂)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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 : 𝕂)))
⊢ 1 = 1 / 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
⊢ Differentiable 𝕜 (F := 𝕜) fun (x : 𝕜) ↦ Polynomial.eval x (descPochhammer 𝕜 n)

Tactic:
simp [descPochhammer_eval_eq_prod_range, Differentiable.fun_finsetProd]

Premises used: descPochhammer_eval_eq_prod_range, Differentiable.fun_finsetProd
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
⊢ Continuous (Y := 𝕜) fun (x : 𝕜) ↦ Polynomial.eval x (descPochhammer 𝕜 n)

Tactic:
differentiable_descPochhammer_eval.continuous

Premises used: differentiable_descPochhammer_eval, Differentiable.continuous
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
⊢ Continuous (Y := 𝕜) fun (x : 𝕜) ↦ Polynomial.eval x (descPochhammer 𝕜 n)

Tactic:
exact differentiable_descPochhammer_eval.continuous

Premises used: differentiable_descPochhammer_eval, Differentiable.continuous
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
k : 𝕜
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ Polynomial.eval x (descPochhammer 𝕜 n)) k)
    (∑ i ∈ Finset.range n, ∏ j ∈ (Finset.range n).erase i, (k - (↑j : 𝕜)))

Tactic:
simp [descPochhammer_eval_eq_prod_range, deriv_fun_finsetProd]

Premises used: descPochhammer_eval_eq_prod_range, deriv_fun_finsetProd
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
⊢ MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ 0))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑0 : ℝ) 1))

Tactic:
simp [monotoneOn_const]

Premises used: monotoneOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
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
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)
⊢ 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

Premises used: Set.mem_Ioi, add_sub_cancel_right, Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
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
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 : ℝ)))
⊢ LE.le (α := ℝ) (deriv (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a)
    (deriv (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b)

Tactic:
simp_rw [deriv_descPochhammer_eval_eq_sum_prod_range_erase]

Premises used: deriv_descPochhammer_eval_eq_sum_prod_range_erase
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
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
succ : ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)), ∀ i_1 ∈ (Finset.range (n + 1)).erase i, 0 ≤ a - (↑i_1 : ℝ)
⊢ 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:
gcongr with i hi
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
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
⊢ j ≠ i ∧ j < n + 1

Tactic:
rw [Finset.mem_erase, Finset.mem_range] at hj

Premises used: Finset.mem_range, Finset.mem_erase
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
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
succ : (↑j : ℝ) ≤ a
⊢ 0 ≤ a - (↑j : ℝ)

Tactic:
apply sub_nonneg_of_le

Premises used: sub_nonneg_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
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
⊢ (↑j : ℝ) ≤ a

Tactic:
ha.le.trans' (mod_cast Nat.le_pred_of_lt hj.2)

Premises used: cast, LT.lt.le, Nat.cast_le._simp_1, Nat.le_pred_of_lt, And.right, Eq.symm, LE.le.trans'
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
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
⊢ (↑j : ℝ) ≤ a

Tactic:
exact ha.le.trans' (mod_cast Nat.le_pred_of_lt hj.2)

Premises used: LT.lt.le, LE.le.trans'
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
zero :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ 0))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑0 : ℝ) 1))
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))
⊢ MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 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)

Premises used: sub_nonneg_of_le, Set.mem_Ioi, Finset.mem_range, monotoneOn_const, Finset.mem_erase, deriv_descPochhammer_eval_eq_sum_prod_range_erase, add_sub_cancel_right, Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
inl :
  ∀ (h_eq : n = 0),
    ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)
inr :
  n > 0 →
    ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)
⊢ ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)

Tactic:
rcases n.eq_zero_or_pos with h_eq | _

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
h_eq : n = 0
⊢ ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)

Tactic:
simp [h_eq, convexOn_const, convex_Ici]

Premises used: convex_Ici, convexOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
h : n > 0
inr :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (interior (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)))
⊢ ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)

Tactic:
apply MonotoneOn.convexOn_of_deriv (convex_Ici (n - 1 : ℝ))
      continuous_descPochhammer_eval.continuousOn
      differentiable_descPochhammer_eval.differentiableOn

Premises used: Continuous.continuousOn, differentiable_descPochhammer_eval, MonotoneOn.convexOn_of_deriv, HSub.hSub, Nat.cast, convex_Ici, Differentiable.differentiableOn, continuous_descPochhammer_eval, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
h : n > 0
inr :
  MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
⊢ MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (interior (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)))

Tactic:
rw [interior_Ici]

Premises used: interior_Ici
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
h : n > 0
⊢ MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))

Tactic:
monotoneOn_deriv_descPochhammer_eval n

Premises used: monotoneOn_deriv_descPochhammer_eval
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
h : n > 0
⊢ MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))

Tactic:
exact monotoneOn_deriv_descPochhammer_eval n

Premises used: monotoneOn_deriv_descPochhammer_eval
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
k n : ℕ
rw : (↑k : ℝ) < HSub.hSub (α := ℝ) (↑n : ℝ) 1 → LT.lt (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ Eq (α := ℝ)
    ((Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (i : ℝ) ↦ ℝ)
        (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0 (↑k : ℝ) :
      ℝ)
    ((↑(k.descFactorial n) : ℝ) : ℝ)

Tactic:
rw [Set.piecewise, descPochhammer_eval_eq_descFactorial, ite_eq_left_iff, Set.mem_Ici, not_le,
    eq_comm, Pi.zero_apply, Nat.cast_eq_zero, Nat.descFactorial_eq_zero_iff_lt, ← @Nat.cast_lt ℝ]

Premises used: not_le, ite_eq_left_iff, Pi.zero_apply, eq_comm, descPochhammer_eval_eq_descFactorial, Nat.cast_eq_zero, Set.mem_Ici, Nat.descFactorial_eq_zero_iff_lt, Set.piecewise, Nat.cast_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
k n : ℕ
⊢ (↑k : ℝ) < HSub.hSub (α := ℝ) (↑n : ℝ) 1 → LT.lt (α := ℝ) (↑k : ℝ) (↑n : ℝ)

Tactic:
(sub_lt_self (n : ℝ) zero_lt_one).trans'

Premises used: sub_lt_self, Nat.cast, LT.lt.trans', zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
k n : ℕ
⊢ (↑k : ℝ) < HSub.hSub (α := ℝ) (↑n : ℝ) 1 → LT.lt (α := ℝ) (↑k : ℝ) (↑n : ℝ)

Tactic:
exact (sub_lt_self (n : ℝ) zero_lt_one).trans'

Premises used: sub_lt_self, Nat.cast, LT.lt.trans', zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
⊢ 0 < n

Tactic:
rw [← Nat.pos_iff_ne_zero] at hn

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : 0 < n
apply : Polynomial.eval (HSub.hSub (α := ℝ) (↑n : ℝ) 1) (descPochhammer ℝ n) = 0
⊢ ConvexOn ℝ (β := ℝ) Set.univ
    ((Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (a : ℝ) ↦ ℝ)
      (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0)

Tactic:
apply convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic
    (convexOn_descPochhammer_eval n) (convexOn_const 0 (convex_Iic (n - 1 : ℝ)))
    (monotoneOn_descPochhammer_eval n) antitoneOn_const

Premises used: convex_Iic, antitoneOn_const, monotoneOn_descPochhammer_eval, HSub.hSub, convexOn_descPochhammer_eval, Nat.cast, convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic, OfNat.ofNat, convexOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : 0 < n
⊢ Polynomial.eval (HSub.hSub (α := ℝ) (↑n : ℝ) 1) (descPochhammer ℝ n) = 0

Tactic:
simpa [← Nat.cast_pred hn] using descPochhammer_eval_coe_nat_of_lt (Nat.sub_one_lt_of_lt hn)

Premises used: Nat.sub_one_lt_of_lt, Nat.cast_pred, descPochhammer_eval_coe_nat_of_lt