awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
⊢ ¬s = 0
have contrapose : ∀ (s0 : s = 0), s ∉ (R⁰ : Submonoid R)
Tactic: contrapose s0
Cleared hypotheses: s0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
have iterate : Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])
Tactic: iterate 2
    apply mul_ne_zero hq.ne_zero
    rw [Ne, C_eq_zero]
    contrapose s0
    simp [s0, mem_nonZeroDivisors_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart
iterate : Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
have iterate₁ : ¬s = 0
Tactic: iterate 2
    apply mul_ne_zero hq.ne_zero
    rw [Ne, C_eq_zero]
    contrapose s0
    simp [s0, mem_nonZeroDivisors_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart
iterate : Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])
iterate₁ : ¬s = 0
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
have iterate₂ : ∀ (s0 : s = 0), s ∉ (R⁰ : Submonoid R)
Tactic: iterate 2
    apply mul_ne_zero hq.ne_zero
    rw [Ne, C_eq_zero]
    contrapose s0
    simp [s0, mem_nonZeroDivisors_iff_ne_zero]
Cleared hypotheses: s0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
⊢ ∃ (i : ℕ), gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
have pos : ∀ (h_supp : p.support.Nonempty),
  ∃ (i : ℕ), gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: by_cases h_supp : p.support.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
pos :
  ∀ (h_supp : p.support.Nonempty),
    ∃ (i : ℕ), gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ ∃ (i : ℕ), gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
have neg : ∀ (h_supp : ¬p.support.Nonempty),
  ∃ (i : ℕ), gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: by_cases h_supp : p.support.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
h_supp : p.support.Nonempty
⊢ ∃ (i : ℕ), gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
have pos : ∃ (i : ℕ),
  (if h : True then p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
    else 0) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: simp only [gaussNorm, h_supp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
h_supp : p.support.Nonempty
⊢ ∃ (i : ℕ),
    (if h : True then p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
      else 0) =
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
have pos : ∀ (i : ℕ) (hi1 : i ∈ p.support)
  (hi2 :
    (p.support.sup' h_supp fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)) =
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)),
  ∃ (i : ℕ),
    (if h : True then p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
      else 0) =
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: obtain ⟨i, hi1, hi2⟩ := Finset.exists_mem_eq_sup' h_supp fun i ↦ (v (p.coeff i) * c ^ i)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
inst_2 : ZeroHomClass F R ℝ
r : R
⊢ gaussNorm.{u_1, u_2} (R := R) v c ((C : (a : R) → R[X]) r) = (v : (a : R) → ℝ) r
have pos : ∀ (hr : r = 0), gaussNorm.{u_1, u_2} (R := R) v c ((C : (a : R) → R[X]) r) = (v : (a : R) → ℝ) r
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
inst_2 : ZeroHomClass F R ℝ
r : R
pos : ∀ (hr : r = 0), gaussNorm.{u_1, u_2} (R := R) v c ((C : (a : R) → R[X]) r) = (v : (a : R) → ℝ) r
⊢ gaussNorm.{u_1, u_2} (R := R) v c ((C : (a : R) → R[X]) r) = (v : (a : R) → ℝ) r
have neg : ∀ (hr : ¬r = 0), gaussNorm.{u_1, u_2} (R := R) v c ((C : (a : R) → R[X]) r) = (v : (a : R) → ℝ) r
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
inst_2 : ZeroHomClass F R ℝ
n : ℕ
r : R
⊢ gaussNorm.{u_1, u_2} (R := R) v c ((monomial n : (a : R) → R[X]) r) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) r : ℝ) (c ^ n)
have pos : ∀ (hr : r = 0),
  gaussNorm.{u_1, u_2} (R := R) v c ((monomial n : (a : R) → R[X]) r) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) r : ℝ) (c ^ n)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
