mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
h : AffineIndependent k fun p ↦ ↑p
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hp₁ : p₁ ∈ s
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
· have p₁ : P := AddTorsor.nonempty.some
    let hsv := Basis.ofVectorSpace k V
    have hsvi := hsv.linearIndependent
    have hsvt := hsv.span_eq
    rw [Basis.coe_ofVectorSpace] at hsvi hsvt
    have h0 : ∀ v : V, v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0 := by
      intro v hv
      simpa [hsv] using hsv.ne_zero ⟨v, hv⟩
    rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
    exact
      ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' _, Set.empty_subset _, hsvi,
        affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt⟩

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hp₁ : p₁ ∈ s
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
Module: Mathlib.Topology.AlexandrovDiscrete

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

Tactic:
simp_rw [sUnion_eq_biUnion, closure_iUnion]

Goal state after:
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 : α
⊢ ∀ (a : α) (b : β), 𝓝 a ×ˢ 𝓝 b = 𝓟 (nhdsKer {(a, b)})

Tactic:
← principal_nhdsKer_singleton,

Goal state after:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ ∀ (a : α) (b : β), 𝓟 (nhdsKer {a}) ×ˢ 𝓟 (nhdsKer {b}) = 𝓟 (nhdsKer {(a, b)})
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)
⊢ ∀ (a : (i : ι) → X i), (Filter.pi fun i ↦ 𝓝 (a i)) = 𝓟 (nhdsKer {a})

Tactic:
← principal_nhdsKer_singleton,

Goal state after:
ι✝ : 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)
⊢ ∀ (a : (i : ι) → X i), (Filter.pi fun i ↦ 𝓟 (nhdsKer {a i})) = 𝓟 (nhdsKer {a})
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case neg
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
⊢ a • x + b • y ∈ s

Tactic:
· convert! h { x, y } (fun z => if z = y then b else a) _ _ _
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial]
    · grind
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial, hab]
    · intro i hi
      simp only [Finset.mem_singleton, Finset.mem_insert] at hi
      cases hi <;> subst i <;> assumption

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

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ U

Tactic:
let K := J ∪ {i | ¬PathConnectedSpace (Z i)}

Goal state after:
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ U
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
⊢ LocallyPathConnectedSpace ↑S

Tactic:
by
  refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨t, ht⟩ ↦ mem_of_superset ht.1.1 ht.2⟩⟩⟩
  let ⟨t, ht⟩ := (mem_nhds_subtype S x s).mp hs
  let ⟨t', ht'⟩ := (LocallyConvexSpace.convex_basis (𝕜 := ℝ) x.1).mem_iff.mp ht.1
  refine ⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩
  · exact continuousAt_subtype_val.preimage_mem_nhds ht'.1.1
  · refine Subtype.preimage_coe_self_inter _ _ ▸ IsPathConnected.preimage_coe ?_ inter_subset_left
    exact (hS.inter ht'.1.2).isPathConnected ⟨x, x.2, mem_of_mem_nhds ht'.1.1⟩

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
x : E
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (preimage ⇑f)

Tactic:
nhds_induced

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
x : E
⊢ (comap (⇑f) (𝓝 (f x))).HasBasis (fun s ↦ s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (preimage ⇑f)
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✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign r * SignType.sign (w₂ i) = SignType.sign r * SignType.sign (w₂ j)

Tactic:
hij

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign r * SignType.sign (w₂ j) = SignType.sign r * SignType.sign (w₂ j)
Module: Mathlib.Topology.Algebra.Module.UniformConvergence

Goal state before:
pp: case hsmul
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
⊢ ∀ {i : Set E}, i ∈ 𝓝 0 → ∃ V ∈ 𝓝 0, ∃ j ∈ 𝓝 0, V • {u | ∀ (x : α), φ u x ∈ j} ⊆ {u | ∀ (x : α), φ u x ∈ i}

Tactic:
intro U hU

Goal state after:
case hsmul
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∃ j ∈ 𝓝 0, V • {u | ∀ (x : α), φ u x ∈ j} ⊆ {u | ∀ (x : α), φ u x ∈ U}
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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ x ∈ t₁, x ∉ t₂ → w₁ x = 0
⊢ ∑ y ∈ t₁ ∩ t₂, w₁ y = 1

Tactic:
rwa [sum_subset inter_subset_left]

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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ x ∈ t₁, x ∉ t₂ → w₁ x = 0
⊢ ∀ x ∈ t₁, x ∉ t₁ ∩ t₂ → w₁ x = 0
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ x ∈ t₁, x ∉ t₂ → w₁ x = 0
⊢ ∑ y ∈ t₁ ∩ t₂, w₁ y • y = x

Tactic:
rwa [sum_subset inter_subset_left]

Goal state after:
case 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ x ∈ t₁, x ∉ t₂ → w₁ x = 0
⊢ ∀ x ∈ t₁, x ∉ t₁ ∩ t₂ → w₁ x • x = 0
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
hw' : 0 < ∑ i ∈ t with w i ≠ 0, w i
⊢ (∑ i ∈ t with w i ≠ 0, w i) • f y ≤ ∑ i ∈ t with w i ≠ 0, w i • (f ∘ p) i

Tactic:
← smul_le_smul_iff_of_pos_left (inv_pos.2 hw'),

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✝⁴ : 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
hw' : 0 < ∑ i ∈ t with w i ≠ 0, w i
⊢ (∑ i ∈ t with w i ≠ 0, w i)⁻¹ • (∑ i ∈ t with w i ≠ 0, w i) • f y ≤
    (∑ i ∈ t with w i ≠ 0, w i)⁻¹ • ∑ i ∈ t with w i ≠ 0, w i • (f ∘ p) i
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 ι
x : 𝕜
U : Set F
hU : U ∈ p.basisSets
⊢ ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y ↦ x • y) ⁻¹' U

Tactic:
by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  rw [hU]
  by_cases h : x ≠ 0
  · rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero]
    use (s.sup p).ball 0 (r / ‖x‖)
    exact ⟨p.basisSets_mem s (div_pos hr (norm_pos_iff.mpr h)), Subset.rfl⟩
  refine ⟨(s.sup p).ball 0 r, p.basisSets_mem s hr, ?_⟩
  simp only [not_ne_iff.mp h, Set.subset_def, mem_ball_zero, hr, mem_univ, map_zero, imp_true_iff,
    preimage_const_of_mem, zero_smul]

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

Goal state before:
pp: case refine_1.refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ id ((p i).ball 0 ε) ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε

Tactic:
· rw [id, (p i).ball_zero_eq_preimage_ball]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ id ((s.sup p).ball 0 r) ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]

