awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log x‖) atTop atTop

Tactic:
have B : Tendsto (fun x => ‖Real.log x‖) atTop atTop :=
    tendsto_norm_atTop_atTop.comp Real.tendsto_log_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x
B : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log x‖) atTop atTop
⊢ ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ici a) volume

Tactic:
not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter atTop (Ici_mem_atTop a)
    (A.mono (fun x hx ↦ hx.differentiableAt)) B
    (Filter.EventuallyEq.isBigO (A.mono (fun x hx ↦ hx.deriv)))

Premises used: Filter.EventuallyEq.isBigO, HasDerivAt.differentiableAt, HasDerivAt.deriv, Filter.Eventually.mono, Filter.atTop, not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter, Filter.Ici_mem_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x
B : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log x‖) atTop atTop
⊢ ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ici a) volume

Tactic:
exact not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter atTop (Ici_mem_atTop a)
    (A.mono (fun x hx ↦ hx.differentiableAt)) B
    (Filter.EventuallyEq.isBigO (A.mono (fun x hx ↦ hx.deriv)))

Premises used: Filter.EventuallyEq.isBigO, HasDerivAt.differentiableAt, HasDerivAt.deriv, Filter.Eventually.mono, Filter.atTop, not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter, Filter.Ici_mem_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a : ℝ
⊢ ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioi a) volume

Tactic:
simpa only [IntegrableOn, restrict_Ioi_eq_restrict_Ici] using not_integrableOn_Ici_inv

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.restrict_Ioi_eq_restrict_Ici, not_integrableOn_Ici_inv
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
n : ℕ
rw :
  ((ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c) n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) =
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
rw₁ rw₂ :
  ordinaryHypergeometricCoefficient a b c n • x ^ n =
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) =
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_apply_eq]

