-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
/-- If any parameter to the series is a sufficiently large nonpositive integer, then the series
term is zero. -/
lemma ordinaryHypergeometricSeries_eq_zero_of_neg_nat {n k : ℕ} (habc : k = -a ∨ k = -b ∨ k = -c)
    (hk : k < n) : ordinaryHypergeometricSeries 𝔸 a b c n = 0

Proof state:
case inr.inr.H
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -c
x✝ : Fin n → 𝔸
⊢ (ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) x✝ = 0 x✝

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

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
hk : k < n
⊢ ordinaryHypergeometricSeries 𝔸 a b c n = 0

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
hk : k < n
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

Proof state:
case inr.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -c
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

Tactic:
ext

Result:
case inr.inr.H
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -c
x✝ : Fin n → 𝔸
⊢ (ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) x✝ = 0 x✝

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
hk : k < n
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

Tactic:
rcases habc with h | h | h

Result:
case inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -a
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

case inr.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -b
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

case inr.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -c
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

Proof state:
case inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -a
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

case inr.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -b
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

case inr.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -c
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

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

Result:
no goals