awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
neg : Ne (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜)
neg₁ neg₂ neg₃ neg₄ : k ≠ n
⊢ HSub.hSub (α := 𝕜) (β := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜)
      ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜) ≠
    0

Tactic:
rwa [sub_ne_zero, (Embedding.injective _).ne_iff]

Premises used: sub_ne_zero, Function.Injective.ne_iff, Function.Embedding.injective
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
⊢ NoncompactSpace 𝕜

Tactic:
NormedSpace.noncompactSpace 𝕜 𝕜

Premises used: NormedSpace.noncompactSpace
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace ℝ E
⊢ NoncompactSpace E

Tactic:
NormedSpace.noncompactSpace ℝ E

Premises used: Real, NormedSpace.noncompactSpace
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
rw : ‖HSMul.hSMul (β := 𝕜') x 1‖ = ‖x‖ * norm.{u_2} (E := 𝕜') 1
⊢ norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') = ‖x‖ * norm.{u_2} (E := 𝕜') 1

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖HSMul.hSMul (β := 𝕜') x 1‖ = ‖x‖ * norm.{u_2} (E := 𝕜') 1

Tactic:
norm_smul _ _

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖HSMul.hSMul (β := 𝕜') x 1‖ = ‖x‖ * norm.{u_2} (E := 𝕜') 1

Tactic:
exact norm_smul _ _

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ nnnorm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') = ‖x‖₊ * nnnorm.{u_2} (E := 𝕜') 1

Tactic:
Subtype.ext <| norm_algebraMap 𝕜' x

Premises used: NNReal, norm_algebraMap, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x y : 𝕜
⊢ dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') =
    dist x y * norm.{u_2} (E := 𝕜') 1

Tactic:
simp only [dist_eq_norm, ← map_sub, norm_algebraMap]

Premises used: dist_eq_norm, map_sub, norm_algebraMap
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x : 𝕜
rw : ‖x‖ * norm.{u_2} (E := 𝕜') 1 = ‖x‖
rw₁ : ‖x‖ * 1 = ‖x‖
rw₂ rw₃ : ‖x‖ = ‖x‖
⊢ norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') = ‖x‖

Tactic:
rw [norm_algebraMap, norm_one, mul_one]

Premises used: NormOneClass.norm_one, norm_algebraMap, mul_one
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x : 𝕜
⊢ ‖HSMul.hSMul (β := 𝕜') x 1‖ = ‖x‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x : 𝕜
⊢ nnnorm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') = ‖x‖₊

Tactic:
Subtype.ext <| norm_algebraMap' _ _

Premises used: NNReal, norm_algebraMap', Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x y : 𝕜
⊢ dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') = dist x y

Tactic:
simp only [dist_eq_norm, ← map_sub, norm_algebraMap']

Premises used: dist_eq_norm, map_sub, norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜' : Type u_2
inst : SeminormedRing 𝕜'
inst_1 : NormOneClass 𝕜'
inst_2 : NormedAlgebra ℝ 𝕜'
x : ℝ≥0
⊢ norm (E := 𝕜') ((algebraMap ℝ≥0 𝕜' : (a : ℝ≥0) → 𝕜') x : 𝕜') = (↑x : ℝ)

Tactic:
(norm_algebraMap' 𝕜' (x : ℝ)).symm ▸ Real.norm_of_nonneg x.prop

Premises used: Eq.rec, Subtype.prop, norm_algebraMap', Eq.symm, NNReal.toReal, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜' : Type u_2
inst : SeminormedRing 𝕜'
inst_1 : NormOneClass 𝕜'
inst_2 : NormedAlgebra ℝ 𝕜'
x : ℝ≥0
⊢ nnnorm (E := 𝕜') ((algebraMap ℝ≥0 𝕜' : (a : ℝ≥0) → 𝕜') x : 𝕜') = x

Tactic:
Subtype.ext <| norm_algebraMap_nnreal 𝕜' x

Premises used: norm_algebraMap_nnreal, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_6
𝕜' : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
rw : (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c ∈ cobounded 𝕜
⊢ Membership.mem (γ := Filter 𝕜') (map (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') (cobounded 𝕜)) c

Tactic:
rw [mem_map]

Premises used: Filter.mem_map
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_6
𝕜' : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
rw :
  ∀ (hc : ∃ (C : ℝ), ∀ x ∈ cᶜ, ‖x‖ ≤ C),
    ∃ (C : ℝ), ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ((⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c)ᶜ x → ‖x‖ ≤ C
⊢ (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c ∈ cobounded 𝕜

Tactic:
rw [← isCobounded_def, ← isBounded_compl_iff, isBounded_iff_forall_norm_le] at hc ⊢

Premises used: isBounded_iff_forall_norm_le, Bornology.isBounded_compl_iff, Bornology.isCobounded_def
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_6
𝕜' : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
c : Set 𝕜'
hc : ∃ (C : ℝ), ∀ x ∈ cᶜ, ‖x‖ ≤ C
obtain :
  ∀ (s : ℝ) (hs : ∀ x ∈ cᶜ, ‖x‖ ≤ s),
    ∃ (C : ℝ), ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ((⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c)ᶜ x → ‖x‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ((⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c)ᶜ x → ‖x‖ ≤ C

Tactic:
obtain ⟨s, hs⟩ := hc
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_6
𝕜' : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
c : Set 𝕜'
s : ℝ
hs : ∀ x ∈ cᶜ, ‖x‖ ≤ s
x : 𝕜
hx : Membership.mem (γ := Set 𝕜) ((⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c)ᶜ x
⊢ ‖x‖ ≤ s

Tactic:
simpa using hs (algebraMap 𝕜 𝕜' x) hx

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_6
𝕜' : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
c : Set 𝕜'
s : ℝ
hs : ∀ x ∈ cᶜ, ‖x‖ ≤ s
⊢ ∃ (C : ℝ), ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ((⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c)ᶜ x → ‖x‖ ≤ C

Tactic:
exact ⟨s, fun x hx ↦ by simpa using hs (algebraMap 𝕜 𝕜' x) hx⟩
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
⊢ Isometry.{u_1, u_2} (α := 𝕜) (β := 𝕜') (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜')

Tactic:
Isometry.of_dist_eq fun x y => ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
refine :
  ∀ (x y : 𝕜),
    dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') = dist x y
⊢ Isometry.{u_1, u_2} (α := 𝕜) (β := 𝕜') (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜')

Tactic:
refine Isometry.of_dist_eq fun x y => ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x y : 𝕜
rw :
  ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
    dist x y
rw₁ :
  ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
    ‖x - y‖
rw₂ : norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') (x - y) : 𝕜') = ‖x - y‖
rw₃ rw₄ : ‖x - y‖ = ‖x - y‖
⊢ dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') = dist x y

Tactic:
rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap']

Premises used: dist_eq_norm, map_sub, norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜_1
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜_1 𝕜'
𝕜 : Type u_6
inst_3 : NormedDivisionRing 𝕜
inst_4 : CharZero 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
q : ℚ
x : 𝕜
rw : ‖HSMul.hSMul (β := ℝ) q 1 • x‖ ≤ ‖q‖ * ‖x‖
rw₁ : ‖HSMul.hSMul (α := ℝ) (↑q : ℝ) x‖ ≤ ‖q‖ * ‖x‖
rw₂ : norm (E := ℝ) (↑q : ℝ) * ‖x‖ ≤ ‖q‖ * ‖x‖
rw₃ rw₄ : ‖q‖ * ‖x‖ ≤ ‖q‖ * ‖x‖
⊢ ‖q • x‖ ≤ ‖q‖ * ‖x‖

Tactic:
rw [← smul_one_smul ℝ q x, Rat.smul_one_eq_cast, norm_smul, Rat.norm_cast_real]

Premises used: Real, norm_smul, Rat.norm_cast_real, smul_one_smul, Rat.smul_one_eq_cast
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
q : 𝕜
x : PUnit.{u_6 + 1}
⊢ ‖q • x‖ ≤ ‖q‖ * ‖x‖

Tactic:
simp only [norm_eq_zero, mul_zero, le_refl]

Premises used: le_refl, PUnit.norm_eq_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : SeminormedAddCommGroup E
inst_4 : NormedSpace 𝕜' E
c : 𝕜
x : E
rw rw₁ : ‖c‖ * ‖x‖ = ‖c‖ * ‖x‖
⊢ norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') c : 𝕜') * ‖x‖ = ‖c‖ * ‖x‖

Tactic:
rw [norm_algebraMap']

Premises used: norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_6
inst_3 : SeminormedAddCommGroup E
h : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
inst_5 : IsScalarTower 𝕜 𝕜' E
smul : ∀ (x : 𝕜) (x_1 : E), SMul.smul x x_1 = SMul.smul x x_1
⊢ restrictScalars 𝕜 𝕜' E = h

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_6
inst_3 : SeminormedAddCommGroup E
h : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
inst_5 : IsScalarTower 𝕜 𝕜' E
x : 𝕜
x_1 : E
⊢ SMul.smul x x_1 = SMul.smul x x_1

Tactic:
apply algebraMap_smul

Premises used: algebraMap_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
simp : norm.{u_7} (E := E) 0 = 0
⊢ ‖-x + x‖ = 0

Tactic:
simp only [add_comm, ← sub_eq_add_neg, sub_self]

Premises used: sub_self, sub_eq_add_neg, add_comm
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
⊢ 0 = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (β := E) 0 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
⊢ 0 = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (β := E) 0 0

Tactic:
have : (0 : E) = (0 : 𝕜) • (0 : E) := by simp
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
this : 0 = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (β := E) 0 0
rw : norm.{u_6} (E := 𝕜) 0 * norm.{u_7} (E := E) 0 = 0
⊢ norm.{u_7} (E := E) 0 = 0

Tactic:
rw [this, core.norm_smul]

Premises used: SeminormedSpace.Core.norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
this : 0 = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (β := E) 0 0
⊢ norm.{u_6} (E := 𝕜) 0 * norm.{u_7} (E := E) 0 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
simp : -y + x = x + -y
⊢ -y + x = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (-1) (-x + y)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
⊢ -y + x = x + -y

Tactic:
abel
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
⊢ -y + x = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (-1) (-x + y)

Tactic:
have : -y + x = (-1 : 𝕜) • (-x + y) := by simp; abel
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
this : -y + x = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (-1) (-x + y)
rw : ‖-x + y‖ = norm.{u_6} (E := 𝕜) (-1) * ‖-x + y‖
⊢ ‖-x + y‖ = ‖-y + x‖

Tactic:
rw [this, core.norm_smul]

Premises used: SeminormedSpace.Core.norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
this : -y + x = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (-1) (-x + y)
⊢ ‖-x + y‖ = norm.{u_6} (E := 𝕜) (-1) * ‖-x + y‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
⊢ -x + z = -x + y + (-y + z)

Tactic:
abel
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
⊢ -x + z = -x + y + (-y + z)

Tactic:
have : -x + z = (-x + y) + (-y + z) := by abel
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
this : -x + z = -x + y + (-y + z)
rw : ‖-x + y + (-y + z)‖ ≤ ‖-x + y‖ + ‖-y + z‖
⊢ ‖-x + z‖ ≤ ‖-x + y‖ + ‖-y + z‖

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
this : -x + z = -x + y + (-y + z)
⊢ ‖-x + y + (-y + z)‖ ≤ ‖-x + y‖ + ‖-y + z‖

Tactic:
core.norm_triangle _ _

Premises used: SeminormedSpace.Core.norm_triangle
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
this : -x + z = -x + y + (-y + z)
⊢ ‖-x + y + (-y + z)‖ ≤ ‖-x + y‖ + ‖-y + z‖

Tactic:
exact core.norm_triangle _ _

Premises used: SeminormedSpace.Core.norm_triangle
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
⊢ (↑(NNReal.mk ((fun (x y : E) ↦ ‖-x + y‖) x y) ⋯) : ℝ≥0∞) = ENNReal.ofReal ‖-x + y‖

Tactic:
(ENNReal.ofReal_eq_coe_nnreal _).symm

Premises used: ENNReal.ofReal_eq_coe_nnreal, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
⊢ (↑(NNReal.mk ((fun (x y : E) ↦ ‖-x + y‖) x y) ⋯) : ℝ≥0∞) = ENNReal.ofReal ‖-x + y‖

Tactic:
exact (ENNReal.ofReal_eq_coe_nnreal _).symm

Premises used: ENNReal.ofReal_eq_coe_nnreal, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
rw : ‖-x + y‖ = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]

Premises used: sub_eq_zero, norm_neg_add, NormedSpace.Core.norm_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
h
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
exact h
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
rw : ‖-x + y‖ = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]

Premises used: sub_eq_zero, norm_neg_add, NormedSpace.Core.norm_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
h
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
exact h
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = UniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
rw : ‖-x + y‖ = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]

Premises used: sub_eq_zero, norm_neg_add, NormedSpace.Core.norm_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = UniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
h
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = UniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
exact h
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
rw : ‖-x + y‖ = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]

Premises used: sub_eq_zero, norm_neg_add, NormedSpace.Core.norm_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
h
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
exact h