awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ k
⊢ f ^ p ^ (k + 1) =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)
have succ : HPow.hPow (α := MvPowerSeries σ R)
    ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
    p =
  (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
    ((expand (p ^ (k + 1)) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)
Tactic: conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ k
⊢ HPow.hPow (α := MvPowerSeries σ R)
      ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
        MvPowerSeries σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)
have succ : Eq (α := MvPowerSeries σ R)
  ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
    MvPowerSeries σ R)
  ((map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
    MvPowerSeries σ R)
Tactic: simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ k
succ :
  Eq (α := MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
      MvPowerSeries σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
⊢ HPow.hPow (α := MvPowerSeries σ R)
      ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
        MvPowerSeries σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)
have succ₁ : Eq (α := MvPowerSeries σ R)
  ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
    MvPowerSeries σ R)
  ((map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p * p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
    MvPowerSeries σ R)
Tactic: simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ k
succ :
  Eq (α := MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
      MvPowerSeries σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
succ₁ :
  Eq (α := MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
      MvPowerSeries σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p * p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
⊢ HPow.hPow (α := MvPowerSeries σ R)
      ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
        MvPowerSeries σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)
have succ₂ : Eq (α := MvPowerSeries σ R)
  ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
    MvPowerSeries σ R)
  ((map (iterateFrobenius R p (1 + k)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p * p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
    MvPowerSeries σ R)
Tactic: simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : ℕ
⊢ (map (iterateFrobenius R p n) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ n) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ n
have zero : (map (iterateFrobenius R p 0) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
    ((expand (HPow.hPow (β := ℕ) p 0) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
  f ^ HPow.hPow (β := ℕ) p 0
Tactic: induction n with
  | zero => simp [map_id]
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : ℕ
zero :
  (map (iterateFrobenius R p 0) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (HPow.hPow (β := ℕ) p 0) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ HPow.hPow (β := ℕ) p 0
⊢ (map (iterateFrobenius R p n) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ n) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ n
have succ : ∀ (k : ℕ)
  (n_ih :
    (map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
      f ^ p ^ k),
  (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ (k + 1)
Tactic: induction n with
  | zero => simp [map_id]
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
⊢ LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
have pos : ∀ (h : HasGaussNorm v c f),
  LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
Tactic: by_cases h : HasGaussNorm v c f
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
pos :
  ∀ (h : HasGaussNorm v c f),
    LE.le (α := ℝ) 0
      (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
⊢ LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
have neg : ∀ (h : ¬HasGaussNorm v c f),
  LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
Tactic: by_cases h : HasGaussNorm v c f
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
⊢ LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
have trans : 0 ≤ v ((constantCoeff : (a : MvPowerSeries σ R) → R) f)
Tactic: trans v (constantCoeff f)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
trans : 0 ≤ v ((constantCoeff : (a : MvPowerSeries σ R) → R) f)
⊢ LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
have trans₁ : v ((constantCoeff : (a : MvPowerSeries σ R) → R) f) ≤
  ⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2
Tactic: trans v (constantCoeff f)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
⊢ v ((constantCoeff : (a : MvPowerSeries σ R) → R) f) ≤
    ⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2
have h₁ : v ((constantCoeff : (a : MvPowerSeries σ R) → R) f) =
  v ((coeff 0 : (a : MvPowerSeries σ R) → R) f) * Finsupp.prod 0 fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2
Tactic: convert! (le_gaussNorm v c f h 0)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
⊢ gaussNorm v c f = 0 ↔ f = 0
have refine : gaussNorm v c f = 0 → f = 0
Tactic: refine ⟨?_, fun hf ↦ by simp [hf, vZero]⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
⊢ gaussNorm v c f = 0 → f = 0
have contrapose! : f ≠ 0 → gaussNorm v c f ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
⊢ gaussNorm v c f ≠ 0
have h : 0 < gaussNorm v c f
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
⊢ 0 < gaussNorm v c f
have h : ∀ (n : σ →₀ ℕ) (hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)), 0 < gaussNorm v c f
Tactic: obtain ⟨n, hn⟩ := (MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero f).mp hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 0 <
    v ((coeff n : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ n.support, HPow.hPow (β := ℕ) (c i) ((n : (a : σ) → ℕ) i : ℕ)
have apply : 0 < v ((coeff n : (a : MvPowerSeries σ R) → R) f)
Tactic: apply mul_pos _ (by exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 0 < v ((coeff n : (a : MvPowerSeries σ R) → R) f)
have h_eq_zero₁ : v ((coeff n : (a : MvPowerSeries σ R) → R) f) = 0 →
  Eq.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: specialize h_eq_zero (f.coeff n)
Cleared hypotheses: h_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 0 < gaussNorm v c f
have v₁ : 0 < v ((coeff n : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ n.support, HPow.hPow (β := ℕ) (c i) ((n : (a : σ) → ℕ) i : ℕ)
Tactic: calc
  0 < v (f.coeff n) * ∏ i ∈ n.support, (c i) ^ (n i) := by
    apply mul_pos _ (by exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i)
    specialize h_eq_zero (f.coeff n)
    grind
  _ ≤ _ := le_gaussNorm v c f hbd n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
⊢ gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)
have H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Tactic: have H (t : σ →₀ ℕ) : 0 ≤ ∏ i ∈ t.support, c i ^ t i :=
    Finset.prod_nonneg (fun i hi ↦ pow_nonneg (hc i) (t i))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
      ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
have hv₁ : v
    (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
Tactic: specialize hv (coeff t f) (coeff t g)
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
      ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
have inl : ∀
  (h :
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
      v ((coeff t : (a : MvPowerSeries σ R) → R) f)),
  v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
      ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Tactic: rcases max_choice (v ((coeff t) f)) (v ((coeff t) g)) with h | h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
inl :
  ∀
    (h :
      max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
        v ((coeff t : (a : MvPowerSeries σ R) → R) f)),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
      ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
have inr : ∀
  (h :
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
      v ((coeff t : (a : MvPowerSeries σ R) → R) g)),
  v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
      ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Tactic: rcases max_choice (v ((coeff t) f)) (v ((coeff t) g)) with h | h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
⊢ max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
have simp : v ((coeff t : (a : MvPowerSeries σ R) → R) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
  v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
Tactic: simp only [sup_eq_left]