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 : ℝ
f : R⟦X⟧
r : R
h : ¬r = 0
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
ε : ℝ
h_1 : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → norm (E := R) ((coeff n_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ n_1 < ε / ‖r‖
N : ℕ
hN : n ≤ N
⊢ ‖r‖ * norm (E := R) ((coeff N : (a : R⟦X⟧) → R) f : R) * |c| ^ N < ‖r‖ * (ε / ‖r‖)
have rw : ‖r‖ * (norm (E := R) ((coeff N : (a : R⟦X⟧) → R) f : R) * |c| ^ N) < ‖r‖ * (ε / ‖r‖)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
r : R
h : ¬r = 0
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
ε : ℝ
h_1 : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → norm (E := R) ((coeff n_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ n_1 < ε / ‖r‖
N : ℕ
hN : n ≤ N
⊢ norm (E := R) ((coeff N : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ N < ε
have calc : ‖r‖ * norm (E := R) ((coeff N : (a : R⟦X⟧) → R) f : R) * |c| ^ N < ‖r‖ * (ε / ‖r‖)
Tactic: calc _ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ N :=
        mul_le_mul_of_nonneg (norm_mul_le _ _) (by simp) (by simp) (by simp)
       _ < ‖r‖ * (ε / ‖r‖) := by
        rw [mul_assoc]; aesop
       _ = ε := mul_div_cancel₀ _ (by aesop)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf : IsRestricted c f
r : R
⊢ IsRestricted c (r • f)
have if : ∀ (h : r = 0), IsRestricted c (r • f)
Tactic: if h : r = 0 then simpa [h] using zero c else
  simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf
  intro ε _
  obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity)
  refine ⟨n, fun N hN ↦ ?_⟩
  calc _ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ N :=
        mul_le_mul_of_nonneg (norm_mul_le _ _) (by simp) (by simp) (by simp)
       _ < ‖r‖ * (ε / ‖r‖) := by
        rw [mul_assoc]; aesop
       _ = ε := mul_div_cancel₀ _ (by aesop)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf : IsRestricted c f
r : R
if : ∀ (h : r = 0), IsRestricted c (r • f)
⊢ IsRestricted c (r • f)
have if₁ : ∀ (h : ¬r = 0), IsRestricted c (r • f)
Tactic: if h : r = 0 then simpa [h] using zero c else
  simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf
  intro ε _
  obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity)
  refine ⟨n, fun N hN ↦ ?_⟩
  calc _ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ N :=
        mul_le_mul_of_nonneg (norm_mul_le _ _) (by simp) (by simp) (by simp)
       _ < ‖r‖ * (ε / ‖r‖) := by
        rw [mul_assoc]; aesop
       _ = ε := mul_div_cancel₀ _ (by aesop)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf : IsRestricted c f
⊢ BddAbove (convergenceSet c f)
have hf₁ : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
Tactic: simp_rw [isRestricted_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
⊢ BddAbove (convergenceSet c f)
have obtain : ∀ (N : ℕ) (hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1),
  BddAbove (convergenceSet c f)
Tactic: obtain ⟨N, hf⟩ := by simpa using (hf 1)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
⊢ ∃ (x : ℝ),
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i = x} y →
        y ≤ x
have h : ∀ (y : ℝ),
  Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i = x} y →
    y ≤ max 1 (max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) sorry)
Tactic: use max 1 (max' (image (fun i ↦ ‖coeff i f‖ * c ^ i) (range (N + 1))) (by simp))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
⊢ ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i = x} y →
      y ≤
        max 1 (max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) ⋯)
have h : ∀ (a : ℕ),
  norm (E := R) ((coeff a : (a : R⟦X⟧) → R) f : R) * c ^ a ≤ 1 ∨
    norm (E := R) ((coeff a : (a : R⟦X⟧) → R) f : R) * c ^ a ≤
      max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) sorry
Tactic: simp only [Set.mem_setOf_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
i : ℕ
⊢ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1 ∨
    norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
      max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) ⋯
have h : ∀ (h : i ≤ N),
  norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1 ∨
    norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
      max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) sorry
Tactic: rcases le_total i N with h | h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
i : ℕ
h :
  ∀ (h : i ≤ N),
    norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1 ∨
      norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
        max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) ⋯
⊢ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1 ∨
    norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
      max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) ⋯
have h₁ : ∀ (h : N ≤ i),
  norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1 ∨
    norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
      max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) sorry
Tactic: rcases le_total i N with h | h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
i : ℕ
h : i ≤ N
⊢ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1 ∨
    norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
      max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) ⋯
have h₁ : norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
  max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) sorry
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
i : ℕ
h : i ≤ N
⊢ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
    max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) ⋯