inst_2 : ZeroHomClass F R ℝ
n : ℕ
r : R
pos :
  ∀ (hr : r = 0),
    gaussNorm.{u_1, u_2} (R := R) v c ((monomial n : (a : R) → R[X]) r) =
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) r : ℝ) (c ^ n)
⊢ gaussNorm.{u_1, u_2} (R := R) v c ((monomial n : (a : R) → R[X]) r) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) r : ℝ) (c ^ n)
have neg : ∀ (hr : ¬r = 0),
  gaussNorm.{u_1, u_2} (R := R) v c ((monomial n : (a : R) → R[X]) r) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) r : ℝ) (c ^ n)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
inst_2 : NonnegHomClass F R ℝ
p : R[X]
h : p.support.Nonempty
hc : 0 ≤ c
⊢ LE.le (α := ℝ) 0 (p.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
have simp : ∃ (b : ℕ), p.coeff b ≠ 0 ∧ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff b) : ℝ) (c ^ b)
Tactic: simp only [Finset.le_sup'_iff, mem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
inst_2 : NonnegHomClass F R ℝ
p : R[X]
h : p.support.Nonempty
hc : 0 ≤ c
⊢ ∃ (b : ℕ), p.coeff b ≠ 0 ∧ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff b) : ℝ) (c ^ b)
have h₁ : p.coeff p.natDegree ≠ 0 ∧ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff p.natDegree) : ℝ) (c ^ p.natDegree)
Tactic: use p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
inst_2 : NonnegHomClass F R ℝ
p : R[X]
h : p.support.Nonempty
hc : 0 ≤ c
⊢ p.coeff p.natDegree ≠ 0 ∧ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff p.natDegree) : ℝ) (c ^ p.natDegree)
have h₁ : ∀ (h : ¬p = 0) (hc : 0 ≤ c), 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) p.leadingCoeff : ℝ) (c ^ p.natDegree)
Tactic: simp_all only [support_nonempty, ne_eq, coeff_natDegree, leadingCoeff_eq_zero, not_false_eq_true,
    true_and]
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
f : ↥p.support → ℝ :=
  fun (i : ↥p.support) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (↑i : ℕ)) : ℝ) (c ^ (↑i : ℕ))
⊢ (f '' ⊤ ∪ {0}).Finite
have apply : (f '' ⊤).Finite
Tactic: apply Set.Finite.union _ <| Set.finite_singleton 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
f : ↥p.support → ℝ :=
  fun (i : ↥p.support) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (↑i : ℕ)) : ℝ) (c ^ (↑i : ℕ))
⊢ (f '' ⊤).Finite
have apply : Set.Finite (α := ↥p.support) ⊤
Tactic: apply Set.Finite.image f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
f : ↥p.support → ℝ :=
  fun (i : ↥p.support) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (↑i : ℕ)) : ℝ) (c ^ (↑i : ℕ))
⊢ Set.Finite (α := ↥p.support) ⊤
have rw : Finite (↑(↑p.support : Set ℕ) : Type)
Tactic: rw [Set.top_eq_univ, Set.finite_univ_iff, ← @Finset.coe_sort_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
f : ↥p.support → ℝ :=
  fun (i : ↥p.support) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (↑i : ℕ)) : ℝ) (c ^ (↑i : ℕ))
⊢ BddAbove (α := ℝ) {x : ℝ | ∃ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) = x}
have h_fin : (f '' ⊤ ∪ {0}).Finite
Tactic: have h_fin : (f '' ⊤ ∪ {0}).Finite := by
    apply Set.Finite.union _ <| Set.finite_singleton 0
    apply Set.Finite.image f
    rw [Set.top_eq_univ, Set.finite_univ_iff, ← @Finset.coe_sort_coe]
    exact Finite.of_fintype p.support
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
f : ↥p.support → ℝ :=
  fun (i : ↥p.support) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (↑i : ℕ)) : ℝ) (c ^ (↑i : ℕ))
h_fin : (f '' ⊤ ∪ {0}).Finite
⊢ BddAbove (α := ℝ) {x : ℝ | ∃ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) = x}
have refine : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) = x}
      x →
    x ∈ f '' ⊤ ∪ {0}
