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
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) < r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) < r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ < r
rw₄ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) < r
rw₅ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • (x - a⁻¹ • y)) < r
rw₆ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • x - a • a⁻¹ • y) < r
rw₇ rw₈ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • x - y) < r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)

Tactic:
rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]

Premises used: Iff.mpr, norm_pos_iff, lt_div_iff₀, smul_inv_smul₀, smul_sub, SeminormClass.map_smul_eq_mul, Seminorm.mem_ball, mul_comm, Set.mem_preimage
-- 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
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) ≤ r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ ≤ r
rw₄ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ≤ r
rw₅ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • (x - a⁻¹ • y)) ≤ r
rw₆ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • x - a • a⁻¹ • y) ≤ r
rw₇ rw₈ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • x - y) ≤ r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)

Tactic:
rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]

Premises used: Iff.mpr, norm_pos_iff, smul_inv_smul₀, smul_sub, SeminormClass.map_smul_eq_mul, mul_comm, le_div_iff₀, Seminorm.mem_closedBall, Set.mem_preimage
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
⊢ ConvexOn ℝ (E := E) (β := ℝ) univ (⇑p : (a : E) → ℝ)

Tactic:
⟨convex_univ, fun x _ y _ a b ha hb _ => ?_⟩

Premises used: convex_univ, And.intro, ConvexOn
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
refine :
  ∀ (x : E),
    Membership.mem (γ := Set E) univ x →
      ∀ (y : E),
        Membership.mem (γ := Set E) univ y →
          ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b),
            a + b = 1 →
              (p : (a : E) → ℝ) (a • x + b • y) ≤
                HSMul.hSMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HSMul.hSMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
⊢ ConvexOn ℝ (E := E) (β := ℝ) univ (⇑p : (a : E) → ℝ)

Tactic:
refine ⟨convex_univ, fun x _ y _ a b ha hb _ => ?_⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
⊢ (p : (a : E) → ℝ) (a • x + b • y) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ)

Tactic:
map_add_le_add p _ _

Premises used: SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
      (HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ))
rw₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
      ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) b 1 • y) : ℝ)
rw₂ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) b 1 • y) : ℝ)
rw₃ rw₄ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ)

Tactic:
rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]

Premises used: smul_one_smul, SeminormClass.map_smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₁ :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) (‖b‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₂ :
  HMul.hMul (β := ℝ) (‖a‖ * 1) ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₃ :
  HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₄ :
  HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) ‖b‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₅ :
  HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) ‖b‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₆ rw₇ :
  HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
⊢ HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)

Tactic:
rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]

Premises used: norm_smul, NormOneClass.norm_one, mul_one, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
p₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ)
p₂ :
  HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
⊢ (p : (a : E) → ℝ) (a • x + b • y) ≤
    HSMul.hSMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HSMul.hSMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)

Tactic:
calc
    p (a • x + b • y) ≤ p (a • x) + p (b • y) := map_add_le_add p _ _
    _ = ‖a • (1 : 𝕜)‖ * p x + ‖b • (1 : 𝕜)‖ * p y := by
      rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
    _ = a * p x + b * p y := by
      rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]

Premises used: HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, SubadditiveHomClass.map_add_le_add, DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex.{0, u_7} ℝ (E := E)
    {x_1 : E |
      Membership.mem (γ := Set E) (preimage (β := E) (fun (z : E) ↦ -x + z) univ) x_1 ∧
        Function.comp (β := E) (⇑p : (a : E) → ℝ) (fun (z : E) ↦ z + -x) x_1 < r}

Tactic:
(p.convexOn.translate_left (-x)).convex_lt r

Premises used: Seminorm.convexOn, ConvexOn.translate_left, ConvexOn.convex_lt, Neg.neg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
h :
  p.ball x r =
    {x_1 : E |
      Membership.mem (γ := Set E) (preimage (β := E) (fun (z : E) ↦ -x + z) univ) x_1 ∧
        Function.comp (β := E) (⇑p : (a : E) → ℝ) (fun (z : E) ↦ z + -x) x_1 < r}
⊢ Convex ℝ (p.ball x r)

Tactic:
convert! (p.convexOn.translate_left (-x)).convex_lt r

Premises used: Seminorm.convexOn, ConvexOn.translate_left, ConvexOn.convex_lt, Neg.neg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
h :
  ∀ (y : E),
    y ∈ p.ball x r ↔
      Membership.mem (γ := Set E)
        {x_1 : E |
          Membership.mem (γ := Set E) (preimage (β := E) (fun (z : E) ↦ -x + z) univ) x_1 ∧
            Function.comp (β := E) (⇑p : (a : E) → ℝ) (fun (z : E) ↦ z + -x) x_1 < r}
        y
⊢ p.ball x r =
    {x_1 : E |
      Membership.mem (γ := Set E) (preimage (β := E) (fun (z : E) ↦ -x + z) univ) x_1 ∧
        Function.comp (β := E) (⇑p : (a : E) → ℝ) (fun (z : E) ↦ z + -x) x_1 < r}

Tactic:
ext y
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
h :
  (p : (a : E) → ℝ) (y + -x) < r ↔
    Membership.mem (γ := Set E) {x_1 : E | Function.comp (β := E) (⇑p : (a : E) → ℝ) (fun (z : E) ↦ z + -x) x_1 < r} y
⊢ y ∈ p.ball x r ↔
    Membership.mem (γ := Set E)
      {x_1 : E |
        Membership.mem (γ := Set E) (preimage (β := E) (fun (z : E) ↦ -x + z) univ) x_1 ∧
          Function.comp (β := E) (⇑p : (a : E) → ℝ) (fun (z : E) ↦ z + -x) x_1 < r}
      y

Tactic:
rw [preimage_univ, sep_univ, p.mem_ball, sub_eq_add_neg]

Premises used: Set.sep_univ, sub_eq_add_neg, Seminorm.mem_ball, Set.preimage_univ
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ (p : (a : E) → ℝ) (y + -x) < r ↔
    Membership.mem (γ := Set E) {x_1 : E | Function.comp (β := E) (⇑p : (a : E) → ℝ) (fun (z : E) ↦ z + -x) x_1 < r} y

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
rw : Convex.{0, u_7} ℝ (E := E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ)
⊢ Convex ℝ (p.closedBall x r)

Tactic:
rw [closedBall_eq_biInter_ball]

Premises used: Seminorm.closedBall_eq_biInter_ball
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex.{0, u_7} ℝ (E := E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ)

Tactic:
convex_iInter₂ fun _ _ => convex_ball _ _ _

Premises used: Seminorm.convex_ball, convex_iInter₂
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex.{0, u_7} ℝ (E := E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ)

Tactic:
exact convex_iInter₂ fun _ _ => convex_ball _ _ _

Premises used: Seminorm.convex_ball, convex_iInter₂
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
𝕜' : Type u_12
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
inst_4 : AddCommGroup E
inst_5 : Module 𝕜' E
inst_6 : SMul 𝕜 E
inst_7 : IsScalarTower 𝕜 𝕜' E
p : Seminorm 𝕜' E
a : 𝕜
x : E
rw : p.toFun (HSMul.hSMul (β := 𝕜') a 1 • x) = ‖a‖ * p.toFun x
rw₁ : ‖HSMul.hSMul (β := 𝕜') a 1‖ * p.toFun x = ‖a‖ * p.toFun x
rw₂ : ‖a‖ * norm.{u_12} (E := 𝕜') 1 * p.toFun x = ‖a‖ * p.toFun x
rw₃ : ‖a‖ * 1 * p.toFun x = ‖a‖ * p.toFun x
rw₄ rw₅ : ‖a‖ * p.toFun x = ‖a‖ * p.toFun x
⊢ p.toFun (a • x) = ‖a‖ * p.toFun x

Tactic:
rw [← smul_one_smul 𝕜' a x, p.smul', norm_smul, norm_one, mul_one]

Premises used: norm_smul, NormOneClass.norm_one, Seminorm.smul', smul_one_smul, mul_one
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
𝕜' : Type u_12
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
inst_4 : AddCommGroup E
inst_5 : Module 𝕜' E
inst_6 : SMul 𝕜 E
inst_7 : IsScalarTower 𝕜 𝕜' E
p : Seminorm 𝕜' E
⊢ Eq (α := (a : E) → ℝ) (⇑(Seminorm.restrictScalars 𝕜 p) : (a : E) → ℝ) (⇑p : (a : E) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
𝕜' : Type u_12
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
inst_4 : AddCommGroup E
inst_5 : Module 𝕜' E
inst_6 : SMul 𝕜 E
inst_7 : IsScalarTower 𝕜 𝕜' E
p : Seminorm 𝕜' E
⊢ ball (Seminorm.restrictScalars 𝕜 p) = p.ball

Tactic:
rfl

Premises used: Seminorm.restrictScalars, setOf, Seminorm.ball, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
𝕜' : Type u_12
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
inst_4 : AddCommGroup E
inst_5 : Module 𝕜' E
inst_6 : SMul 𝕜 E
inst_7 : IsScalarTower 𝕜 𝕜' E
p : Seminorm 𝕜' E
⊢ closedBall (Seminorm.restrictScalars 𝕜 p) = p.closedBall

Tactic:
rfl

Premises used: Seminorm.restrictScalars, setOf, Seminorm.closedBall, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
⊢ ∀ r > 0, Membership.mem (γ := Filter E) (𝓝 0) (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r))

Tactic:
simp_rw [Seminorm.closedBall_zero_eq_preimage_closedBall] at hp

Premises used: Seminorm.closedBall_zero_eq_preimage_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, Membership.mem (γ := Filter E) (𝓝 0) (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r))
rwa : Tendsto (α := E) (β := ℝ) ((⇑p : (a : E) → ℝ) : (a : E) → ℝ) (𝓝 0) (𝓝 ((p : (a : E) → ℝ) 0) : Filter ℝ)
rwa₁ :
  ∀ (i : ℝ),
    0 < i →
      ∀ᶠ (x : E) in 𝓝 0,
        Membership.mem (α := ℝ) (γ := Set ℝ) (Metric.closedBall ((p : (a : E) → ℝ) 0) i : Set ℝ)
          ((p : (a : E) → ℝ) x : ℝ)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (i : ℝ),
    0 < i → ∀ᶠ (x : E) in 𝓝 0, Membership.mem (α := ℝ) (γ := Set ℝ) (Metric.closedBall 0 i) ((p : (a : E) → ℝ) x : ℝ)
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0

Tactic:
rwa [ContinuousAt, Metric.nhds_basis_closedBall.tendsto_right_iff, map_zero]

Premises used: ContinuousAt, map_zero, Filter.HasBasis.tendsto_right_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0

Tactic:
continuousAt_zero_of_forall' fun ε hε ↦ ?_

Premises used: Seminorm.continuousAt_zero_of_forall'
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
refine : ∀ (ε : ℝ) (hε : ε > 0), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 ε)
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0

Tactic:
refine continuousAt_zero_of_forall' fun ε hε ↦ ?_

Premises used: Seminorm.continuousAt_zero_of_forall'
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
ε : ℝ
hε : ε > 0
inl : ∀ (hr : r ≤ 0), ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε
inr : ∀ (hr : 0 < r), ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε
⊢ ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε

Tactic:
rcases le_or_gt r 0 with hr | hr

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
ε : ℝ
hε : ε > 0
hr : r ≤ 0
h : 0 < norm.{u_3} (E := 𝕜) 1 ∧ norm.{u_3} (E := 𝕜) 1 * r < ε
⊢ ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε

Tactic:
use 1
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
ε : ℝ
hε : ε > 0
hr : r ≤ 0
⊢ 0 < norm.{u_3} (E := 𝕜) 1 ∧ norm.{u_3} (E := 𝕜) 1 * r < ε

Tactic:
simpa using hr.trans_lt hε

Premises used: 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
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
ε : ℝ
hε : ε > 0
hr : 0 < r
⊢ ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε

Tactic:
simpa [lt_div_iff₀ hr] using exists_norm_lt 𝕜 (div_pos hε hr)

Premises used: lt_div_iff₀, div_pos, NormedField.exists_norm_lt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
ε : ℝ
hε : ε > 0
obtain : ∀ (k : 𝕜) (hk₀ : 0 < ‖k‖) (hk : ‖k‖ * r < ε), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 ε)
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 ε)

