awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
apply : 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

Tactic:
apply mul_ne_zero hq.ne_zero

Premises used: Polynomial.IsPrimitive.ne_zero, mul_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
rw : ¬s = 0
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])

Tactic:
rw [Ne, C_eq_zero]

Premises used: Polynomial.C_eq_zero, Ne
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
contrapose : ∀ (s0 : s = 0), s ∉ (R⁰ : Submonoid R)
⊢ ¬s = 0

Tactic:
contrapose s0
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
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
s0 : s = 0
⊢ s ∉ (R⁰ : Submonoid R)

Tactic:
simp [s0, mem_nonZeroDivisors_iff_ne_zero]

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
apply : 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

Tactic:
apply mul_ne_zero hq.ne_zero

Premises used: Polynomial.IsPrimitive.ne_zero, mul_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
rw : ¬s = 0
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])

Tactic:
rw [Ne, C_eq_zero]

Premises used: Polynomial.C_eq_zero, Ne
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
contrapose : ∀ (s0 : s = 0), s ∉ (R⁰ : Submonoid R)
⊢ ¬s = 0

Tactic:
contrapose s0
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
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
s0 : s = 0
⊢ s ∉ (R⁰ : Submonoid R)

Tactic:
simp [s0, mem_nonZeroDivisors_iff_ne_zero]

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
iterate₂ : ∀ (s0 : s = 0), s ∉ (R⁰ : Submonoid R)
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 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]

Premises used: Polynomial.C_eq_zero, Ne, Polynomial.IsPrimitive.ne_zero, mem_nonZeroDivisors_iff_ne_zero, mul_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ p ∣ q ↔ Dvd.dvd (α := K[X]) (map (algebraMap R K) p) (map (algebraMap R K) q)

Tactic:
⟨fun ⟨a, b⟩ => ⟨a.map (algebraMap R K), b.symm ▸ Polynomial.map_mul (algebraMap R K)⟩, fun h =>
    hp.dvd_of_fraction_map_dvd_fraction_map hq h⟩

Premises used: _private.0.Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map.match_1, Polynomial.map_mul, Dvd.dvd, Algebra.algebraMap, Eq.rec, Polynomial.IsPrimitive.dvd_of_fraction_map_dvd_fraction_map, Iff.intro, Exists.intro, Polynomial.map, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
p : ℤ[X]
hp : p.IsPrimitive
⊢ Irreducible p ↔ Irreducible (map (Int.castRingHom ℚ) p)

Tactic:
hp.irreducible_iff_irreducible_map_fraction_map

Premises used: Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
p q : ℤ[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ p ∣ q ↔ map (Int.castRingHom ℚ) p ∣ map (Int.castRingHom ℚ) q

Tactic:
hp.dvd_iff_fraction_map_dvd_fraction_map ℚ hq

Premises used: Rat, Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
⊢ gaussNorm.{u_1, u_2} (R := R) v c 0 = 0

Tactic:
simp [gaussNorm]

Premises used: Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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)
neg :
  ∀ (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)

Tactic:
by_cases h_supp : p.support.Nonempty

Premises used: Finset.Nonempty, Polynomial.support
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
pos :
  ∃ (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)
⊢ ∃ (i : ℕ), gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
simp only [gaussNorm, h_supp]

Premises used: Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
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' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
        else 0) =
        HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ ∃ (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)

Tactic:
obtain ⟨i, hi1, hi2⟩ := Finset.exists_mem_eq_sup' h_supp fun i ↦ (v (p.coeff i) * c ^ i)

Premises used: HMul.hMul, Polynomial.coeff, HPow.hPow, Finset.exists_mem_eq_sup', DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 : ℕ
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' ⋯ 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:
⟨i, hi2⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 : ℕ
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' ⋯ 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:
exact ⟨i, hi2⟩
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
neg : ∀ (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

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
hr : r = 0
⊢ gaussNorm.{u_1, u_2} (R := R) v c ((C : (a : R) → R[X]) r) = (v : (a : R) → ℝ) r

Tactic:
simp [gaussNorm, support_C, hr]

Premises used: Polynomial.support_C, Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
hr : ¬r = 0
⊢ gaussNorm.{u_1, u_2} (R := R) v c ((C : (a : R) → R[X]) r) = (v : (a : R) → ℝ) r

Tactic:
simp [gaussNorm, support_C, hr]

Premises used: Polynomial.support_C, Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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)
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)
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
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:
simp [gaussNorm, support_monomial, hr]