Tactic: refine Set.Finite.bddAbove <| Set.Finite.subset h_fin fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
f : ↥p.support → ℝ :=
  fun (i : ↥p.support) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (↑i : ℕ)) : ℝ) (c ^ (↑i : ℕ))
h_fin : (f '' ⊤ ∪ {0}).Finite
x : ℝ
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) = x}
      x →
    x ∈ f '' ⊤ ∪ {0}
have simp : Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) = x} x →
  x = 0 ∨ ∃ (a : ℕ) (h : p.coeff a ≠ 0), f (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ p.support) a sorry) = x
Tactic: simp only [Set.top_eq_univ, Set.image_univ, Set.union_singleton, Set.mem_insert_iff,
    Set.mem_range, Subtype.exists, mem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
⊢ PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = gaussNorm v c p
have pos : ∀ (hp : p = 0), PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = gaussNorm v c p
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
pos : ∀ (hp : p = 0), PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = gaussNorm v c p
⊢ PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = gaussNorm v c p
have neg : ∀ (hp : ¬p = 0), PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = gaussNorm v c p
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = gaussNorm v c p
have neg : Eq (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
  (p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
Tactic: simp only [PowerSeries.gaussNorm_eq, coeff_coe, gaussNorm, support_nonempty, ne_eq, hp,
      not_false_eq_true, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ Eq (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
have neg : LE.le (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
  (p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
neg :
  LE.le (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
⊢ Eq (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
have neg₁ : LE.le (α := ℝ) (p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
  (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ LE.le (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
have neg : ∀ (x : ℕ),
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) ≤
    p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: apply ciSup_le
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
have pos : ∀ (h : n ∈ p.support),
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
    p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: by_cases h : n ∈ p.support
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
pos :
  ∀ (h : n ∈ p.support),
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
      p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
have neg : ∀ (h : n ∉ p.support),
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
    p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: by_cases h : n ∈ p.support
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ LE.le (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
have neg : ∀ (i : ℕ) (hi : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)),
  LE.le (α := ℝ) (p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
Tactic: obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
i : ℕ
hi : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ LE.le (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
have hi₁ : (p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)) =
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: simp only [gaussNorm, support_nonempty.mpr hp, ↓reduceDIte] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
i : ℕ
hi :
  (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ LE.le (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
have neg : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤
  ⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: rw [hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
⊢ gaussNorm v c p = 0 ↔ p = 0
have rw : PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = 0 ↔ p = 0
Tactic: rw [← gaussNorm_coe_powerSeries _ _ (le_of_lt hc)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
⊢ PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = 0 ↔ p = 0
have h : p = 0 ↔ (↑p : PowerSeries R) = 0
Tactic: convert!
    PowerSeries.gaussNorm_eq_zero_iff v c p (by grind) (by simp) h_eq_zero hc
      (by simpa [PowerSeries.HasGaussNorm] using aux_bdd v p)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : NonnegHomClass F R ℝ
hc : 0 ≤ c
⊢ 0 ≤ gaussNorm v c p
have pos : ∀ (hp : p.support.Nonempty), 0 ≤ gaussNorm v c p
Tactic: by_cases hp : p.support.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : NonnegHomClass F R ℝ
hc : 0 ≤ c
pos : ∀ (hp : p.support.Nonempty), 0 ≤ gaussNorm v c p
⊢ 0 ≤ gaussNorm v c p
have neg : ∀ (hp : ¬p.support.Nonempty), 0 ≤ gaussNorm v c p
Tactic: by_cases hp : p.support.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c p
have rw : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((PowerSeries.coeff i : (a : PowerSeries R) → R) (↑p : PowerSeries R) : R) : ℝ)
    (c ^ i) ≤
  PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R)
Tactic: rw [← gaussNorm_coe_powerSeries _ _ hc, ← coeff_coe]