awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
⊢ 0 < ‖c‖ ^ (n + 1)

Tactic:
xεpos.trans hn.2

Premises used: And.right, LT.lt.trans
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
⊢ 0 < ‖c‖ ^ (n + 1)

Tactic:
exact xεpos.trans hn.2

Premises used: And.right, LT.lt.trans
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
⊢ 0 < ‖c ^ (n + 1)‖

Tactic:
have cnpos : 0 < ‖c ^ (n + 1)‖ := by rw [norm_zpow]; exact xεpos.trans hn.2
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
⟨-(n + 1), ?_, ?_, ?_, ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
refine_1 : c ^ (-(n + 1)) ≠ 0
refine_2 : (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x) < ε
refine_3 : ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x)
refine_4 : ‖c ^ (-(n + 1))‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
refine ⟨-(n + 1), ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ c ^ (-(n + 1)) ≠ 0

Tactic:
zpow_ne_zero _ (norm_pos_iff.1 cpos)

Premises used: norm_pos_iff, Iff.mp, zpow_ne_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ c ^ (-(n + 1)) ≠ 0

Tactic:
exact zpow_ne_zero _ (norm_pos_iff.1 cpos)

Premises used: norm_pos_iff, Iff.mp, zpow_ne_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
refine_2 : (p : (a : E) → ℝ) x < ‖c‖ ^ (n + 1) * ε
⊢ (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x) < ε

Tactic:
rw [map_smul_eq_mul, zpow_neg, norm_inv, ← div_eq_inv_mul, div_lt_iff₀ cnpos, mul_comm,
        norm_zpow]

Premises used: div_lt_iff₀, norm_inv, SeminormClass.map_smul_eq_mul, zpow_neg, mul_comm, norm_zpow, div_eq_inv_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ (p : (a : E) → ℝ) x < ‖c‖ ^ (n + 1) * ε

Tactic:
(div_lt_iff₀ εpos).1 (hn.2)

Premises used: div_lt_iff₀, And.right, Iff.mp
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ (p : (a : E) → ℝ) x < ‖c‖ ^ (n + 1) * ε

Tactic:
exact (div_lt_iff₀ εpos).1 (hn.2)

Premises used: div_lt_iff₀, And.right, Iff.mp
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
refine_3 : ‖c‖ ^ n * ε ≤ (p : (a : E) → ℝ) x
⊢ ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x)

Tactic:
rw [zpow_neg, div_le_iff₀ cpos, map_smul_eq_mul, norm_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos),
        zpow_one, mul_inv_rev, mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel₀ (ne_of_gt cpos),
        one_mul, ← div_eq_inv_mul, le_div_iff₀ (zpow_pos cpos _), mul_comm]

Premises used: div_le_iff₀, mul_inv_cancel₀, mul_assoc, ne_of_gt, zpow_one, norm_inv, zpow_pos, zpow_add₀, SeminormClass.map_smul_eq_mul, zpow_neg, mul_comm, norm_zpow, mul_inv_rev, div_eq_inv_mul, le_div_iff₀, one_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ‖c‖ ^ n * ε ≤ (p : (a : E) → ℝ) x

Tactic:
(le_div_iff₀ εpos).1 hn.1

Premises used: And.left, Iff.mp, le_div_iff₀
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ‖c‖ ^ n * ε ≤ (p : (a : E) → ℝ) x

Tactic:
exact (le_div_iff₀ εpos).1 hn.1

Premises used: And.left, Iff.mp, le_div_iff₀
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖

Tactic:
ring
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖

Tactic:
have : ε⁻¹ * ‖c‖ * p x = ε⁻¹ * p x * ‖c‖ := by ring
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖
refine_4 : ‖c‖ ^ n * ‖c‖ ≤ HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε * ‖c‖
⊢ ‖c ^ (-(n + 1))‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rw [zpow_neg, norm_inv, inv_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos), zpow_one, this,
        ← div_eq_inv_mul]

Premises used: ne_of_gt, zpow_one, norm_inv, zpow_add₀, inv_inv, zpow_neg, norm_zpow, div_eq_inv_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖
refine_4 : ‖c‖ ^ n ≤ HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ ‖c‖ ^ n * ‖c‖ ≤ HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε * ‖c‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖
⊢ ‖c‖ ^ n ≤ HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
hn.1

Premises used: And.left
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖
⊢ ‖c‖ ^ n ≤ HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
exact hn.1

Premises used: And.left
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (d : 𝕜),
    d ≠ 0 ∧
      (p : (a : E) → ℝ) (d • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (d • x) ∧ ‖d‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
let ⟨_, hn⟩ := p.rescale_to_shell_zpow hc εpos hx; ⟨_, hn⟩

Premises used: Norm.norm, HMul.hMul, Seminorm.rescale_to_shell_zpow, Exists, HDiv.hDiv, Ne, LE.le, And, Inv.inv, HPow.hPow, LT.lt, Exists.intro, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, _private.0.Seminorm.rescale_to_shell.match_1
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p q : Seminorm 𝕜 E
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    ε / ‖c‖ ≤ (p : (a : E) → ℝ) x →
      (p : (a : E) → ℝ) x < ε → (q : (a : E) → ℝ) x ≤ HMul.hMul (β := ℝ) C ((p : (a : E) → ℝ) x : ℝ)
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
rcases :
  ∀ (δ : 𝕜) (hδ : δ ≠ 0) (δxle : (p : (a : E) → ℝ) (δ • x) < ε) (leδx : ε / ‖c‖ ≤ (p : (a : E) → ℝ) (δ • x)),
    (q : (a : E) → ℝ) x ≤ HMul.hMul (β := ℝ) C ((p : (a : E) → ℝ) x : ℝ)
⊢ (q : (a : E) → ℝ) x ≤ HMul.hMul (β := ℝ) C ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rcases p.rescale_to_shell hc ε_pos hx with ⟨δ, hδ, δxle, leδx, -⟩

Premises used: Seminorm.rescale_to_shell
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p q : Seminorm 𝕜 E
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    ε / ‖c‖ ≤ (p : (a : E) → ℝ) x →
      (p : (a : E) → ℝ) x < ε → (q : (a : E) → ℝ) x ≤ HMul.hMul (β := ℝ) C ((p : (a : E) → ℝ) x : ℝ)
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
δ : 𝕜
hδ : δ ≠ 0
δxle : (p : (a : E) → ℝ) (δ • x) < ε
leδx : ε / ‖c‖ ≤ (p : (a : E) → ℝ) (δ • x)
⊢ (q : (a : E) → ℝ) x ≤ HMul.hMul (β := ℝ) C ((p : (a : E) → ℝ) x : ℝ)

Tactic:
simpa only [map_smul_eq_mul, mul_left_comm C, mul_le_mul_iff_right₀ (norm_pos_iff.2 hδ)]
    using hf (δ • x) leδx δxle

Premises used: Iff.mpr, norm_pos_iff, mul_left_comm, SeminormClass.map_smul_eq_mul, HSMul.hSMul, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    ε / ‖c‖ ≤ (p : (a : E) → ℝ) x →
      (p : (a : E) → ℝ) x < ε → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p : (a : E) → ℝ) x : ℝ)
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p : (a : E) → ℝ) x : ℝ)

Tactic:
Seminorm.bound_of_shell p q ε_pos hc hf hx

Premises used: Seminorm.bound_of_shell
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
hx : ∃ j ∈ s, Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
rcases :
  ∀ (j : ι) (hj : j ∈ s) (hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)),
    LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)

Tactic:
rcases hx with ⟨j, hj, hjx⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
have : (s.sup p) x ≠ 0 :=
    ne_of_gt ((hjx.symm.lt_of_le <| apply_nonneg _ _).trans_le (le_finset_sup_apply hj))
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)

Tactic:
(s.sup p).bound_of_shell_smul q ε_pos hc (fun y hle hlt ↦ ?_) this

