mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ f (0 • x + b • y) ≤ 0 • f x + b • f y

Tactic:
rw [zero_add] at hab
    subst b
    simp_rw [zero_smul, zero_add, one_smul, le_rfl]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ p₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s

Tactic:
mem_direction_iff_eq_vsub_right hp

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ (∃ p₂_1 ∈ s, p₂ -ᵥ p = p₂_1 -ᵥ p) ↔ p₂ ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)

Tactic:
apply sum_insert_zero

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ w i • (p i -ᵥ p i) = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ : E
r : ℝ
p q : Seminorm 𝕜 E
a : 𝕜
x : E
⊢ p (a • x) + q (a • x) = ‖a‖ * (p x + q x)

Tactic:
simp only [map_smul_eq_mul, map_smul_eq_mul, mul_add]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝¹⁴ : SeminormedRing 𝕜
inst✝¹³ : SeminormedRing 𝕜₂
inst✝¹² : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁰ : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁹ : RingHomIsometric σ₁₃
inst✝⁸ : AddCommGroup E
inst✝⁷ : AddCommGroup E₂
inst✝⁶ : AddCommGroup E₃
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ E₂
inst✝³ : Module 𝕜₃ E₃
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x✝¹ : 𝕜
x✝ : E
⊢ p (f (x✝¹ • x✝)) = ‖x✝¹‖ * p (f x✝)

Tactic:
by simp only [map_smulₛₗ _, map_smul_eq_mul, RingHomIsometric.norm_map]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ ↑(r • 1) * ⨅ u, p u + q (x✝ - u) = ⨅ u, ↑(r • 1) * p u + ↑(r • 1) * q (x✝ - u)

Tactic:
Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _),

Goal state after:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ ⨅ i, ↑(r • 1) * (p i + q (x✝ - i)) = ⨅ u, ↑(r • 1) * p u + ↑(r • 1) * q (x✝ - u)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ Metric.ball 0 r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff,
    map_smul_eq_mul]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ ∀ (a : 𝕜), ‖a‖ < r₁ → ∀ (b : E), p b ≤ r₂ → ‖a‖ * p b < r₁ * r₂
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
𝕜' : Type u_12
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedRing 𝕜'
inst✝⁶ : SMul 𝕜 𝕜'
inst✝⁵ : NormSMulClass 𝕜 𝕜'
inst✝⁴ : NormOneClass 𝕜'
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜' E
inst✝¹ : SMul 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜' E
p : Seminorm 𝕜' E
a : 𝕜
x : E
⊢ p.toFun (a • x) = ‖a‖ * p.toFun x

Tactic:
rw [← smul_one_smul 𝕜' a x, p.smul', norm_smul, norm_one, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i j : ι
hij : p i = p j
⊢ i = j

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub _ _ j] at ha

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent k fun i ↦ p ↑i -ᵥ p j
hij : p i = p j
⊢ i = j
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)