Premises used: Polynomial.support_monomial, Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
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:
simp [gaussNorm, support_monomial, hr]

Premises used: Polynomial.support_monomial, Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
simp : ∃ (b : ℕ), p.coeff b ≠ 0 ∧ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff b) : ℝ) (c ^ b)
⊢ LE.le (α := ℝ) 0 (p.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))

Tactic:
simp only [Finset.le_sup'_iff, mem_support_iff]

Premises used: Finset.le_sup'_iff, Polynomial.mem_support_iff
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
h₁ : p.coeff p.natDegree ≠ 0 ∧ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff p.natDegree) : ℝ) (c ^ p.natDegree)
⊢ ∃ (b : ℕ), p.coeff b ≠ 0 ∧ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff b) : ℝ) (c ^ b)

Tactic:
use p.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
h₁ : ∀ (h : ¬p = 0) (hc : 0 ≤ c), 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) p.leadingCoeff : ℝ) (c ^ p.natDegree)
⊢ p.coeff p.natDegree ≠ 0 ∧ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff p.natDegree) : ℝ) (c ^ p.natDegree)

Tactic:
simp_all only [support_nonempty, ne_eq, coeff_natDegree, leadingCoeff_eq_zero, not_false_eq_true,
    true_and]

Premises used: Polynomial.coeff_natDegree, ne_eq, not_false_eq_true, Polynomial.leadingCoeff_eq_zero, Polynomial.support_nonempty, true_and
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 = 0
hc : 0 ≤ c
⊢ 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) p.leadingCoeff : ℝ) (c ^ p.natDegree)

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 : ℕ))
apply : (f '' ⊤).Finite
⊢ (f '' ⊤ ∪ {0}).Finite

Tactic:
apply Set.Finite.union _ <| Set.finite_singleton 0

Premises used: Set.Finite.union, OfNat.ofNat, Set.finite_singleton
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 : ℕ))
apply : Set.Finite (α := ↥p.support) ⊤
⊢ (f '' ⊤).Finite

Tactic:
apply Set.Finite.image f

Premises used: Set.Finite.image
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 : ℕ))
rw : Finite (↑(↑p.support : Set ℕ) : Type)
⊢ Set.Finite (α := ↥p.support) ⊤

Tactic:
rw [Set.top_eq_univ, Set.finite_univ_iff, ← @Finset.coe_sort_coe]

Premises used: Finset.coe_sort_coe, Set.top_eq_univ, Set.finite_univ_iff
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 : ℕ))
⊢ Finite (↑(↑p.support : Set ℕ) : Type)

Tactic:
Finite.of_fintype p.support

Premises used: Membership.mem, Subtype, Finite.of_fintype, Polynomial.support
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 : ℕ))
⊢ Finite (↑(↑p.support : Set ℕ) : Type)

Tactic:
exact Finite.of_fintype p.support

Premises used: Membership.mem, Subtype, Finite.of_fintype, Polynomial.support
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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

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
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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}

Tactic:
Set.Finite.bddAbove <| Set.Finite.subset h_fin fun _ ↦ ?_

Premises used: Set.Finite.subset, Set.Finite.bddAbove
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
refine :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) = x}
        x →
      x ∈ f '' ⊤ ∪ {0}
⊢ BddAbove (α := ℝ) {x : ℝ | ∃ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) = x}

Tactic:
refine Set.Finite.bddAbove <| Set.Finite.subset h_fin fun _ ↦ ?_

Premises used: Set.Finite.subset, Set.Finite.bddAbove
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 : ℝ
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 ⋯) = x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) = x}
      x →
    x ∈ f '' ⊤ ∪ {0}

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]

Premises used: Set.image_univ, Set.mem_range, Subtype.exists, Polynomial.mem_support_iff, Set.top_eq_univ, Set.mem_insert_iff, Set.union_singleton
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 = 0 ∨ ∃ (a : ℕ) (h : p.coeff a ≠ 0), f (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ p.support) a ⋯) = x

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
neg : ∀ (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

Tactic:
by_cases hp : p = 0