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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ ∀ x ∈ t', x ∉ t → (∑ x ∈ t', w x)⁻¹ • w x • z x = 0

Tactic:
intro i

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
i : ι
⊢ i ∈ t' → i ∉ t → (∑ x ∈ t', w x)⁻¹ • w i • z i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1

Tactic:
intro i

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
⊢ w i ∈ Set.Icc 0 1
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
⊢ closure[inst✝¹] (⋃ i ∈ S, i) = ⋃ s ∈ S, closure[inst✝¹] s

Tactic:
closure_iUnion

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

Goal state before:
pp: case neg.convert_3
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ ∀ x_1 ∈ {x, y}, x_1 ∈ s

Tactic:
intro i

Goal state after:
case neg.convert_3
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
⊢ i ∈ {x, y} → i ∈ s
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι✝ : Sort u_1
κ : ι✝ → Sort u_2
α : Type u_3
β : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AlexandrovDiscrete α
inst✝³ : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst✝² : Finite ι
X : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), AlexandrovDiscrete (X i)
⊢ AlexandrovDiscrete ((i : ι) → X i)

Tactic:
by
  simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton,
    pi_principal, nhdsKer_singleton_pi, forall_true_iff]

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
⊢ connectedComponent x = connectedComponent y ↔ Joined x y

Tactic:
rw [← mem_pathComponent_iff, pathComponent_eq_connectedComponent, eq_comm]
  exact connectedComponent_eq_iff_mem

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : (𝓝 0).HasBasis p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ (𝓝 x).HasBasis p fun i ↦ (fun x_1 ↦ x + x_1) '' b i

Tactic:
rw [← map_add_left_nhds_zero]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : (𝓝 0).HasBasis p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ (map (fun x_1 ↦ x + x_1) (𝓝 0)).HasBasis p fun i ↦ (fun x_1 ↦ x + x_1) '' b i
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) • v x = 0

Tactic:
intro i

Goal state after:
case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
⊢ i ∈ s ∪ s' → i ∉ s' → (if i ∈ s' then b * w' i else 0) • v i = 0
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * w x else 0) • v x = 0

Tactic:
intro i

Goal state after:
case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
⊢ i ∈ s ∪ s' → i ∉ s → (if i ∈ s then a * w i else 0) • v i = 0
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_3
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
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : ∑ i ∈ sx, wx i = 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : ∑ i ∈ sy, wy i = 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ i ∈ sx.disjSum sy, Sum.elim zx zy i ∈ s

Tactic:
intro i

Goal state after:
case refine_2.refine_3
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
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : ∑ i ∈ sx, wx i = 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : ∑ i ∈ sy, wy i = 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι ⊕ ι'
⊢ i ∈ sx.disjSum sy → Sum.elim zx zy i ∈ s
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✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Tactic:
have : k ∈ t.erase j := mem_erase.2 ⟨ne_of_apply_ne _ hjk.symm, hk⟩

Goal state after:
𝕜 : 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✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
⊢ ∀ i ∈ s, 0 ≤ w i

Tactic:
intro i

Goal state after:
case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
i : ι
⊢ i ∈ s → 0 ≤ w i
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (√r * √r) ⊆ (s.sup p).ball 0 r

Tactic:
Real.mul_self_sqrt (le_of_lt hr)

Goal state after:
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 r ⊆ (s.sup p).ball 0 r
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
⊢ ∀ i ∈ u, w i ≤ 1

Tactic:
intro i

Goal state after:
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
i : Fin (n + 1)
⊢ i ∈ u → w i ≤ 1
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
⊢ ∀ (i : Fin (n + 1)), (↑u).indicator w i ∈ Icc 0 1

Tactic:
intro i

Goal state after:
case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
i : Fin (n + 1)
⊢ (↑u).indicator w i ∈ Icc 0 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
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
⊢ ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p

Tactic:
intro i

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
i : ι'
⊢ i ∈ s' → (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
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✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ (𝓝 x).HasBasis (fun sr ↦ 0 < sr.2) fun sr ↦ (sr.1.sup p).ball x sr.2

Tactic:
rw [← map_add_left_nhds_zero]

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ (Filter.map (fun x_1 ↦ x + x_1) (𝓝 0)).HasBasis (fun sr ↦ 0 < sr.2) fun sr ↦ (sr.1.sup p).ball x sr.2
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✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ (fun sr ↦ (sr.1.sup p).ball x sr.2) = fun i ↦ (fun x_1 ↦ x + x_1) '' (i.1.sup p).ball 0 i.2

Tactic:
ext sr : 1

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
sr : Finset ι × ℝ
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] ⇑(p i)
⊢ ∀ (i : ι), ⨅ i, comap (⇑↑i) (𝓝 0) ≤ comap (⇑(p i)) (𝓝 0)

Tactic:
intro i

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] ⇑(p i)
i : ι
⊢ ⨅ i, comap (⇑↑i) (𝓝 0) ≤ comap (⇑(p i)) (𝓝 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
G : Type u_5
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ IsUniformAddGroup (E →SLᵤ[σ, 𝔖] F)

Tactic:
by
  let φ : (E →SLᵤ[σ, 𝔖] F) →+ E →ᵤ[𝔖] F :=
    ⟨⟨(DFunLike.coe : (E →SLᵤ[σ, 𝔖] F) → E →ᵤ[𝔖] F), rfl⟩, fun _ _ => rfl⟩
  exact (isUniformEmbedding_coeFn _ _ _).isUniformAddGroup φ

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

Goal state before:
pp: 𝕜 : 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
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
⊢ p.ball 0 (‖c‖ * 1) ⊆ p.ball 0 r

Tactic:
exact ball_mono (by simpa using hc.le)

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

Goal state before:
pp: 𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
⊢ Tendsto (⇑f) (𝓝 0) (𝓝 (f 0))

Tactic:
f.map_zero,

Goal state after:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
⊢ Tendsto (⇑f) (𝓝 0) (𝓝 0)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
⊢ ∀ (i : ι'), Tendsto (⇑(q i) ∘ ⇑f) (𝓝 0) (𝓝 0)

Tactic:
intro i

Goal state after:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
i : ι'
⊢ Tendsto (⇑(q i) ∘ ⇑f) (𝓝 0) (𝓝 0)
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✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_bound' f hC fun x hx => ?_

Goal state after:
𝕜 : 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✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
⊢ ‖f x‖ ≤ C * ‖x‖
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✝¹⁰ : AddCommMonoid 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
y : F
⊢ (f 0) y = 0

Tactic:
f.map_zero,

Goal state after:
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✝¹⁰ : AddCommMonoid 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
y : F
⊢ 0 y = 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ Seminorm.IsBounded (fun s ↦ s.sup p) p LinearMap.id

Tactic:
intro i

Goal state after:
case refine_2
𝕜 : 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
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup fun s ↦ s.sup p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ Seminorm.IsBounded p (fun i ↦ (Finset.Iic i).sup p) LinearMap.id

Tactic:
intro i

Goal state after:
case refine_1
𝕜 : 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
i : ι
⊢ ∃ s C, ((fun i ↦ (Finset.Iic i).sup p) i).comp LinearMap.id ≤ C • s.sup p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1
𝕜 : 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
i : ι
⊢ ∃ s C, ((fun i ↦ (Finset.Iic i).sup p) i).comp LinearMap.id ≤ C • s.sup p

Tactic:
refine ⟨Finset.Iic i, 1, ?_⟩

Goal state after:
case refine_1
𝕜 : 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
i : ι
⊢ ((fun i ↦ (Finset.Iic i).sup p) i).comp LinearMap.id ≤ 1 • (Finset.Iic i).sup p