-- 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 : 𝕂)‖⁻¹⁻¹
_₁ :
  ‖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 : 𝕂)‖
⊢ (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 : 𝕂)‖

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)

Premises used: Polynomial.eval, ascPochhammer, Nat.cast, Nat.factorial