Premises used: FormalMultilinearSeries.ofScalars_apply_eq, ordinaryHypergeometricSeries
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
rw :
  Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸)
    (fun (n : ℕ) ↦
      (ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c) n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
    fun (n : ℕ) ↦
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸) (fun (n : ℕ) ↦ ordinaryHypergeometricCoefficient a b c n • x ^ n) fun (n : ℕ) ↦
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
⊢ Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸)
    (fun (n : ℕ) ↦ (ordinaryHypergeometricSeries 𝔸 a b c n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
    fun (n : ℕ) ↦
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_apply_eq']

Premises used: FormalMultilinearSeries.ofScalars_apply_eq', ordinaryHypergeometricSeries
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
⊢ FormalMultilinearSeries.sum (ordinaryHypergeometricSeries 𝔸 a b c : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    ∑' (n : ℕ),
      ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
        x ^ n

Tactic:
tsum_congr fun n => ordinaryHypergeometricSeries_apply_eq a b c x n

Premises used: tsum_congr, ordinaryHypergeometricSeries_apply_eq, FormalMultilinearSeries.sum
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) (₂F₁ a b c) fun (x : 𝔸) ↦
    ∑' (n : ℕ),
      ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
        x ^ n

Tactic:
funext (ordinaryHypergeometric_sum_eq a b c)

Premises used: ordinaryHypergeometric_sum_eq, funext
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
rw :
  ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      HPow.hPow (α := 𝔸) 0 n =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n
⊢ Eq (α := 𝔸) ((ordinaryHypergeometricSeries 𝔸 a b c n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x : Fin n) ↦ 0 : 𝔸)
    (Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n : 𝔸)

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_apply_eq, ordinaryHypergeometricCoefficient]

Premises used: FormalMultilinearSeries.ofScalars_apply_eq, ordinaryHypergeometricCoefficient, ordinaryHypergeometricSeries
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
zero :
  ((↑0! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 0) * Polynomial.eval b (ascPochhammer 𝕂 0) *
        (Polynomial.eval c (ascPochhammer 𝕂 0))⁻¹) •
      HPow.hPow (α := 𝔸) (β := ℕ) 0 0 =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 0
succ :
  ∀ (n : ℕ),
    ((↑(n + 1)! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 (n + 1)) * Polynomial.eval b (ascPochhammer 𝕂 (n + 1)) *
          (Polynomial.eval c (ascPochhammer 𝕂 (n + 1)))⁻¹) •
        HPow.hPow (α := 𝔸) 0 (n + 1) =
      Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
⊢ ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      HPow.hPow (α := 𝔸) 0 n =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n

Tactic:
cases n
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ ((↑0! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 0) * Polynomial.eval b (ascPochhammer 𝕂 0) *
        (Polynomial.eval c (ascPochhammer 𝕂 0))⁻¹) •
      HPow.hPow (α := 𝔸) (β := ℕ) 0 0 =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((↑(n + 1)! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 (n + 1)) * Polynomial.eval b (ascPochhammer 𝕂 (n + 1)) *
        (Polynomial.eval c (ascPochhammer 𝕂 (n + 1)))⁻¹) •
      HPow.hPow (α := 𝔸) 0 (n + 1) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ Eq.{u_2 + 1} (α := 𝔸) (₂F₁ a b c 0) 1

Tactic:
simp [ordinaryHypergeometric_eq_tsum, ← ordinaryHypergeometricSeries_apply_eq,
    ordinaryHypergeometricSeries_apply_zero]

Premises used: ordinaryHypergeometricSeries_apply_zero, ordinaryHypergeometric_eq_tsum, ordinaryHypergeometricSeries_apply_eq
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
unfold :
  Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ofScalars 𝔸 fun (n : ℕ) ↦
        (↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹ :
      FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ofScalars 𝔸 fun (n : ℕ) ↦
        (↑n ! : 𝕂)⁻¹ * Polynomial.eval b (ascPochhammer 𝕂 n) * Polynomial.eval a (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹ :
      FormalMultilinearSeries 𝕂 𝔸 𝔸)
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ordinaryHypergeometricSeries 𝔸 b a c : FormalMultilinearSeries 𝕂 𝔸 𝔸)

Tactic:
unfold ordinaryHypergeometricSeries ordinaryHypergeometricCoefficient

Premises used: ordinaryHypergeometricCoefficient, ordinaryHypergeometricSeries
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ofScalars 𝔸 fun (n : ℕ) ↦
        (↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹ :
      FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ofScalars 𝔸 fun (n : ℕ) ↦
        (↑n ! : 𝕂)⁻¹ * Polynomial.eval b (ascPochhammer 𝕂 n) * Polynomial.eval a (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹ :
      FormalMultilinearSeries 𝕂 𝔸 𝔸)

Tactic:
simp [mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
hk : k < n
inl :
  ∀ (h : (↑k : 𝕂) = -a),
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
      0
inr :
  ∀ (h : (↑k : 𝕂) = -b),
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
      0
inr₁ :
  ∀ (h : (↑k : 𝕂) = -c),
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
      0
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0

Tactic:
rcases habc with h | h | h
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -a
inl :
  ∀ (x : (i : Fin n) → 𝔸),
    Eq (α := 𝔸)
      ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸)
              (ordinaryHypergeometricCoefficient a b c n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
            (a : (i : Fin n) → 𝔸) → 𝔸)
          x :
        𝔸)
      ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -a
x : (i : Fin n) → 𝔸
⊢ Eq (α := 𝔸)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
          (a : (i : Fin n) → 𝔸) → 𝔸)
        x :
      𝔸)
    ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)

Tactic:
simp [(ascPochhammer_eval_eq_zero_iff n _).2 ⟨k, hk, h⟩]

Premises used: Iff.mpr, ascPochhammer_eval_eq_zero_iff, And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -b
inr :
  ∀ (x : (i : Fin n) → 𝔸),
    Eq (α := 𝔸)
      ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸)
              (ordinaryHypergeometricCoefficient a b c n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
            (a : (i : Fin n) → 𝔸) → 𝔸)
          x :
        𝔸)
      ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -b
x : (i : Fin n) → 𝔸
⊢ Eq (α := 𝔸)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
          (a : (i : Fin n) → 𝔸) → 𝔸)
        x :
      𝔸)
    ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)

Tactic:
simp [(ascPochhammer_eval_eq_zero_iff n _).2 ⟨k, hk, h⟩]