have h₁ : Membership.mem (γ := Finset ℝ)
  (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1)))
  (norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i)
Tactic: apply le_max'
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
i : ℕ
h : i ≤ N
⊢ Membership.mem (γ := Finset ℝ)
    (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1)))
    (norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i)
have h₁ : ∃ a < N + 1,
  norm (E := R) ((coeff a : (a : R⟦X⟧) → R) f : R) * c ^ a = norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i
Tactic: simp only [mem_image, mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
i : ℕ
h : N ≤ i
⊢ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1 ∨
    norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤
      max' (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1))) ⋯
have h₁ : norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
i : ℕ
h : N ≤ i
⊢ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1
have calc : norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * |c ^ i|
Tactic: calc _ ≤ ‖(coeff i) f‖ * |c ^ i| := by bound
         _ ≤ 1 := by simpa using (hf i h).le
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf_1 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε
N : ℕ
hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1
i : ℕ
h : N ≤ i
calc :
  norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * |c ^ i|
⊢ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i ≤ 1
have calc₁ : norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * |c ^ i| ≤ 1
Tactic: calc _ ≤ ‖(coeff i) f‖ * |c ^ i| := by bound
         _ ≤ 1 := by simpa using (hf i h).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⟧
hf : IsRestricted c f
hg : IsRestricted c g
⊢ IsRestricted c (f * g)
have obtain : ∀ (a : ℝ) (ha : 1 ≤ a) (fBound1 : ∀ y ∈ convergenceSet |c| f, y ≤ a), IsRestricted c (f * g)
Tactic: obtain ⟨a, ha, fBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _
    ((isRestricted_iff_abs c f).mp hf))
-- 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⟧
hf : IsRestricted c f
hg : IsRestricted c g
a : ℝ
ha : 1 ≤ a
fBound1 : ∀ y ∈ convergenceSet |c| f, y ≤ a
⊢ IsRestricted c (f * g)
have obtain : ∀ (b : ℝ) (hb : 1 ≤ b) (gBound1 : ∀ y ∈ convergenceSet |c| g, y ≤ b), IsRestricted c (f * g)
Tactic: obtain ⟨b, hb, gBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _
    ((isRestricted_iff_abs c g).mp hg))
-- 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⟧
hf : IsRestricted c f
hg : IsRestricted c g
a : ℝ
ha : 1 ≤ a
fBound1 : ∀ y ∈ convergenceSet |c| f, y ≤ a
b : ℝ
hb : 1 ≤ b
gBound1 : ∀ y ∈ convergenceSet |c| g, y ≤ b
⊢ IsRestricted c (f * g)
have fBound1₁ : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
Tactic: simp only [convergenceSet, Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff]
    at fBound1 gBound1
Cleared hypotheses: fBound1, gBound1
-- 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⟧
hf : IsRestricted c f
hg : IsRestricted c g
a : ℝ
ha : 1 ≤ a
fBound1 : ∀ y ∈ convergenceSet |c| f, y ≤ a
b : ℝ
hb : 1 ≤ b
gBound1 : ∀ y ∈ convergenceSet |c| g, y ≤ b
fBound1₁ : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
⊢ IsRestricted c (f * g)
have gBound1₁ : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
Tactic: simp only [convergenceSet, Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff]
    at fBound1 gBound1
Cleared hypotheses: fBound1, gBound1
-- 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⟧
hf : IsRestricted c f
hg : IsRestricted c g
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
⊢ IsRestricted c (f * g)
have simp : ∀ (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 < ε)
  (ε : ℝ),
  0 < ε →
    ∃ (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: simp only [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm,
    PowerSeries.coeff_mul] at ⊢ hf hg
Cleared hypotheses: hf, hg
-- 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 < ε
⊢ ∃ (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 <
          ε
have obtain : ∀ (Nf : ℕ) (fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : 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: obtain ⟨Nf, fBound2⟩ := (hf (ε / (max a b))) (by positivity)
-- 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
⊢ ∃ (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 <
          ε
have 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 <
          ε
Tactic: obtain ⟨Ng, gBound2⟩ := (hg (ε / (max a b))) (by positivity)
-- 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
⊢ ∃ (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 <
          ε
have 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 <
    ε
Tactic: refine ⟨2 * max Nf Ng, fun n hn ↦ ?_⟩
-- 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
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 <
    ε
have 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 <
    ε
Tactic: obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finsetSum_le (Finset.antidiagonal n)
    (fun a ↦ (coeff a.1) f * (coeff a.2) g)
-- 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
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)‖
⊢ 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 <
    ε
have 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) <
    ε
Tactic: obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩)
Cleared hypotheses: n, hn, hi, ultrametric