Goal state after:
case refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ ∀ i ∈ s, (p i).ball 0 r ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)
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
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0

Tactic:
congrm _ = ⨅ i, ?_

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ comap (⇑(p i)) (𝓝 0) = 𝓝 0
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
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0

Tactic:
congrm _ = ⨅ i, ?_

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ comap (⇑(p i)) (𝓝 0) = 𝓝 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
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : U ∈ 𝓝 0
⊢ ∀ᶠ (f : E →SLᵤ[σ, 𝔖] F) in 𝓝 0, MapsTo (⇑f) s U

Tactic:
rw [nhds_zero_eq]

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)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : U ∈ 𝓝 0
⊢ ∀ᶠ (f : E →SLᵤ[σ, 𝔖] F) in ⨅ s ∈ 𝔖, ⨅ t ∈ 𝓝 0, 𝓟 {f | MapsTo (⇑f) s t}, MapsTo (⇑f) s U
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
R : Type u_6
inst✝⁵ : SeminormedRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : DistribMulAction R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
⊢ IsVonNBounded R (image2 (fun f x ↦ f x) S s)

Tactic:
intro U hU

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
R : Type u_6
inst✝⁵ : SeminormedRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : DistribMulAction R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
⊢ Absorbs R U (image2 (fun f x ↦ f x) S s)
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : Nontrivial F'
τ : 𝕜 →+* ℝ
inst✝² : FunLike 𝓕' E F'
inst✝¹ : SemilinearMapClass 𝓕' τ E F'
inst✝ : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
h : sphere x r ⊆ Set.range ⇑f
⊢ Function.Surjective ⇑f

Tactic:
grw [← (closedBall_subset_range_iff_surjective x hr), ← convexHull_sphere_eq_closedBall x hr.le,
    convexHull_mono h, (convexHull_eq_self (𝕜 := ℝ) (s := Set.range ↑f)).mpr]

Goal state after:
𝕜 : Type u_1
E : Type u_4
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : Nontrivial F'
τ : 𝕜 →+* ℝ
inst✝² : FunLike 𝓕' E F'
inst✝¹ : SemilinearMapClass 𝓕' τ E F'
inst✝ : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
h : sphere x r ⊆ Set.range ⇑f
⊢ Convex ℝ (Set.range ⇑f)
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 σ₁₂
𝕜' : Type u_9
inst✝³ : DistribSMul 𝕜' F
inst✝² : SMulCommClass 𝕜₂ 𝕜' F
inst✝¹ : SeminormedAddCommGroup 𝕜'
inst✝ : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖c • f x✝‖ ≤ ‖c‖ * ‖f‖ * ‖x✝‖

Tactic:
norm_smul_le,

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 σ₁₂
𝕜' : Type u_9
inst✝³ : DistribSMul 𝕜' F
inst✝² : SMulCommClass 𝕜₂ 𝕜' F
inst✝¹ : SeminormedAddCommGroup 𝕜'
inst✝ : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖c‖ * ‖f x✝‖ ≤ ‖c‖ * ‖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
⊢ ‖f‖₊ = sInf {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}

Tactic:
ext
  rw [NNReal.coe_sInf, coe_nnnorm, norm_def, NNReal.coe_image]
  simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_ofPred_eq, NNReal.coe_mk,
    exists_prop]

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
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
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
let _ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup

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
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ Inseparable (f x) (f' x)

Tactic:
by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm

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

Goal state before:
pp: case mp
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ b, ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≥ a) → b ≥ a) →
    ∃ x,
      ∃ (hx : 0 ≤ x),
        ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
          (∀ᶠ (a : ι) in f, ↑(NNReal.mk x_1 hx_1) ≤ ↑(u a)) → ↑(NNReal.mk x_1 hx_1) ≤ ↑(NNReal.mk x hx)

Tactic:
rintro ⟨b, hb⟩
    exact ⟨b, hb _ (by simp), fun x _ ↦ hb _⟩

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

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
ha₀,

Goal state after:
case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ limsup (fun x ↦ 0 * u x) f = 0 * limsup u f
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun x ↦ a * u x) f = a * liminf u f

Tactic:
ha₀,

Goal state after:
case pos
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun x ↦ 0 * u x) f = 0 * liminf u f
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f g : α →ₘ[μ] β
h : ↑f =ᵐ[μ] ↑g
⊢ mk ↑f ⋯ = g

Tactic:
← g.mk_coeFn,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f g : α →ₘ[μ] β
h : ↑f =ᵐ[μ] ↑g
⊢ mk ↑f ⋯ = mk ↑g ⋯