awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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)‖
⊢ ‖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)
have 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)
Tactic: grw [norm_mul_le]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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 + 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)
have 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)
Tactic: rw [pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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) <
    ε
have 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) <
  ε
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
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (hypothesis)
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) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
    ε
have this : max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd
Tactic: have : max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd := by lia
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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
⊢ 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) <
    ε
have 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) <
    ε
Tactic: rcases this with this | this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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) <
      ε
⊢ 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) <
    ε
have 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) <
    ε
Tactic: rcases this with this | this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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 *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
    ε / max a b * b
have grw : norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst * b < ε / max a b * b
Tactic: grw [gBound1 snd]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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 * b < ε / max a b * b
have hbc : norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst < ε / max a b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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 a b * b ≤ ε
have rw : b / max a b ≤ 1
Tactic: rw [div_mul_comm, mul_le_iff_le_one_left ‹_›]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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 *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
    ε
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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
⊢ 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) <
    ε
have calc₁ : ε / max a b * b ≤ ε
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
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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 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)
have grw : a * (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) < a * (ε / max a b)
Tactic: grw [fBound1 fst]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
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 * (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) < a * (ε / max a b)
have hbc : norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd < ε / max a b
Tactic: gcongr