mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} =
    sInf {x | ∃ (h : 0 ≤ x), NNReal.mk x h ∈ {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖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
⊢ sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} =
    sInf {x | ∃ (h : 0 ≤ x), NNReal.mk x h ∈ {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}}
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 ≤ 0

Tactic:
]

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
M : ℝ≥0
hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
⊢ ↑‖x‖₊ ≠ 0

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
M : ℝ≥0
hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
⊢ ↑‖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 σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ≥0
hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C
x : E
hx : ‖x‖ = 1
⊢ ↑‖x‖₊ = 1

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 σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ≥0
hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C
x : E
hx : ‖x‖ = 1
⊢ ↑‖x‖₊ = 1
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case neg
𝕜 : 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
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
hlt : (normSeminorm 𝕜 F) x < ε
⊢ ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x

Tactic:
]

Goal state after:
case neg
𝕜 : 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
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
hlt : (normSeminorm 𝕜 F) x < ε
⊢ ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
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 : ‖f x‖ ≤ ↑M * ‖x‖
⊢ ‖f x‖ ≤ ↑M * ‖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
M : ℝ≥0
h'M : ↑M < ∞
x : E
hM : ‖f x‖ ≤ ↑M * ‖x‖
⊢ ‖f x‖ ≤ ↑M * ‖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
𝕜₂ : 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 F
inst✝² : IsTopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝² : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this✝¹ : IsUniformAddGroup G
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformOnFun.topologicalSpace E G 𝔖]
    ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ fun f ↦ L ∘SL f)

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
𝕜₂ : 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 F
inst✝² : IsTopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝² : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this✝¹ : IsUniformAddGroup G
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformOnFun.topologicalSpace E G 𝔖]
    ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ fun f ↦ L ∘SL f)
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 * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊

Tactic:
]

Goal state after:
𝕜 : 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 * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
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 * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
k : 𝕜
hk₁ : r * ‖f y‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
⊢ r * ‖f y‖₊⁻¹ < ‖k‖₊

Tactic:
]

Goal state after:
𝕜 : 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 * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
k : 𝕜
hk₁ : r * ‖f y‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
⊢ r * ‖f y‖₊⁻¹ < ‖k‖₊
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := { toModule := inst✝, norm_smul_le := ⋯ }
⊢ (s.sup p).ball 0 ε ⊆ q.ball 0 1

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := { toModule := inst✝, norm_smul_le := ⋯ }
⊢ (s.sup p).ball 0 ε ⊆ q.ball 0 1
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
hbdd : ∀ y ∈ (fun x ↦ ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊
⊢ sSup ((fun x ↦ ‖f x‖₊) '' ball 0 1) ≤ sSup ((fun x ↦ ‖f x‖₊) '' closedBall 0 1)

Tactic:
]

Goal state after:
𝕜 : 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
hbdd : ∀ y ∈ (fun x ↦ ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊
⊢ sSup ((fun x ↦ ‖f x‖₊) '' ball 0 1) ≤ sSup ((fun x ↦ ‖f x‖₊) '' closedBall 0 1)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case hbasis
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ p.moduleFilterBasis.filter.HasBasis (fun s ↦ s ∈ p.basisSets) id

Tactic:
]

Goal state after:
case hbasis
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ p.moduleFilterBasis.filter.HasBasis (fun s ↦ s ∈ p.basisSets) id
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_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(s.sup fun i ↦ NNReal.mk ((q i) (f x)) ⋯) = ↑(s.sup fun i ↦ NNReal.mk ((q.comp f i) x) ⋯)

Tactic:
]

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(s.sup fun i ↦ NNReal.mk ((q i) (f x)) ⋯) = ↑(s.sup fun i ↦ NNReal.mk ((q.comp f i) 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)
⊢ Continuous[Pi.topologicalSpace, UniformOnFun.topologicalSpace E ((i : ι) → F i) 𝔖]
    ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ fun F_1 ↦ ContinuousLinearMap.pi F_1)

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)
⊢ Continuous[Pi.topologicalSpace, UniformOnFun.topologicalSpace E ((i : ι) → F i) 𝔖]
    ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ fun F_1 ↦ ContinuousLinearMap.pi F_1)
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_9
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
⊢ ⨅ i, comap (⇑f) (comap (⇑(q i)) (𝓝 0)) = ⨅ i, comap (⇑(q.comp f i)) (𝓝 0)

Tactic:
]

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
⊢ ⨅ i, comap (⇑f) (comap (⇑(q i)) (𝓝 0)) = ⨅ i, comap (⇑(q.comp f i)) (𝓝 0)
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_9
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst✝ : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ WithSeminorms (q.comp f)

Tactic:
]

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst✝ : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ WithSeminorms (q.comp f)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
𝕜 : Type u_11
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
hp : Continuous[inst✝¹, _] ⇑p
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
s : Finset ι
C : ℝ≥0
hC : C ≠ 0
hqC : p ≤ (C • s.sup q).comp f
⊢ ∃ s C, C ≠ 0 ∧ p ≤ (C • s.sup q).comp f

Tactic:
]

Goal state after:
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
𝕜 : Type u_11
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
hp : Continuous[inst✝¹, _] ⇑p
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
s : Finset ι
C : ℝ≥0
hC : C ≠ 0
hqC : p ≤ (C • s.sup q).comp f
⊢ ∃ s C, C ≠ 0 ∧ p ≤ (C • s.sup q).comp f
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 : α → β
l : Filter α
P : l.Germ β
⊢ ∀ (a b : α → β), a ≈ b → (∃ b, a =ᶠ[l] fun x ↦ b) = ∃ b_1, b =ᶠ[l] fun x ↦ b_1

Tactic:
suffices ∀ f g : α → β, ∀ b : β, f =ᶠ[l] g → (f =ᶠ[l] fun _ ↦ b) → (g =ᶠ[l] fun _ ↦ b) from
      fun f g h ↦ propext ⟨fun ⟨b, hb⟩ ↦ ⟨b, this f g b h hb⟩, fun ⟨b, hb⟩ ↦ ⟨b, h.trans hb⟩⟩
    exact fun f g b hfg hf ↦ (hfg.symm).trans hf

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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, ⨅ j, PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, ⨅ j, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E
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
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : l.Germ M
f : α → M
⊢ (c₁ + c₂) • ↑f = c₁ • ↑f + c₂ • ↑f

Tactic:
norm_cast
      simp [add_smul]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
ht₁ : PolynormableSpace 𝕜 E
ht₂ : PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
ht₁ : PolynormableSpace 𝕜 E
ht₂ : PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E
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
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : l.Germ R
f✝ : l.Germ M
c₁ c₂ : α → R
f : α → M
⊢ (↑c₁ + ↑c₂) • ↑f = ↑c₁ • ↑f + ↑c₂ • ↑f

Tactic:
norm_cast
      simp [add_smul]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ (⨅ i, comap (⇑(p i)) (𝓝 0)).IsCountablyGenerated

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ (⨅ i, comap (⇑(p i)) (𝓝 0)).IsCountablyGenerated