mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case pos
𝕜 : 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‖
this : 0 < ‖c‖ / ε
x : F
hx : ‖x‖ = 0
⊢ q x ≤ ‖c‖ / ε * ‖x‖

Tactic:
rw [hx, mul_zero]

Goal state after:
case pos
𝕜 : 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‖
this : 0 < ‖c‖ / ε
x : F
hx : ‖x‖ = 0
⊢ q x ≤ 0
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:
;

Goal state after:
𝕜 : 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‖₊
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
x✝ : H
⊢ ((↑↑(e.arrowCongr e)).toFun (x✝² * x✝¹)) x✝ = ((↑↑(e.arrowCongr e)).toFun x✝² * (↑↑(e.arrowCongr e)).toFun x✝¹) x✝

Tactic:
;

Goal state after:
𝕜 : 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
x✝ : H
⊢ ((↑↑(e.arrowCongr e)).toFun (x✝² * x✝¹)) x✝ = ((↑↑(e.arrowCongr e)).toFun x✝² * (↑↑(e.arrowCongr e)).toFun x✝¹) x✝
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✝ : H
⊢ ((↑↑(e.arrowCongr e)).toFun ((algebraMap 𝕜 (G →L[𝕜] G)) x✝¹)) x✝ = ((algebraMap 𝕜 (H →L[𝕜] H)) x✝¹) x✝

Tactic:
;

Goal state after:
𝕜 : 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✝ : H
⊢ ((↑↑(e.arrowCongr e)).toFun ((algebraMap 𝕜 (G →L[𝕜] G)) x✝¹)) x✝ = ((algebraMap 𝕜 (H →L[𝕜] H)) x✝¹) x✝
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
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝³ x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : E
x✝ : ι
⊢ (ContinuousLinearMap.pi (x✝³ + x✝²)) x✝¹ x✝ = (ContinuousLinearMap.pi x✝³ + ContinuousLinearMap.pi x✝²) x✝¹ x✝

Tactic:
;

Goal state after:
𝕜₁ : 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
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝³ x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : E
x✝ : ι
⊢ (ContinuousLinearMap.pi (x✝³ + x✝²)) x✝¹ x✝ = (ContinuousLinearMap.pi x✝³ + ContinuousLinearMap.pi x✝²) x✝¹ x✝
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
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝³ : 𝕜
x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : E
x✝ : ι
⊢ (ContinuousLinearMap.pi (x✝³ • x✝²)) x✝¹ x✝ = ((RingHom.id 𝕜) x✝³ • ContinuousLinearMap.pi x✝²) x✝¹ x✝

Tactic:
;

Goal state after:
𝕜₁ : 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
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝³ : 𝕜
x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : E
x✝ : ι
⊢ (ContinuousLinearMap.pi (x✝³ • x✝²)) x✝¹ x✝ = ((RingHom.id 𝕜) x✝³ • ContinuousLinearMap.pi x✝²) x✝¹ x✝
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
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : ι
x✝ : E
⊢ ((fun f i ↦ ContinuousLinearMap.proj i ∘SL f) ((fun F_1 ↦ ContinuousLinearMap.pi F_1) x✝²) x✝¹) x✝ = (x✝² x✝¹) x✝

Tactic:
;

Goal state after:
𝕜₁ : 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
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : ι
x✝ : E
⊢ ((fun f i ↦ ContinuousLinearMap.proj i ∘SL f) ((fun F_1 ↦ ContinuousLinearMap.pi F_1) x✝²) x✝¹) x✝ = (x✝² x✝¹) x✝
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
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝² : E →Lᵤ[𝕜, 𝔖] (i : ι) → F i
x✝¹ : E
x✝ : ι
⊢ ((fun F_1 ↦ ContinuousLinearMap.pi F_1) ((fun f i ↦ ContinuousLinearMap.proj i ∘SL f) x✝²)) x✝¹ x✝ = x✝² x✝¹ x✝

Tactic:
;

Goal state after:
𝕜₁ : 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
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝² : E →Lᵤ[𝕜, 𝔖] (i : ι) → F i
x✝¹ : E
x✝ : ι
⊢ ((fun F_1 ↦ ContinuousLinearMap.pi F_1) ((fun f i ↦ ContinuousLinearMap.proj i ∘SL f) x✝²)) x✝¹ x✝ = x✝² x✝¹ x✝
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: case ha
𝕜 : 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 σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr✝ : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < ‖f x‖₊
hx0 : 0 < ‖x‖₊
⊢ 0 < ‖f x‖₊

Tactic:
;

