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
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)‖
this : max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd
calc :
  ∀ (this : max Nf Ng ≤ fst),
    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) <
      ε
calc₁ :
  ∀ (this : max Nf Ng ≤ 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) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
    ε

Tactic:
rcases this with this | this
-- 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)‖
this : max Nf Ng ≤ fst
grw : norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst * b < ε / max a b * b
⊢ 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) <
    ε / max a b * b

Tactic:
grw [gBound1 snd]
-- 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)‖
this : max Nf Ng ≤ fst
hbc : norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst < ε / max a b
⊢ norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst * b < ε / max a b * b

Tactic:
gcongr
-- 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)‖
this : max Nf Ng ≤ fst
⊢ Nf ≤ fst

Tactic:
omega
-- 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)‖
this : max Nf Ng ≤ fst
⊢ norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst < ε / max a b

Tactic:
exact fBound2 fst (by omega)
-- 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)‖
this : max Nf Ng ≤ fst
rw : b / max a b ≤ 1
⊢ ε / max a b * b ≤ ε

Tactic:
rw [div_mul_comm, mul_le_iff_le_one_left ‹_›]

Premises used: div_mul_comm, mul_le_iff_le_one_left
-- 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)‖
this : max Nf Ng ≤ fst
⊢ b / max a b ≤ 1

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)‖
this : max Nf Ng ≤ fst
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) <
    ε / max a b * b
calc₁ : ε / max a b * b ≤ ε
⊢ 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:
calc _ < ε / max a b * b := by
          grw [gBound1 snd]
          gcongr
          exact fBound2 fst (by omega)
         _ ≤ ε := by
          rw [div_mul_comm, mul_le_iff_le_one_left ‹_›]
          bound

Premises used: 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
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)‖
this : max Nf Ng ≤ snd
grw : a * (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) < a * (ε / max a b)
⊢ 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) <
    a * (ε / max a b)

Tactic:
grw [fBound1 fst]
-- 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)‖
this : max Nf Ng ≤ snd
hbc : norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd < ε / max a b
⊢ a * (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) < a * (ε / max a b)

Tactic:
gcongr
-- 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)‖
this : max Nf Ng ≤ snd
⊢ Ng ≤ snd

Tactic:
omega
-- 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)‖
this : max Nf Ng ≤ snd
⊢ norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd < ε / max a b

Tactic:
exact gBound2 snd (by omega)
-- 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)‖
this : max Nf Ng ≤ snd
rw : a / max a b ≤ 1
⊢ a * (ε / max a b) ≤ ε

Tactic:
rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›]

Premises used: mul_div_left_comm, mul_le_iff_le_one_right
-- 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)‖
this : max Nf Ng ≤ snd
⊢ a / max a b ≤ 1

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)‖
this : max Nf Ng ≤ snd
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) <
    a * (ε / max a b)
calc₁ : a * (ε / max a b) ≤ ε
⊢ 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:
calc _ < a * (ε / max a b) := by
          grw [fBound1 fst]
          gcongr
          exact gBound2 snd (by omega)
         _ ≤ ε := by
          rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›]
          bound

Premises used: HDiv.hDiv, Max.max
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
⊢ (coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries = n.largeSchroder

Tactic:
simp [largeSchroderSeries]

Premises used: PowerSeries.largeSchroderSeries