awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 : ℝ)
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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) ≤
    HSMul.hSMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HSMul.hSMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
have 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 : ℝ)
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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 : (a : E) → ℝ) (a • x + b • y) ≤
    HSMul.hSMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HSMul.hSMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
have 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 : ℝ)
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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 ℝ (p.ball x r)
have 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}
Tactic: convert! (p.convexOn.translate_left (-x)).convex_lt r
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 : ℝ
⊢ 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}
have 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
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
⊢ 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
have 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
Tactic: rw [preimage_univ, sep_univ, p.mem_ball, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 ℝ (p.closedBall x r)
have rw : Convex.{0, u_7} ℝ (E := E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ)
Tactic: rw [closedBall_eq_biInter_ball]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
⊢ p.toFun (a • x) = ‖a‖ * p.toFun x
have rw : p.toFun (HSMul.hSMul (β := 𝕜') a 1 • x) = ‖a‖ * p.toFun x
Tactic: rw [← smul_one_smul 𝕜' a x, p.smul', norm_smul, norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
⊢ p.toFun (a • x) = ‖a‖ * p.toFun x
have rw₁ : ‖HSMul.hSMul (β := 𝕜') a 1‖ * p.toFun x = ‖a‖ * p.toFun x
Tactic: rw [← smul_one_smul 𝕜' a x, p.smul', norm_smul, norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
⊢ p.toFun (a • x) = ‖a‖ * p.toFun x
have rw₂ : ‖a‖ * norm.{u_12} (E := 𝕜') 1 * p.toFun x = ‖a‖ * p.toFun x
Tactic: rw [← smul_one_smul 𝕜' a x, p.smul', norm_smul, norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
⊢ p.toFun (a • x) = ‖a‖ * p.toFun x
have rw₃ : ‖a‖ * 1 * p.toFun x = ‖a‖ * p.toFun x
Tactic: rw [← smul_one_smul 𝕜' a x, p.smul', norm_smul, norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
⊢ p.toFun (a • x) = ‖a‖ * p.toFun x
have rw₄ : ‖a‖ * p.toFun x = ‖a‖ * p.toFun x
Tactic: rw [← smul_one_smul 𝕜' a x, p.smul', norm_smul, norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
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)
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
have hp₁ : ∀ 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
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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))
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
have rwa : Tendsto (α := E) (β := ℝ) ((⇑p : (a : E) → ℝ) : (a : E) → ℝ) (𝓝 0) (𝓝 ((p : (a : E) → ℝ) 0) : Filter ℝ)
Tactic: rwa [ContinuousAt, Metric.nhds_basis_closedBall.tendsto_right_iff, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 ℝ)
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
have rwa₁ : ∀ (i : ℝ),
  0 < i →
    ∀ᶠ (x : E) in 𝓝 0,
      Membership.mem (α := ℝ) (γ := Set ℝ) (Metric.closedBall ((p : (a : E) → ℝ) 0) i : Set ℝ) ((p : (a : E) → ℝ) x : ℝ)
Tactic: rwa [ContinuousAt, Metric.nhds_basis_closedBall.tendsto_right_iff, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 : ℝ)
⊢ ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
have rwa₂ : ∀ (i : ℝ),
  0 < i → ∀ᶠ (x : E) in 𝓝 0, Membership.mem (α := ℝ) (γ := Set ℝ) (Metric.closedBall 0 i) ((p : (a : E) → ℝ) x : ℝ)
Tactic: rwa [ContinuousAt, Metric.nhds_basis_closedBall.tendsto_right_iff, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
have refine : ∀ (ε : ℝ) (hε : ε > 0), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 ε)
Tactic: refine continuousAt_zero_of_forall' fun ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε
have inl : ∀ (hr : r ≤ 0), ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε
Tactic: rcases le_or_gt r 0 with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 < ε
⊢ ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε
have inr : ∀ (hr : 0 < r), ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε
Tactic: rcases le_or_gt r 0 with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
⊢ ∃ (k : 𝕜), 0 < ‖k‖ ∧ ‖k‖ * r < ε
have h : 0 < norm.{u_3} (E := 𝕜) 1 ∧ norm.{u_3} (E := 𝕜) 1 * r < ε
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 ε)
have obtain : ∀ (k : 𝕜) (hk₀ : 0 < ‖k‖) (hk : ‖k‖ * r < ε), 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)
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 < ε
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 ε)
have grw : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (‖k‖ * r))
Tactic: grw [← hk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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 < ε
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (‖k‖ * r))
have 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))
Tactic: rwa [← set_smul_mem_nhds_zero_iff (norm_pos_iff.1 hk₀), smul_closedBall_zero hk₀] at hp
Cleared hypotheses: hp, hk₀, hk
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
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))
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (‖k‖ * r))
have 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))
Tactic: rwa [← set_smul_mem_nhds_zero_iff (norm_pos_iff.1 hk₀), smul_closedBall_zero hk₀] at hp
Cleared hypotheses: hp, hk₀, hk
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
⊢ UniformContinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
have hp₁ : Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)
Tactic: have hp : Filter.Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp_1 : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
hp : Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)
⊢ UniformContinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
have rw : Tendsto.{u_7, 0} (α := E × E) (β := ℝ)
  ((fun (p : ℝ × ℝ) ↦ dist p.1 p.2) ∘ fun (x : E × E) ↦ ((p : (a : E) → ℝ) x.1, (p : (a : E) → ℝ) x.2))
  (comap (β := E) (fun (x : E × E) ↦ x.1 - x.2) (𝓝 0)) (𝓝 0)
Tactic: rw [UniformContinuous, uniformity_eq_comap_nhds_zero_swapped,
    Metric.uniformity_eq_comap_nhds_zero, Filter.tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
this : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)
have this₁ : IsUniformAddGroup E
Tactic: haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst_3, _] (⇑q : (a : E) → ℝ)
hpq : p ≤ q
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)
have refine : ∀ (r : ℝ) (hr : r > 0), IsOpen[inst_3] (q.ball 0 r)
Tactic: refine Seminorm.continuous_of_forall (fun r hr ↦ Filter.mem_of_superset
    (IsOpen.mem_nhds ?_ <| q.mem_ball_self hr) (ball_antitone hpq))
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst_3, _] (⇑q : (a : E) → ℝ)
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen[inst_3] (q.ball 0 r)
have rw : IsOpen[inst_3] {y : E | (q : (a : E) → ℝ) y < r}
Tactic: rw [ball_zero_eq]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
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 : Continuous[inst_3, _] (⇑p : (a : E) → ℝ)
r : ℝ
hr : 0 < r
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
have this : Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)
Tactic: have this : Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp.tendsto 0
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ inst_3 = PseudoMetricSpace.toUniformSpace
have refine : Eq.{u_7 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
Tactic: refine IsUniformAddGroup.ext ‹_›
    p.toAddGroupSeminorm.toSeminormedAddCommGroup.to_isUniformAddGroup ?_
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ Eq.{u_7 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
have a : LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
a : LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)
⊢ Eq.{u_7 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
have a₁ : LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)
have a : Tendsto.{u_7, 0} (α := E) norm (𝓝 0) (𝓝 0)
Tactic: rw [← @comap_norm_nhds_zero E p.toAddGroupSeminorm.toSeminormedAddGroup, ← tendsto_iff_comap]