Tactic:
obtain ⟨k, hk₀, hk⟩ : ∃ k : 𝕜, 0 < ‖k‖ ∧ ‖k‖ * r < ε := by
    rcases le_or_gt r 0 with hr | hr
    · use 1; simpa using hr.trans_lt hε
    · simpa [lt_div_iff₀ hr] using exists_norm_lt 𝕜 (div_pos hε hr)
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
ε : ℝ
hε : ε > 0
k : 𝕜
hk₀ : 0 < ‖k‖
hk : ‖k‖ * r < ε
grw : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (‖k‖ * r))
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 ε)

Tactic:
grw [← hk]
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
ε : ℝ
hε : ε > 0
k : 𝕜
hk₀ : 0 < ‖k‖
hk : ‖k‖ * r < ε
rwa :
  ∀ (hp : Membership.mem (γ := Filter E) (𝓝 0) (k • p.closedBall 0 r)) (hk₀ : 0 < ‖k‖) (hk : ‖k‖ * r < ε),
    Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (‖k‖ * r))
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (‖k‖ * r))) (hk₀ : 0 < ‖k‖) (hk : ‖k‖ * r < ε),
    Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (‖k‖ * r))
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (‖k‖ * r))

Tactic:
rwa [← set_smul_mem_nhds_zero_iff (norm_pos_iff.1 hk₀), smul_closedBall_zero hk₀] at hp

Premises used: norm_pos_iff, Seminorm.smul_closedBall_zero, set_smul_mem_nhds_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0

Tactic:
continuousAt_zero_of_forall'
    (fun r hr ↦ Filter.mem_of_superset (hp r hr) <| p.ball_subset_closedBall _ _)

Premises used: Seminorm.continuousAt_zero_of_forall', Seminorm.ball_subset_closedBall, OfNat.ofNat, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0

Tactic:
continuousAt_zero' (Filter.mem_of_superset hp <| p.ball_subset_closedBall _ _)

Premises used: Seminorm.continuousAt_zero', Seminorm.ball_subset_closedBall, Filter.mem_of_superset