awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
obtain :
  ∀ (Ng : ℕ) (gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b),
    ∃ (N : ℕ),
      ∀ (n : ℕ),
        N ≤ n →
          norm.{u_1} (E := R)
                (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
                  HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R)
                    ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
              |c| ^ n <
            ε
⊢ ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        norm.{u_1} (E := R)
              (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
                HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
            |c| ^ n <
          ε

Tactic:
obtain ⟨Ng, gBound2⟩ := (hg (ε / (max a b))) (by positivity)

Premises used: HDiv.hDiv, Max.max
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
⊢ ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        norm.{u_1} (E := R)
              (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
                HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
            |c| ^ n <
          ε

Tactic:
⟨2 * max Nf Ng, fun n hn ↦ ?_⟩

Premises used: HMul.hMul, Max.max, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
refine :
  ∀ (n : ℕ) (hn : 2 * max Nf Ng ≤ n),
    norm.{u_1} (E := R)
          (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
            HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
        |c| ^ n <
      ε
⊢ ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        norm.{u_1} (E := R)
              (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
                HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
            |c| ^ n <
          ε

Tactic:
refine ⟨2 * max Nf Ng, fun n hn ↦ ?_⟩
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
n : ℕ
hn : 2 * max Nf Ng ≤ n
obtain :
  ∀ (fst snd : ℕ)
    (hi :
      (@Finset.antidiagonal _ Nat.instAddMonoid _ n).Nonempty →
        (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n)
    (ultrametric :
      norm.{u_1} (E := R)
          (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
            HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
        ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
            ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖),
    norm.{u_1} (E := R)
          (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
            HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
        |c| ^ n <
      ε
⊢ norm.{u_1} (E := R)
        (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
          HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
      |c| ^ n <
    ε

Tactic:
obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finsetSum_le (Finset.antidiagonal n)
    (fun a ↦ (coeff a.1) f * (coeff a.2) g)

Premises used: HMul.hMul, PowerSeries.coeff, Prod.fst, IsUltrametricDist.exists_norm_finsetSum_le, Prod.snd, DFunLike.coe, Finset.HasAntidiagonal.antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
n : ℕ
hn : 2 * max Nf Ng ≤ n
fst snd : ℕ
hi : (@Finset.antidiagonal _ Nat.instAddMonoid _ n).Nonempty → (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
⊢ (0, n) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
n : ℕ
hn : 2 * max Nf Ng ≤ n
fst snd : ℕ
hi : (@Finset.antidiagonal _ Nat.instAddMonoid _ n).Nonempty → (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
⊢ fst + snd = n

Tactic:
simpa using hi (⟨(0, n), by simp⟩)

Premises used: Prod.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
n : ℕ
hn : 2 * max Nf Ng ≤ n
fst snd : ℕ
hi : (@Finset.antidiagonal _ Nat.instAddMonoid _ n).Nonempty → (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
obtain :
  ∀ (hn : 2 * max Nf Ng ≤ fst + snd)
    (hi :
      (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
        (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd))
    (ultrametric :
      norm.{u_1} (E := R)
          (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
            HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
        ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
            ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖),
    norm.{u_1} (E := R)
          (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
            HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
        |c| ^ (fst + snd) <
      ε
⊢ norm.{u_1} (E := R)
        (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
          HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
      |c| ^ n <
    ε

Tactic:
obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩)

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
⊢ norm.{u_1} (E := R)
        (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
          HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
      |c| ^ (fst + snd) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) ((coeff snd : (a : R⟦X⟧) → R) g : R)‖ *
      |c| ^ (fst + snd)

Tactic:
bound
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
grw :
  norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) *
      |c| ^ (fst + snd) ≤
    norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd)
⊢ ‖HMul.hMul (α := R) (β := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) ((coeff snd : (a : R⟦X⟧) → R) g : R)‖ *
      |c| ^ (fst + snd) ≤
    norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd)

Tactic:
grw [norm_mul_le]

Premises used: norm_mul_le
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
rw :
  norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) *
      (|c| ^ fst * |c| ^ snd) ≤
    norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd)
⊢ norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) *
      |c| ^ (fst + snd) ≤
    norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd)

Tactic:
rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
⊢ norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) *
      (|c| ^ fst * |c| ^ snd) ≤
    norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd)

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
calc :
  norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
    ε
⊢ norm.{u_1} (E := R)
        (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
          HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) f : R) ((coeff p.2 : (a : R⟦X⟧) → R) g : R)) *
      |c| ^ (fst + snd) <
    ε

Tactic:
calc _ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (fst + snd) := by bound
       _ ≤ ‖(coeff fst) f‖ * |c| ^ fst * (‖(coeff snd) g‖ * |c| ^ snd) := by
        grw [norm_mul_le]
        #adaptation_note
        /--
        Broken in `nightly-2025-10-26`: this was by `grind`, but is now no longer supported.
        See https://github.com/leanprover/lean4/pull/10970.
        -/
        rw [pow_add]
        grind

Premises used: Norm.norm, HMul.hMul, abs, PowerSeries.coeff, HPow.hPow, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
⊢ max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
⊢ max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd

Tactic:
have : max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd := by lia