awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
rw : Eq (α := Set E) {y : E | (p : (a : E) → ℝ) y ≤ r} (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r))
rw₁ rw₂ : Eq.{u_7 + 1} (α := Set E) {y : E | (p : (a : E) → ℝ) y ≤ r} {x : E | (p : (a : E) → ℝ) x ≤ r}
⊢ p.closedBall 0 r = preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r)

Tactic:
rw [closedBall_zero_eq, preimage_metric_closedBall]

Premises used: Seminorm.preimage_metric_closedBall, Seminorm.closedBall_zero_eq
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ ball.{u_3, u_7} (𝕜 := 𝕜) ⊥ x r = univ

Tactic:
ball_zero' x hr

Premises used: Seminorm.ball_zero'
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ closedBall.{u_3, u_7} (𝕜 := 𝕜) ⊥ x r = univ

Tactic:
closedBall_zero' x hr

Premises used: Seminorm.closedBall_zero'
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun (x : E) ↦ a • x) y = x
rw : HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) < r
⊢ x ∈ p.ball 0 r

Tactic:
rw [mem_ball_zero, ← hx, map_smul_eq_mul]

Premises used: Seminorm.mem_ball_zero, SeminormClass.map_smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun (x : E) ↦ a • x) y = x
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) ≤ (p : (a : E) → ℝ) y

Tactic:
mul_le_of_le_one_left (apply_nonneg p _) ha

Premises used: mul_le_of_le_one_left, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun (x : E) ↦ a • x) y = x
rwa rwa₁ rwa₂ rwa₃ : ∀ (hy : (p : (a : E) → ℝ) y < r) (hx : (fun (x : E) ↦ a • x) y = x), (p : (a : E) → ℝ) y < r
⊢ (p : (a : E) → ℝ) y < r

Tactic:
rwa [mem_ball_zero] at hy

Premises used: Seminorm.mem_ball_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun (x : E) ↦ a • x) y = x
_ : (p : (a : E) → ℝ) y < r
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) < r

Tactic:
calc
    _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
    _ < r := by rwa [mem_ball_zero] at hy

Premises used: mul_le_of_le_one_left, NonnegHomClass.apply_nonneg, DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun (x : E) ↦ a • x) y = x
rw : HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) ≤ r
⊢ x ∈ p.closedBall 0 r

Tactic:
rw [mem_closedBall_zero, ← hx, map_smul_eq_mul]

Premises used: Seminorm.mem_closedBall_zero, SeminormClass.map_smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun (x : E) ↦ a • x) y = x
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) ≤ (p : (a : E) → ℝ) y

Tactic:
mul_le_of_le_one_left (apply_nonneg p _) ha

Premises used: mul_le_of_le_one_left, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun (x : E) ↦ a • x) y = x
rwa rwa₁ rwa₂ rwa₃ : ∀ (hy : (p : (a : E) → ℝ) y ≤ r) (hx : (fun (x : E) ↦ a • x) y = x), (p : (a : E) → ℝ) y ≤ r
⊢ (p : (a : E) → ℝ) y ≤ r

Tactic:
rwa [mem_closedBall_zero] at hy

Premises used: Seminorm.mem_closedBall_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun (x : E) ↦ a • x) y = x
_ : (p : (a : E) → ℝ) y ≤ r
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) ≤ r

Tactic:
calc
    _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
    _ ≤ r := by rwa [mem_closedBall_zero] at hy

Premises used: mul_le_of_le_one_left, NonnegHomClass.apply_nonneg, DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ 0 ≤ r

Tactic:
hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
lift : ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)), (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)
⊢ (s.sup p).ball x r = ⋂ i ∈ s, (p i).ball x r

Tactic:
lift r to NNReal using hr.le

Premises used: LT.lt.le, NNReal
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < (↑r : ℝ)
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) < (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) : ℝ) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₃ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) < r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₄ :
  Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) (y - x)) ⋯ < r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₅ :
  Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, (↑(NNReal.mk ((p b : (a : E) → ℝ) (y - x)) ⋯) : ℝ) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
⊢ (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)

Tactic:
simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
    Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, NNReal.coe_mk]

Premises used: Seminorm.finset_sup_apply, NNReal.coe_mk, Finset.sup_lt_iff, Seminorm.ball, Set.iInter_setOf, NNReal.coe_lt_coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r

Tactic:
hr
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
lift : ∀ (r : ℝ≥0), (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)
⊢ (s.sup p).closedBall x r = ⋂ i ∈ s, (p i).closedBall x r

Tactic:
lift r to NNReal using hr

