awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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) = ⊤
have refine : ∀ (n : ℕ),
  Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin (n + (1 + k))) ↦ 𝔸) 𝔸)
    (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) b c (n + (1 + k))) 0
Tactic: refine FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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 𝔸 a (-(↑k : 𝕂)) c) = ⊤
have rw : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-(↑k : 𝕂)) a c) = ⊤
Tactic: rw [ordinaryHypergeometricSeries_symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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 : 𝕂))) = ⊤
have refine : ∀ (n : ℕ),
  Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin (n + (1 + k))) ↦ 𝔸) 𝔸)
    (ordinaryHypergeometricSeries 𝔸 a b (-(↑k : 𝕂)) (n + (1 + k))) 0
Tactic: refine FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
have refine_1 : ∀ (h : 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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0 ↔
    ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have refine_2 : ∀ (zero : ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c),
  Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0
Tactic: refine ⟨fun h ↦ ?_, fun zero ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (hypothesis)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have h₁ : ordinaryHypergeometricCoefficient a b c n = 0
Tactic: rw [ordinaryHypergeometricSeries, ofScalars_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (hypothesis)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have 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
Tactic: simp only [_root_.mul_eq_zero, inv_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have refine_1 : ∀ (hn : Eq.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
Tactic: rcases h with ((hn | h) | h) | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have refine_1₁ : ∀ (h : Polynomial.eval a (ascPochhammer 𝕂 n) = 0), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
Tactic: rcases h with ((hn | h) | h) | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have refine_1₂ : ∀ (h : Polynomial.eval b (ascPochhammer 𝕂 n) = 0), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
Tactic: rcases h with ((hn | h) | h) | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have refine_1₃ : ∀ (h : Polynomial.eval c (ascPochhammer 𝕂 n) = 0), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
Tactic: rcases h with ((hn | h) | h) | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have refine_1 : ∀ (kn : ℕ) (hkn : kn < n) (hn : (↑kn : 𝕂) = -a), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
Tactic: obtain ⟨kn, hkn, hn⟩ := (ascPochhammer_eval_eq_zero_iff _ _).1 h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ (↑kn : 𝕂) = -a ∨ (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
have tauto : ¬(↑kn : 𝕂) = -a → (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have refine_1 : ∀ (kn : ℕ) (hkn : kn < n) (hn : (↑kn : 𝕂) = -b), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
Tactic: obtain ⟨kn, hkn, hn⟩ := (ascPochhammer_eval_eq_zero_iff _ _).1 h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ (↑kn : 𝕂) = -a ∨ (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
have tauto : ¬(↑kn : 𝕂) = -a → (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ (↑kn : 𝕂) = -a ∨ (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
have tauto₃ : ¬(↑kn : 𝕂) = -a → ¬(↑kn : 𝕂) = -b → (↑kn : 𝕂) = -c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
have refine_1 : ∀ (kn : ℕ) (hkn : kn < n) (hn : (↑kn : 𝕂) = -c), ∃ k < n, (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
Tactic: obtain ⟨kn, hkn, hn⟩ := (ascPochhammer_eval_eq_zero_iff _ _).1 h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ (↑kn : 𝕂) = -a ∨ (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
have tauto : ¬(↑kn : 𝕂) = -a → (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ (↑kn : 𝕂) = -a ∨ (↑kn : 𝕂) = -b ∨ (↑kn : 𝕂) = -c
have tauto₃ : ¬(↑kn : 𝕂) = -a → ¬(↑kn : 𝕂) = -b → (↑kn : 𝕂) = -c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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
⊢ Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c n) 0
have 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
Tactic: obtain ⟨_, h, hn⟩ := zero
Cleared hypotheses: zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖ =
    ‖a + (↑n : 𝕂)‖⁻¹ * ‖b + (↑n : 𝕂)‖⁻¹ * ‖c + (↑n : 𝕂)‖ * ‖HAdd.hAdd (α := 𝕂) 1 (↑n : 𝕂)‖
have 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 : 𝕂)‖
Tactic: simp only [mul_inv_rev, factorial_succ, cast_mul, cast_add,
    cast_one, ascPochhammer_succ_eval, norm_mul, norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖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 : 𝕂)‖
have 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 : 𝕂)‖
Tactic: simp only [inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖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 : 𝕂)‖
have 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 : 𝕂)‖
Tactic: rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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 : 𝕂)‖
⊢ ‖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 : 𝕂)‖
have a₁ : ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0
Tactic: rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖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 : 𝕂)‖
have 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 : 𝕂)‖
Tactic: rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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 : 𝕂)‖
⊢ ‖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 : 𝕂)‖
have a₁ : ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0
Tactic: rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖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 : 𝕂)‖
have 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 : 𝕂)‖
Tactic: rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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 : 𝕂)‖
⊢ ‖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 : 𝕂)‖
have a₁ : ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0
Tactic: rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
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 ! : 𝕂) * (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 : 𝕂)‖
have a₁ : Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) ≠ 0
Tactic: rw [DivisionRing.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, (↑kn : 𝕂) ≠ -a ∧ (↑kn : 𝕂) ≠ -b ∧ (↑kn : 𝕂) ≠ -c
⊢ ‖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 : 𝕂)‖
have a₁ : Norm.norm.{u_1} (E := 𝕂) (↑n ! : 𝕂) ≠ 0
Tactic: repeat rw [DivisionRing.mul_inv_cancel, one_mul]