Tactic:
rw [show (1 : ℝ) = dist (Pi.single i 1 : ι → ℝ) (Pi.single j 1) by
    simp [dist_single_single i j (1 : ℝ) 1 hij, Real.dist_eq]]
  exact Metric.dist_le_diam_of_mem (bounded_stdSimplex _)
    (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
⊢ ∑ x ∈ fs, w' ↑x = ∑ i ∈ fs, w i

Tactic:
exact sum_congr rfl fun t ht ↦ by simp [w']

Goal state after:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a • ∑ i ∈ s, ws i • zs i + b • t.centerMass wt zt =
    (s.disjSum t).centerMass (Sum.elim (fun i ↦ a * ws i) fun j ↦ b * wt j) (Sum.elim zs zt)

Tactic:
t.centerMass_eq_of_sum_1 _ hwt,

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a • ∑ i ∈ s, ws i • zs i + b • ∑ i ∈ t, wt i • zt i =
    (s.disjSum t).centerMass (Sum.elim (fun i ↦ a * ws i) fun j ↦ b * wt j) (Sum.elim zs zt)
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : (interior [x -[𝕜] y]).Nonempty → (interior s).Nonempty
⊢ (interior s).Nonempty

Tactic:
segment_eq_Icc',

Goal state after:
case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : (interior (Icc (min x y) (max x y))).Nonempty → (interior s).Nonempty
⊢ (interior s).Nonempty
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case right
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
x : E
hx : x ∈ s
⊢ ({PUnit.unit}.centerMass (fun x ↦ 1) fun x_1 ↦ x) = x

Tactic:
simp only [Finset.centerMass, Finset.sum_singleton, inv_one, one_smul]

Goal state after:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t✝ : (i : ι) → Set (E i)
x : (i : ι) → E i
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
⊢ (∑ i, (∏ i_1, w i_1 (i i_1)) • fun i_1 ↦ f i_1 (i i_1)) i = ∑ g, (∏ i, w i (g i)) • f i (g i)

Tactic:
simp only [Finset.sum_apply, Pi.smul_apply]

Goal state after:
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
⊢ ∃ i ∈ {i ∈ t | w i ≠ 0}, w i • f y ≤ w i • (f ∘ p) i

Tactic:
by
    have hw' : (0 : 𝕜) < ∑ i ∈ t with w i ≠ 0, w i := by rwa [sum_filter_ne_zero]
    refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') ?_
    rw [← sum_smul, ← smul_le_smul_iff_of_pos_left (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ←
      centerMass, centerMass_filter_ne_zero]
    exact h.map_centerMass_le hw₀ hw₁ hp

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

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ p.moduleFilterBasis.filter = ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
refine le_antisymm (le_iInf fun i => ?_) ?_

Goal state after:
case refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
⊢ p.moduleFilterBasis.filter ≤ comap (⇑(p i)) (𝓝 0)

case refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ ⨅ i, comap (⇑(p i)) (𝓝 0) ≤ p.moduleFilterBasis.filter
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
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsTopologicalAddGroup (E →SLᵤ[σ, 𝔖] F)

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

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
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ IsTopologicalAddGroup (E →SLᵤ[σ, 𝔖] F)
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
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ Continuous[instTopologicalSpace σ F 𝔖, inst✝¹] fun f ↦ f x

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[instTopologicalSpace σ F 𝔖, inst✝¹] fun f ↦ f 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
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ T2Space (E →SLᵤ[σ, 𝔖] F)

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ T2Space (E →SLᵤ[σ, 𝔖] F)
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
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ ContinuousSMul 𝕜₂ (E →SLᵤ[σ, 𝔖] F)

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹¹ : NormedField 𝕜₁
inst✝¹⁰ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ ContinuousSMul 𝕜₂ (E →SLᵤ[σ, 𝔖] F)
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
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ (𝓝 0).HasBasis (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ {f | ∀ x ∈ Si.1, f x ∈ b Si.2}

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (𝓝 0).HasBasis (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
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
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ 𝓝 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ 𝓝 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_3.refine_2
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
⊢ t ∈ 𝓝 0

Tactic:
rcases (SeminormFamily.basisSets_iff _).1 ht with ⟨w, r, r_pos, hw⟩

Goal state after:
case refine_3.refine_2
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
⊢ t ∈ 𝓝 0
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
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: E : Type u_6
ι : Type u_9
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
p : ι → Seminorm ℝ E
hp : WithSeminorms p
f : E →ₗ[ℝ] ℝ
hf : ∃ s C, ∀ (x : E), f x ≤ (C • s.sup p) x
⊢ Continuous[inst✝, _] ⇑f

Tactic:
obtain ⟨s, C, hC⟩ := hf

Goal state after:
E : Type u_6
ι : Type u_9
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
p : ι → Seminorm ℝ E
hp : WithSeminorms p
f : E →ₗ[ℝ] ℝ
s : Finset ι
C : ℝ≥0
hC : ∀ (x : E), f x ≤ (C • s.sup p) x
⊢ Continuous[inst✝, _] ⇑f
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
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖] fun f ↦
    L ∘SL f

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

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 𝔖, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖] fun f ↦
    L ∘SL f