awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 < ε
obtain :
  ∀ (n : ℕ) (hn : ∀ (n_1 : ℕ), n ≤ n_1 → norm (E := R) ((coeff n_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ n_1 < ε / ‖r‖),
    ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ n < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ n < ε

Tactic:
obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity)

Premises used: Norm.norm, HDiv.hDiv
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ n < ε

Tactic:
⟨n, fun N hN ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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‖
refine : ∀ (N : ℕ) (hN : n ≤ N), norm (E := R) ((coeff N : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ N < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ n < ε

Tactic:
refine ⟨n, fun N hN ↦ ?_⟩
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ |c| ^ N ≤ |c| ^ N

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ 0 ≤ ‖HMul.hMul (β := R) r ((coeff N : (a : R⟦X⟧) → R) f : R)‖

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ 0 ≤ |c| ^ N

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
rw : ‖r‖ * (norm (E := R) ((coeff N : (a : R⟦X⟧) → R) f : R) * |c| ^ N) < ‖r‖ * (ε / ‖r‖)
⊢ ‖r‖ * norm (E := R) ((coeff N : (a : R⟦X⟧) → R) f : R) * |c| ^ N < ‖r‖ * (ε / ‖r‖)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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‖)

Tactic:
aesop
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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‖ ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
calc : ‖r‖ * norm (E := R) ((coeff N : (a : R⟦X⟧) → R) f : R) * |c| ^ N < ‖r‖ * (ε / ‖r‖)
⊢ norm (E := R) ((coeff N : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ N < ε

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)

Premises used: Norm.norm, mul_le_mul_of_nonneg, HDiv.hDiv, PowerSeries.coeff, mul_div_cancel₀, norm_mul_le, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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)
if₁ : ∀ (h : ¬r = 0), IsRestricted c (r • f)
if₂ : ∀ (h : r = 0), IsRestricted c (r • f)
if₃ if₄ : ∀ (h : ¬r = 0), IsRestricted c (r • f)
⊢ 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)

Premises used: norm_pow, mul_le_mul_of_nonneg, PowerSeries.IsRestricted.isRestricted_iff, norm_mul, mul_div_cancel₀, abs_norm, norm_mul_le, Real.norm_eq_abs, PowerSeries.IsRestricted.zero
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf : IsRestricted c f
⊢ ∀ (ε : ℝ), 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

Premises used: PowerSeries.IsRestricted.isRestricted_iff
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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‖ < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1

Tactic:
simpa using (hf 1)

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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‖ < ε
obtain :
  ∀ (N : ℕ) (hf : ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < 1),
    BddAbove (convergenceSet c f)
⊢ BddAbove (convergenceSet c f)

Tactic:
obtain ⟨N, hf⟩ := by simpa using (hf 1)
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ Finset.Nonempty (α := ℝ)
    (image (fun (i : ℕ) ↦ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i) (range (N + 1)))

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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))) ⋯)
⊢ ∃ (x : ℝ),
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (i : ℕ), norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * c ^ i = x} y →
        y ≤ x

Tactic:
use max 1 (max' (image (fun i ↦ ‖coeff i f‖ * c ^ i) (range (N + 1))) (by simp))

Premises used: Norm.norm, HMul.hMul, Finset.max', PowerSeries.coeff, Finset.range, HPow.hPow, HAdd.hAdd, Max.max, OfNat.ofNat, DFunLike.coe, Finset.image
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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))) ⋯
⊢ ∀ (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))) ⋯)

Tactic:
simp only [Set.mem_setOf_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: forall_exists_index, Set.mem_setOf_eq, le_sup_iff, forall_apply_eq_imp_iff
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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))) ⋯
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))) ⋯
⊢ 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))) ⋯

Tactic:
rcases le_total i N with h | h

Premises used: le_total
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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))) ⋯
⊢ 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))) ⋯

Tactic:
right
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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)
⊢ 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))) ⋯

Tactic:
apply le_max'

Premises used: Finset.le_max'
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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
⊢ 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:
simp only [mem_image, mem_range]

Premises used: Finset.mem_image, Finset.mem_range
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ i < N + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ ∃ 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:
exact ⟨i, by lia, rfl⟩
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
h₁ : 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 ≤ 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))) ⋯

Tactic:
left
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 ≤ norm (E := R) ((coeff i : (a : R⟦X⟧) → R) f : R) * |c ^ i|

Tactic:
bound
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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

Tactic:
simpa using (hf i h).le

Premises used: LT.lt.le
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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|
calc₁ : 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 ≤ 1

Tactic:
calc _ ≤ ‖(coeff i) f‖ * |c ^ i| := by bound
         _ ≤ 1 := by simpa using (hf i h).le

Premises used: PowerSeries.coeff, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
obtain : ∀ (a : ℝ) (ha : 1 ≤ a) (fBound1 : ∀ y ∈ convergenceSet |c| f, y ≤ a), IsRestricted c (f * g)
⊢ IsRestricted c (f * g)

Tactic:
obtain ⟨a, ha, fBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _
    ((isRestricted_iff_abs c f).mp hf))

Premises used: bddAbove_iff_exists_ge, PowerSeries.IsRestricted.convergenceSet_BddAbove, Iff.mp, OfNat.ofNat, PowerSeries.IsRestricted.isRestricted_iff_abs
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
obtain : ∀ (b : ℝ) (hb : 1 ≤ b) (gBound1 : ∀ y ∈ convergenceSet |c| g, y ≤ b), IsRestricted c (f * g)
⊢ IsRestricted c (f * g)

Tactic:
obtain ⟨b, hb, gBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _
    ((isRestricted_iff_abs c g).mp hg))

Premises used: bddAbove_iff_exists_ge, PowerSeries.IsRestricted.convergenceSet_BddAbove, Iff.mp, OfNat.ofNat, PowerSeries.IsRestricted.isRestricted_iff_abs
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ ∀ (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

Premises used: forall_exists_index, Set.mem_setOf_eq, PowerSeries.IsRestricted.convergenceSet, forall_apply_eq_imp_iff
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ ∀ (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

Premises used: forall_exists_index, Set.mem_setOf_eq, PowerSeries.IsRestricted.convergenceSet, forall_apply_eq_imp_iff
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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 <
              ε
⊢ IsRestricted c (f * g)

Tactic:
simp only [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm,
    PowerSeries.coeff_mul] at ⊢ hf hg

Premises used: norm_pow, PowerSeries.IsRestricted.isRestricted_iff, norm_mul, PowerSeries.coeff_mul, abs_norm, Real.norm_eq_abs
-- 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 < ε
⊢ 0 < ε / max a b

Tactic:
positivity
-- 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 < ε
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 <
            ε
⊢ ∃ (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)

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
⊢ 0 < ε / max a b

Tactic:
positivity