Premises used: Iff.mpr, ascPochhammer_eval_eq_zero_iff, And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -c
inr :
  ∀ (x : (i : Fin n) → 𝔸),
    Eq (α := 𝔸)
      ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸)
              (ordinaryHypergeometricCoefficient a b c n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
            (a : (i : Fin n) → 𝔸) → 𝔸)
          x :
        𝔸)
      ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -c
x : (i : Fin n) → 𝔸
⊢ Eq (α := 𝔸)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
          (a : (i : Fin n) → 𝔸) → 𝔸)
        x :
      𝔸)
    ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)

Tactic:
simp [(ascPochhammer_eval_eq_zero_iff n _).2 ⟨k, hk, h⟩]

Premises used: Iff.mpr, ascPochhammer_eval_eq_zero_iff, And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k : ℕ
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) b c) = ⊤

Tactic:
FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_

Premises used: HAdd.hAdd, FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k : ℕ
refine :
  ∀ (n : ℕ),
    Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin (n + (1 + k))) ↦ 𝔸) 𝔸)
      (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) b c (n + (1 + k))) 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) b c) = ⊤

Tactic:
refine FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_

Premises used: HAdd.hAdd, FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ Eq.{u_1 + 1} (α := 𝕂) (↑k : 𝕂) (- -(↑k : 𝕂)) ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ k < n + (1 + k)

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin (n + (1 + k))) ↦ 𝔸) 𝔸)
    (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) b c (n + (1 + k))) 0

Tactic:
exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat (-(k : 𝕂)) b c (by aesop) (by lia)

Premises used: Nat.cast, ordinaryHypergeometricSeries_eq_zero_of_neg_nat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a c : 𝕂
k : ℕ
rw : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) a c) = ⊤
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 a (-(↑k : 𝕂)) c) = ⊤

Tactic:
rw [ordinaryHypergeometricSeries_symm]

Premises used: ordinaryHypergeometricSeries_symm
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a c : 𝕂
k : ℕ
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) a c) = ⊤

Tactic:
ordinaryHypergeometric_radius_top_of_neg_nat₁ 𝔸 a c

Premises used: ordinaryHypergeometric_radius_top_of_neg_nat₁
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a c : 𝕂
k : ℕ
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) a c) = ⊤

Tactic:
exact ordinaryHypergeometric_radius_top_of_neg_nat₁ 𝔸 a c

Premises used: ordinaryHypergeometric_radius_top_of_neg_nat₁
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k : ℕ
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 a b (-(↑k : 𝕂))) = ⊤

Tactic:
FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_

Premises used: HAdd.hAdd, FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_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 : 𝕂
k : ℕ
refine :
  ∀ (n : ℕ),
    Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin (n + (1 + k))) ↦ 𝔸) 𝔸)
      (ordinaryHypergeometricSeries 𝔸 a b (-(↑k : 𝕂)) (n + (1 + k))) 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 a b (-(↑k : 𝕂))) = ⊤

Tactic:
refine FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_

Premises used: HAdd.hAdd, FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_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 : 𝕂
k n : ℕ
⊢ (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ Eq.{u_1 + 1} (α := 𝕂) (↑k : 𝕂) (- -(↑k : 𝕂))

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k n : ℕ
⊢ k < n + (1 + k)

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k n : ℕ
⊢ Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin (n + (1 + k))) ↦ 𝔸) 𝔸)
    (ordinaryHypergeometricSeries 𝔸 a b (-(↑k : 𝕂)) (n + (1 + k))) 0

Tactic:
exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat a b (-(k : 𝕂)) (by aesop) (by lia)

Premises used: Nat.cast, ordinaryHypergeometricSeries_eq_zero_of_neg_nat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0 ↔
    ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
⟨fun h ↦ ?_, fun zero ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
refine_1 :
  ∀ (h : Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0),
    ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
refine_2 :
  ∀ (zero : ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c),
    Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0
⊢ Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0 ↔
    ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
refine ⟨fun h ↦ ?_, fun zero ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0
⊢ ordinaryHypergeometricCoefficient a b c n = 0

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_eq_zero] at h

Premises used: FormalMultilinearSeries.ofScalars_eq_zero, ordinaryHypergeometricSeries