Premises used: NNReal
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) : ℝ) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₃ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) ≤ r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₄ :
  Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) (y - x)) ⋯ ≤ r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₅ :
  Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, (↑(NNReal.mk ((p b : (a : E) → ℝ) (y - x)) ⋯) : ℝ) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
⊢ (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)

Tactic:
simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
    NNReal.coe_le_coe, NNReal.coe_mk]

Premises used: Seminorm.finset_sup_apply, NNReal.coe_mk, Seminorm.closedBall, Set.iInter_setOf, Finset.sup_le_iff, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
rw : (s.sup p).ball x r = ⨅ a ∈ s, (p a).ball x r
⊢ (s.sup p).ball x r = s.inf fun (i : ι) ↦ (p i).ball x r

Tactic:
rw [Finset.inf_eq_iInf]

Premises used: Finset.inf_eq_iInf
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = ⨅ a ∈ s, (p a).ball x r

Tactic:
ball_finset_sup_eq_iInter _ _ _ hr

Premises used: Set.iInter, Seminorm.ball_finset_sup_eq_iInter
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = ⨅ a ∈ s, (p a).ball x r

Tactic:
exact ball_finset_sup_eq_iInter _ _ _ hr

Premises used: Seminorm.ball_finset_sup_eq_iInter
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
rw : (s.sup p).closedBall x r = ⨅ a ∈ s, (p a).closedBall x r
⊢ (s.sup p).closedBall x r = s.inf fun (i : ι) ↦ (p i).closedBall x r

Tactic:
rw [Finset.inf_eq_iInf]

Premises used: Finset.inf_eq_iInf
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = ⨅ a ∈ s, (p a).closedBall x r

Tactic:
closedBall_finset_sup_eq_iInter _ _ _ hr

Premises used: Set.iInter, Seminorm.closedBall_finset_sup_eq_iInter
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = ⨅ a ∈ s, (p a).closedBall x r

Tactic:
exact closedBall_finset_sup_eq_iInter _ _ _ hr

Premises used: Seminorm.closedBall_finset_sup_eq_iInter
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
h : ∀ (x_1 : E), x_1 ∈ p.ball x r ↔ Membership.mem (γ := Set E) ∅ x_1
⊢ p.ball x r = ∅

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x_1 : E
h : r ≤ (p : (a : E) → ℝ) (x_1 - x)
⊢ x_1 ∈ p.ball x r ↔ Membership.mem (γ := Set E) ∅ x_1

Tactic:
rw [Seminorm.mem_ball, Set.mem_empty_iff_false, iff_false, not_lt]

Premises used: iff_false, not_lt, Seminorm.mem_ball, Set.mem_empty_iff_false
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x_1 : E
⊢ r ≤ (p : (a : E) → ℝ) (x_1 - x)

Tactic:
hr.trans (apply_nonneg p _)

Premises used: LE.le.trans, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x_1 : E
⊢ r ≤ (p : (a : E) → ℝ) (x_1 - x)

Tactic:
exact hr.trans (apply_nonneg p _)

Premises used: LE.le.trans, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
h : ∀ (x_1 : E), x_1 ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) ∅ x_1
⊢ p.closedBall x r = ∅

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x_1 : E
h : r < (p : (a : E) → ℝ) (x_1 - x)
⊢ x_1 ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) ∅ x_1

Tactic:
rw [Seminorm.mem_closedBall, Set.mem_empty_iff_false, iff_false, not_le]

Premises used: not_le, iff_false, Set.mem_empty_iff_false, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x_1 : E
⊢ r < (p : (a : E) → ℝ) (x_1 - x)

Tactic:
hr.trans_le (apply_nonneg _ _)

Premises used: LT.lt.trans_le, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x_1 : E
⊢ r < (p : (a : E) → ℝ) (x_1 - x)

Tactic:
exact hr.trans_le (apply_nonneg _ _)

Premises used: LT.lt.trans_le, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
simp :
  ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), (p : (a : E) → ℝ) b < r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.closedBall 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul]

Premises used: Seminorm.mem_ball_zero, Set.smul_subset_iff, SeminormClass.map_smul_eq_mul, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), (p : (a : E) → ℝ) b < r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂

Tactic:
fun a ha b hb ↦ mul_lt_mul' ha hb (apply_nonneg _ _) ?_

Premises used: mul_lt_mul', NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
refine : ∀ (a : 𝕜) (ha : ‖a‖ ≤ r₁) (b : E) (hb : (p : (a : E) → ℝ) b < r₂), 0 < r₁
⊢ ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), (p : (a : E) → ℝ) b < r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂

Tactic:
refine fun a ha b hb ↦ mul_lt_mul' ha hb (apply_nonneg _ _) ?_

Premises used: mul_lt_mul', NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : (p : (a : E) → ℝ) b < r₂
⊢ 0 < r₁

Tactic:
hr₁.lt_or_gt.resolve_left <| ((norm_nonneg a).trans ha).not_gt

Premises used: Or.resolve_left, LE.le.not_gt, LE.le.trans, norm_nonneg, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : (p : (a : E) → ℝ) b < r₂
⊢ 0 < r₁

Tactic:
exact hr₁.lt_or_gt.resolve_left <| ((norm_nonneg a).trans ha).not_gt

Premises used: Or.resolve_left, LE.le.not_gt, LE.le.trans, norm_nonneg, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
simp :
  ∀ (a : 𝕜), ‖a‖ < r₁ → ∀ (b : E), (p : (a : E) → ℝ) b ≤ r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.closedBall 0 r₂) ⊆ p.ball 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff,
    map_smul_eq_mul]

Premises used: Seminorm.mem_ball_zero, Seminorm.mem_closedBall_zero, Set.smul_subset_iff, SeminormClass.map_smul_eq_mul, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
rw : HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) b : ℝ) ‖a‖ < r₂ * r₁
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂

Tactic:
rw [mul_comm, mul_comm r₁]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
⊢ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) b : ℝ) ‖a‖ < r₂ * r₁

Tactic:
mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_gt.resolve_left ?_)

Premises used: Or.resolve_left, mul_lt_mul', norm_nonneg, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
refine : ¬r₂ < 0
⊢ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) b : ℝ) ‖a‖ < r₂ * r₁

Tactic:
refine mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_gt.resolve_left ?_)

Premises used: Or.resolve_left, mul_lt_mul', norm_nonneg, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
⊢ ¬r₂ < 0

Tactic:
((apply_nonneg p b).trans hb).not_gt

Premises used: LE.le.not_gt, LE.le.trans, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
⊢ ¬r₂ < 0

Tactic:
exact ((apply_nonneg p b).trans hb).not_gt

Premises used: LE.le.not_gt, LE.le.trans, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
inl : HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 0) ⊆ p.ball 0 (r₁ * 0)
inr : ∀ (hr₂ : r₂ ≠ 0), HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)

Tactic:
rcases eq_or_ne r₂ 0 with rfl | hr₂

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 0) ⊆ p.ball 0 (r₁ * 0)

Tactic:
simp
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)

Tactic:
(smul_subset_smul_left (ball_subset_closedBall _ _ _)).trans
      (ball_smul_closedBall _ _ hr₂)

Premises used: Seminorm.ball_smul_closedBall, Set.smul_subset_smul_left, HasSubset.Subset.trans, Seminorm.ball_subset_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)

Tactic:
exact (smul_subset_smul_left (ball_subset_closedBall _ _ _)).trans
      (ball_smul_closedBall _ _ hr₂)

Premises used: Seminorm.ball_smul_closedBall, Set.smul_subset_smul_left, HasSubset.Subset.trans, Seminorm.ball_subset_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
simp :
  ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), (p : (a : E) → ℝ) b ≤ r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) ≤ r₁ * r₂
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.closedBall 0 r₁) (p.closedBall 0 r₂) ⊆ p.closedBall 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_closedBall_zero, mem_closedBall_zero_iff, map_smul_eq_mul]

Premises used: Seminorm.mem_closedBall_zero, Set.smul_subset_iff, SeminormClass.map_smul_eq_mul, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
b0 : 0 ≤ r₁
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) ≤ r₁ * r₂

Tactic:
gcongr
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
⊢ 0 ≤ r₁

Tactic:
(norm_nonneg _).trans ha

Premises used: LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
⊢ 0 ≤ r₁

Tactic:
exact (norm_nonneg _).trans ha

Premises used: LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -x ∈ p.ball 0 r ↔ x ∈ p.ball 0 r

Tactic:
simp only [mem_ball_zero, map_neg_eq_map]

Premises used: Seminorm.mem_ball_zero, AddGroupSeminormClass.map_neg_eq_map
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -x ∈ p.closedBall 0 r ↔ x ∈ p.closedBall 0 r

Tactic:
simp only [mem_closedBall_zero, map_neg_eq_map]

Premises used: Seminorm.mem_closedBall_zero, AddGroupSeminormClass.map_neg_eq_map
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
h : ∀ (x_1 : E), x_1 ∈ -p.ball x r ↔ x_1 ∈ p.ball (-x) r
⊢ -p.ball x r = p.ball (-x) r

Tactic:
ext