Premises used: Seminorm.bound_of_shell_smul, Finset.sup
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
refine :
  ∀ (y : E) (hle : ε / ‖c‖ ≤ (s.sup p : (a : E) → ℝ) y) (hlt : (s.sup p : (a : E) → ℝ) y < ε),
    LE.le (α := ℝ) ((q : (a : E) → ℝ) y : ℝ) ((C • s.sup p : (a : E) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)

Tactic:
refine (s.sup p).bound_of_shell_smul q ε_pos hc (fun y hle hlt ↦ ?_) this

Premises used: Seminorm.bound_of_shell_smul, Finset.sup
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
y : E
hle : ε / ‖c‖ ≤ (s.sup p : (a : E) → ℝ) y
hlt : (s.sup p : (a : E) → ℝ) y < ε
rcases :
  ∀ (i : ι) (hi : i ∈ s) (hiy : Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) y : ℝ) ((p i : (a : E) → ℝ) y : ℝ)),
    LE.le (α := ℝ) ((q : (a : E) → ℝ) y : ℝ) ((C • s.sup p : (a : E) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) y : ℝ) ((C • s.sup p : (a : E) → ℝ) y : ℝ)

Tactic:
rcases exists_apply_eq_finset_sup p ⟨j, hj⟩ y with ⟨i, hi, hiy⟩

Premises used: Seminorm.exists_apply_eq_finset_sup, Exists.intro
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
y : E
hle : ε / ‖c‖ ≤ (s.sup p : (a : E) → ℝ) y
hlt : (s.sup p : (a : E) → ℝ) y < ε
i : ι
hi : i ∈ s
hiy : Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) y : ℝ) ((p i : (a : E) → ℝ) y : ℝ)
rw : (q : (a : E) → ℝ) y ≤ HSMul.hSMul (β := ℝ) C ((p i : (a : E) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) y : ℝ) ((C • s.sup p : (a : E) → ℝ) y : ℝ)

Tactic:
rw [smul_apply, hiy]

Premises used: Seminorm.smul_apply
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
y : E
hle : ε / ‖c‖ ≤ (s.sup p : (a : E) → ℝ) y
hlt : (s.sup p : (a : E) → ℝ) y < ε
i : ι
hi : i ∈ s
hiy : Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) y : ℝ) ((p i : (a : E) → ℝ) y : ℝ)
⊢ (q : (a : E) → ℝ) y ≤ HSMul.hSMul (β := ℝ) C ((p i : (a : E) → ℝ) y : ℝ)

Tactic:
hf y (fun k hk ↦ (le_finset_sup_apply hk).trans_lt hlt) i hi (hiy ▸ hle)

Premises used: Seminorm.le_finset_sup_apply, Eq.rec, LE.le.trans_lt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
y : E
hle : ε / ‖c‖ ≤ (s.sup p : (a : E) → ℝ) y
hlt : (s.sup p : (a : E) → ℝ) y < ε
i : ι
hi : i ∈ s
hiy : Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) y : ℝ) ((p i : (a : E) → ℝ) y : ℝ)
⊢ (q : (a : E) → ℝ) y ≤ HSMul.hSMul (β := ℝ) C ((p i : (a : E) → ℝ) y : ℝ)

Tactic:
exact hf y (fun k hk ↦ (le_finset_sup_apply hk).trans_lt hlt) i hi (hiy ▸ hle)

Premises used: Seminorm.le_finset_sup_apply, Eq.rec, LE.le.trans_lt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
rw : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
⊢ BddAbove (range p)

Tactic:
rw [Seminorm.bddAbove_range_iff]

Premises used: Seminorm.bddAbove_range_iff
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ c • x ∈ s

Tactic:
(eventually_mem_nhdsWithin.and (hs.eventually_nhdsNE_zero x)).exists

Premises used: eventually_mem_nhdsWithin, Set.Mem, setOf, Filter.Eventually.and, Absorbent.eventually_nhdsNE_zero, Filter.Eventually.exists, Set.singleton, Not
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
obtain : ∀ (c : 𝕜) (hc₀ : c ≠ 0) (hc : c • x ∈ s), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)

Tactic:
obtain ⟨c, hc₀, hc⟩ : ∃ c ≠ 0, (c : 𝕜) • x ∈ s :=
    (eventually_mem_nhdsWithin.and (hs.eventually_nhdsNE_zero x)).exists

Premises used: eventually_mem_nhdsWithin, Filter.Eventually.and, Absorbent.eventually_nhdsNE_zero, Filter.Eventually.exists