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 : 𝕂
n : ℕ
h : ordinaryHypergeometricCoefficient a b c n = 0
⊢ ((Eq.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0 ∨ Polynomial.eval a (ascPochhammer 𝕂 n) = 0) ∨
      Polynomial.eval b (ascPochhammer 𝕂 n) = 0) ∨
    Polynomial.eval c (ascPochhammer 𝕂 n) = 0

Tactic:
simp only [_root_.mul_eq_zero, inv_eq_zero] at h

Premises used: inv_eq_zero, mul_eq_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.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0 ∨ Polynomial.eval a (ascPochhammer 𝕂 n) = 0) ∨
      Polynomial.eval b (ascPochhammer 𝕂 n) = 0) ∨
    Polynomial.eval c (ascPochhammer 𝕂 n) = 0
refine_1 : ∀ (hn : Eq.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
refine_1₁ : ∀ (h : Polynomial.eval a (ascPochhammer 𝕂 n) = 0), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
refine_1₂ : ∀ (h : Polynomial.eval b (ascPochhammer 𝕂 n) = 0), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
refine_1₃ : ∀ (h : Polynomial.eval c (ascPochhammer 𝕂 n) = 0), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
rcases h with ((hn | h) | h) | h
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
hn : Eq.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
simp [Nat.factorial_ne_zero] at hn

Premises used: Nat.factorial_ne_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 : Polynomial.eval a (ascPochhammer 𝕂 n) = 0
refine_1 : ∀ (kn : ℕ) (hkn : kn < n) (hn : (↑kn : 𝕂) = -a), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
obtain ⟨kn, hkn, hn⟩ := (ascPochhammer_eval_eq_zero_iff _ _).1 h

Premises used: ascPochhammer_eval_eq_zero_iff, Iff.mp
-- 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 : Polynomial.eval a (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : (↑kn : 𝕂) = -a
tauto tauto₁ : ¬(↑kn : 𝕂) = -a → (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
⊢ (↑kn : 𝕂) = -a ∨ (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c

Tactic:
tauto
-- 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 : Polynomial.eval a (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : (↑kn : 𝕂) = -a
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
exact ⟨kn, hkn, by tauto⟩
-- 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 : Polynomial.eval b (ascPochhammer 𝕂 n) = 0
refine_1 : ∀ (kn : ℕ) (hkn : kn < n) (hn : (↑kn : 𝕂) = -b), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
obtain ⟨kn, hkn, hn⟩ := (ascPochhammer_eval_eq_zero_iff _ _).1 h

Premises used: ascPochhammer_eval_eq_zero_iff, Iff.mp
-- 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 : Polynomial.eval b (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : (↑kn : 𝕂) = -b
tauto tauto₁ tauto₂ : ¬(↑kn : 𝕂) = -a → (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
tauto₃ tauto₄ : ¬(↑kn : 𝕂) = -a → ¬(↑kn : 𝕂) = -b → (↑kn : 𝕂) = -c
⊢ (↑kn : 𝕂) = -a ∨ (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c

Tactic:
tauto
-- 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 : Polynomial.eval b (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : (↑kn : 𝕂) = -b
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
exact ⟨kn, hkn, by tauto⟩
-- 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 : Polynomial.eval c (ascPochhammer 𝕂 n) = 0
refine_1 : ∀ (kn : ℕ) (hkn : kn < n) (hn : (↑kn : 𝕂) = -c), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
obtain ⟨kn, hkn, hn⟩ := (ascPochhammer_eval_eq_zero_iff _ _).1 h

Premises used: ascPochhammer_eval_eq_zero_iff, Iff.mp
-- 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 : Polynomial.eval c (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : (↑kn : 𝕂) = -c
tauto tauto₁ tauto₂ : ¬(↑kn : 𝕂) = -a → (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
tauto₃ : ¬(↑kn : 𝕂) = -a → ¬(↑kn : 𝕂) = -b → (↑kn : 𝕂) = -c
⊢ (↑kn : 𝕂) = -a ∨ (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c

Tactic:
tauto
-- 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 : Polynomial.eval c (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : (↑kn : 𝕂) = -c
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c

Tactic:
exact ⟨kn, hkn, by tauto⟩
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
zero : ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
refine_2 :
  ∀ (w : ℕ) (h : w < n) (hn : (↑w : 𝕂) = -a ∨ (↑w : 𝕂) = -b ∨ (↑w : 𝕂) = -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

Tactic:
obtain ⟨_, h, hn⟩ := 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 w : ℕ
h : w < n
hn : (↑w : 𝕂) = -a ∨ (↑w : 𝕂) = -b ∨ (↑w : 𝕂) = -c
⊢ Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0

Tactic:
ordinaryHypergeometricSeries_eq_zero_of_neg_nat a b c hn h

Premises used: ordinaryHypergeometricSeries_eq_zero_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 c : 𝕂
n w : ℕ
h : w < n
hn : (↑w : 𝕂) = -a ∨ (↑w : 𝕂) = -b ∨ (↑w : 𝕂) = -c
⊢ Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0

Tactic:
exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat a b c hn h

Premises used: ordinaryHypergeometricSeries_eq_zero_of_neg_nat
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
simp :
  (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 : 𝕂)‖
⊢ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖ =
    ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖

Tactic:
simp only [mul_inv_rev, factorial_succ, cast_mul, cast_add,
    cast_one, ascPochhammer_succ_eval, norm_mul, norm_inv]

Premises used: ascPochhammer_succ_eval, Nat.factorial_succ, norm_mul, norm_inv, Nat.cast_add, Nat.cast_mul, mul_inv_rev, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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)‖⁻¹)) =
    ‖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:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
simp :
  ‖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 : 𝕂)‖
⊢ ‖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 : 𝕂)‖

Tactic:
simp only [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
rw :
  ‖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 : 𝕂)‖
a₁ : ‖Polynomial.eval a (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 : 𝕂)‖

Tactic:
rw [DivisionRing.mul_inv_cancel, one_mul]

Premises used: DivisionRing.mul_inv_cancel, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
rw :
  ‖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 : 𝕂)‖
a₁ : ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0
⊢ ‖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 : 𝕂)‖

Tactic:
rw [DivisionRing.mul_inv_cancel, one_mul]

Premises used: DivisionRing.mul_inv_cancel, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
rw :
  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 : 𝕂)‖
a₁ : ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0
⊢ ‖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 : 𝕂)‖

Tactic:
rw [DivisionRing.mul_inv_cancel, one_mul]

Premises used: DivisionRing.mul_inv_cancel, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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
⊢ 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 : 𝕂)‖

Tactic:
rw [DivisionRing.mul_inv_cancel, one_mul]

Premises used: DivisionRing.mul_inv_cancel, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
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
a₄ : ‖Polynomial.eval a (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 : 𝕂)‖

Tactic:
repeat rw [DivisionRing.mul_inv_cancel, one_mul]

Premises used: DivisionRing.mul_inv_cancel, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
⊢ Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Premises used: norm_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : Polynomial.eval c (ascPochhammer 𝕂 n) ≠ 0
⊢ ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Premises used: norm_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0
⊢ ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Premises used: norm_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : Polynomial.eval a (ascPochhammer 𝕂 n) ≠ 0
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Premises used: norm_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : ¬∃ k < n, (↑k : 𝕂) = -c
⊢ Polynomial.eval c (ascPochhammer 𝕂 n) ≠ 0

Tactic:
apply (ascPochhammer_eval_eq_zero_iff n _).not.2

Premises used: Iff.mpr, Iff.not, ascPochhammer_eval_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -c
⊢ ¬∃ k < n, (↑k : 𝕂) = -c

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
kn : ℕ
hkn : kn < n
⊢ (↑kn : 𝕂) ≠ -c

Tactic:
simp [habc kn hkn]
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -c

Tactic:
exact fun kn hkn ↦ by simp [habc kn hkn]
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : ¬∃ k < n, (↑k : 𝕂) = -b
⊢ Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0

Tactic:
apply (ascPochhammer_eval_eq_zero_iff n _).not.2

Premises used: Iff.mpr, Iff.not, ascPochhammer_eval_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -b
⊢ ¬∃ k < n, (↑k : 𝕂) = -b

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
kn : ℕ
hkn : kn < n
⊢ (↑kn : 𝕂) ≠ -b

Tactic:
simp [habc kn hkn]
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -b

Tactic:
exact fun kn hkn ↦ by simp [habc kn hkn]
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : ¬∃ k < n, (↑k : 𝕂) = -a
⊢ Polynomial.eval a (ascPochhammer 𝕂 n) ≠ 0

Tactic:
apply (ascPochhammer_eval_eq_zero_iff n _).not.2

Premises used: Iff.mpr, Iff.not, ascPochhammer_eval_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
a₁ : ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -a
⊢ ¬∃ k < n, (↑k : 𝕂) = -a

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
kn : ℕ
hkn : kn < n
⊢ (↑kn : 𝕂) ≠ -a

Tactic:
simp [habc kn hkn]
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ∀ (k : ℕ) (_ : k < n), (↑k : 𝕂) ≠ -a

Tactic:
exact fun kn hkn ↦ by simp [habc kn hkn]
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0

Tactic:
cast_ne_zero.2 (factorial_ne_zero n)

Premises used: Iff.mpr, Nat.factorial_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0

Tactic:
exact cast_ne_zero.2 (factorial_ne_zero n)

Premises used: Iff.mpr, Nat.factorial_ne_zero, Nat.cast_ne_zero
-- 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
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c)) =
    (↑1 : ENNReal)

Tactic:
ofScalars_radius_eq_of_tendsto 𝔸 _ one_ne_zero ?_

Premises used: FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto, one_ne_zero
-- 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 (fun (n : ℕ) ↦ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖)
    atTop (𝓝 (↑1 : ℝ))
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c) = 1

Tactic:
convert! ofScalars_radius_eq_of_tendsto 𝔸 _ one_ne_zero ?_

Premises used: FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto, one_ne_zero