Goal state after:
case ha
𝕜 : 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 σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr✝ : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < ‖f x‖₊
hx0 : 0 < ‖x‖₊
⊢ 0 < ‖f x‖₊
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddMonoidWithOne M
⊢ 0 = fun x ↦ 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddMonoidWithOne M
⊢ 0 = fun x ↦ 0
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddMonoidWithOne M
x✝ : ℕ
⊢ ↑x✝ + 1 = fun x ↦ ↑x✝ + 1

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddMonoidWithOne M
x✝ : ℕ
⊢ ↑x✝ + 1 = fun x ↦ ↑x✝ + 1
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddGroupWithOne G
x✝ : ℕ
⊢ -1 + -↑x✝ = fun x ↦ -1 + -↑x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddGroupWithOne G
x✝ : ℕ
⊢ -1 + -↑x✝ = fun x ↦ -1 + -↑x✝
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: case hbc
𝕜 : Type u_1
E : Type u_4
Eₗ : Type u_5
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : SeminormedAddCommGroup Fₗ
inst✝⁵ : SeminormedAddCommGroup Gₗ
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜 Eₗ
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ ‖compL 𝕜 Eₗ Fₗ Gₗ‖ ≤ 1

Tactic:
;

Goal state after:
case hbc
𝕜 : Type u_1
E : Type u_4
Eₗ : Type u_5
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : SeminormedAddCommGroup Fₗ
inst✝⁵ : SeminormedAddCommGroup Gₗ
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜 Eₗ
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ ‖compL 𝕜 Eₗ Fₗ Gₗ‖ ≤ 1
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup F
inst✝¹⁷ : SeminormedAddCommGroup G
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gF : F' →SL[σ₂'] F
x✝¹ : E'
x✝ : F'
⊢ ((f.bilinearComp 0 gF) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup F
inst✝¹⁷ : SeminormedAddCommGroup G
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gF : F' →SL[σ₂'] F
x✝¹ : E'
x✝ : F'
⊢ ((f.bilinearComp 0 gF) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup F
inst✝¹⁷ : SeminormedAddCommGroup G
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
x✝¹ : E'
x✝ : F'
⊢ ((f.bilinearComp gE 0) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup F
inst✝¹⁷ : SeminormedAddCommGroup G
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
x✝¹ : E'
x✝ : F'
⊢ ((f.bilinearComp gE 0) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: case hbc
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
x : E
⊢ ‖c x‖ ≤ ‖c‖ * ‖x‖

Tactic:
;

Goal state after:
case hbc
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
x : E
⊢ ‖c x‖ ≤ ‖c‖ * ‖x‖
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst✝³² : SeminormedAddCommGroup E
inst✝³¹ : SeminormedAddCommGroup Eₗ
inst✝³⁰ : SeminormedAddCommGroup F
inst✝²⁹ : SeminormedAddCommGroup Fₗ
inst✝²⁸ : SeminormedAddCommGroup G
inst✝²⁷ : SeminormedAddCommGroup Gₗ
inst✝²⁶ : NontriviallyNormedField 𝕜
inst✝²⁵ : NontriviallyNormedField 𝕜₂
inst✝²⁴ : NontriviallyNormedField 𝕜₃
inst✝²³ : NormedSpace 𝕜 E
inst✝²² : NormedSpace 𝕜 Eₗ
inst✝²¹ : NormedSpace 𝕜₂ F
inst✝²⁰ : NormedSpace 𝕜 Fₗ
inst✝¹⁹ : NormedSpace 𝕜₃ G
inst✝¹⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : FunLike 𝓕 E F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁴ : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst✝¹³ : SeminormedAddCommGroup E'
inst✝¹² : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝¹¹ : NontriviallyNormedField 𝕜₁'
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
inst✝⁹ : NormedSpace 𝕜₁' E'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝⁶ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁵ : RingHomIsometric σ₂₃
inst✝⁴ : RingHomIsometric σ₁₃'
inst✝³ : RingHomIsometric σ₂₃'
inst✝² : RingHomIsometric σ₁₃
inst✝¹ : RingHomIsometric σ₁'
inst✝ : RingHomIsometric σ₂'
c : StrongDual 𝕜 E
x : Fₗ
⊢ ‖({ toFun := smulRightₗ, map_add' := ⋯, map_smul' := ⋯ } c) x‖ ≤ 1 * ‖c‖ * ‖x‖

Tactic:
simp only [coe_smulRightₗ, one_mul, norm_smulRight_apply, LinearMap.coe_mk, AddHom.coe_mk,
        le_refl]

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, ↑(u a) ≤ b
⊢ ∀ (a : ι), ↑(u a) ≤ b → ↑(u a) ≤ ↑b.toNNReal

Tactic:
;

Goal state after:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, ↑(u a) ≤ b
⊢ ∀ (a : ι), ↑(u a) ≤ b → ↑(u a) ≤ ↑b.toNNReal
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf (fun i ↦ ↑(u i)) f = ↑(liminf u f)

pp: case neg
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : ¬IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf (fun i ↦ ↑(u i)) f = ↑(liminf u f)

Tactic:
;

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf (fun i ↦ ↑(u i)) f = ↑(liminf u f)

case neg
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : ¬IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf (fun i ↦ ↑(u i)) f = ↑(liminf u f)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)

pp: case neg
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)

Tactic:
;

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)

case neg
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ᶠ (a : α) in f, ∀ (b : β), u a b ≤ limsup (fun a' ↦ u a' b) f

Tactic:
by
    rw [eventually_countable_forall]
    exact fun b => ENNReal.eventually_le_limsup fun a => u a b

Goal state after: