mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module 𝕜₃ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →L[𝕜₃] F →SL[σ₂₃] G
c : 𝕜₃
x : E
y : F
⊢ (f (c • x)) y = c • (f x) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_3_to_5 :
  UniformEquicontinuous (DFunLike.coe ∘ f) →
    BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧ Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))
tfae_5_to_4 :
  BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧ Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k))) →
    ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p
p : Seminorm 𝕜 E
hp : Continuous[inst✝².toTopologicalSpace, _] ⇑p
hfp : ∀ (k : κ), (q i).comp (f k) ≤ p
x : E
k : κ
⊢ dist ((DFunLike.coe ∘ f) k 0) ((DFunLike.coe ∘ f) k x) ≤ p x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
⊢ Continuous[inst✝², instTopologicalSpace σ F 𝔖] ⇑B

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : Semiring R
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
⊢ (f (x - x')) y = (f x) y - (f x') y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : Semiring R
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ (f (-x)) y = -(f x) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
u : UniformSpace F
hu : IsUniformAddGroup F
hq : WithSeminorms q
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∀ (i : ι'), ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      ∀ (i : ι'),
        BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
          Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding (restrictScalars 𝕜')

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Seminorm.IsBounded p q LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Seminorm.IsBounded q p LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ WithSeminorms q

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ WithSeminorms fun s ↦ s.sup p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
⊢ 𝓤 (E →SL[σ₁₂] F) = ⨅ r, ⨅ (_ : r > 0), 𝓟 {f | ‖-f.1 + f.2‖ < r}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup F
inst✝⁹ : SeminormedAddCommGroup G
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ 0 ≤ ‖h‖ * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ WithSeminorms fun i ↦ (Finset.Iic i).sup p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup F
inst✝⁹ : SeminormedAddCommGroup G
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
⊢ ‖(h ∘SL f) x‖ ≤ ‖h‖ * ‖f‖ * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝²¹ : NormedField 𝕜₁✝
inst✝²⁰ : NormedField 𝕜₂✝
σ✝ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
G✝ : Type u_5
inst✝¹⁹ : AddCommGroup E✝
inst✝¹⁸ : Module 𝕜₁✝ E✝
inst✝¹⁷ : TopologicalSpace E✝
inst✝¹⁶ : AddCommGroup F✝
inst✝¹⁵ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
inst✝¹² : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹¹ : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup G
inst✝⁵ : Module 𝕜₃ G
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun x ↦ ⇑L '' x) 𝔖 𝔗
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖] fun f ↦
    f ∘SL L

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
x : E
hx : 0 < ‖x‖
⊢ 0 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
⊢ ‖f‖ = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
⊢ WithSeminorms (p ∘ ⇑e)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
⊢ 0 ≤ C * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
⊢ ‖pi L‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup F
inst✝¹⁰ : SeminormedAddCommGroup G
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NontriviallyNormedField 𝕜₃
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₁₃
inst✝ : RingHomIsometric σ₂₃
L : F →SL[σ₂₃] G
⊢ 0 ≤ ‖L‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 < ‖c‖ / ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ₁₂] F
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
x : E
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗᵢ[σ₁₂] F
x : E
⊢ ‖f.toContinuousLinearMap x‖ ≤ 1 * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ ‖f‖₊ = sInf {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
S : Type u_5
inst✝²² : NormedField 𝕜
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommGroup E
inst✝¹⁹ : Module 𝕜 E
inst✝¹⁸ : TopologicalSpace E
inst✝¹⁷ : IsTopologicalAddGroup E
inst✝¹⁶ : ContinuousConstSMul 𝕜 E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : Module 𝕜 F
inst✝¹³ : TopologicalSpace F
inst✝¹² : IsTopologicalAddGroup F
inst✝¹¹ : ContinuousConstSMul 𝕜 F
inst✝¹⁰ : AddCommGroup G
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalAddGroup G
inst✝⁶ : ContinuousConstSMul 𝕜 G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass 𝕜 S G
inst✝³ : ContinuousConstSMul S G
inst✝² : Module S F
inst✝¹ : SMulCommClass 𝕜 S F
inst✝ : ContinuousConstSMul S F
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] (↑(prodₗ S)).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
⊢ ‖x‖₊ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ≥0
hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C
x : E
hx : ‖x‖ = 1
⊢ ‖x‖₊ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsLeast {C | ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : SeminormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ ‖h ∘SL f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : AddCommGroup G
inst✝¹³ : AddCommGroup H
inst✝¹² : NormedField 𝕜
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : Module 𝕜 H
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalAddGroup G
inst✝² : IsTopologicalAddGroup H
inst✝¹ : ContinuousConstSMul 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x✝¹ x✝ : G →L[𝕜] G
⊢ (↑↑(e.arrowCongr e)).toFun (x✝¹ * x✝) = (↑↑(e.arrowCongr e)).toFun x✝¹ * (↑↑(e.arrowCongr e)).toFun x✝

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
hM : ∀ (x : E), ‖f x‖ₑ ≤ ↑M * ‖x‖ₑ
h'M : ↑M < ∞
⊢ 0 ≤ ↑M

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : AddCommGroup G
inst✝¹³ : AddCommGroup H
inst✝¹² : NormedField 𝕜
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : Module 𝕜 H
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalAddGroup G
inst✝² : IsTopologicalAddGroup H
inst✝¹ : ContinuousConstSMul 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x✝ : 𝕜
⊢ (↑↑(e.arrowCongr e)).toFun ((algebraMap 𝕜 (G →L[𝕜] G)) x✝) = (algebraMap 𝕜 (H →L[𝕜] H)) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
h'M : ↑M < ∞
x : E
hM : ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal ↑M * ENNReal.ofReal ‖x‖
⊢ 0 ≤ ↑M

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
h'M : ↑M < ∞
x : E
hM : ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal (↑M * ‖x‖)
⊢ 0 ≤ ↑M * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0∞
hM : ∀ (x : E), ‖f x‖ₑ ≤ M * ‖x‖ₑ
⊢ ‖f‖ₑ ≤ M

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
a b : ℝ≥0∞
hf : ‖f‖ₑ ≤ a
hx : ‖x‖ₑ ≤ b
⊢ ‖f‖ₑ * ‖x‖ₑ ≤ a * b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
⊢ ∃ x, r * ‖x‖₊ < ‖f x‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr₀ : 0 ≤ r
hr : r < ‖f‖
⊢ ∃ x, r * ‖x‖ < ‖f x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖f y‖₊
heq : y = 0
⊢ False

Tactic:
by

Goal state after: