mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h : ¬(p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0)
⊢ cfcₙ f a = cfcₙ g a

Tactic:
· simp only [not_and_or] at h
    obtain (ha | hg | h0) := h
    · simp [cfcₙ_apply_of_not_predicate a ha]
    · rw [cfcₙ_apply_of_not_continuousOn a hg, cfcₙ_apply_of_not_continuousOn]
      exact fun hf ↦ hg (hf.congr hfg.symm)
    · rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero]
      exact fun hf ↦ h0 (hfg (quasispectrum.zero_mem R a) ▸ hf)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
hE : Nonempty E
f : α → E
hf : BoundedVariationOn f univ
⊢ ∃ x, Tendsto f atTop (𝓝 x)

Tactic:
simpa using hf.exists_tendsto_atTop

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
⊢ eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s

Tactic:
apply iSup_le _
  rintro ⟨n, ⟨u, hu, us⟩⟩
  calc
    (∑ i ∈ Finset.range n, edist (f (g (u (i + 1)))) (f (g (u i)))) ≤
        ∑ i ∈ Finset.range n, C * edist (g (u (i + 1))) (g (u i)) :=
      Finset.sum_le_sum fun i _ => h (hg (us _)) (hg (us _))
    _ = C * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i)) := by rw [Finset.mul_sum]
    _ ≤ C * eVariationOn g s := by grw [eVariationOn.sum_le hu us]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < n - ν → eval 1 ((⇑derivative)^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
intro w
  rw [flip' _ _ _ (tsub_pos_iff_lt.mp (pos_of_gt w)).le]
  simp [Polynomial.eval_comp, iterate_derivative_at_0_eq_zero_of_lt R n w]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr.inl.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ ¬ContinuousOn (fun x ↦ -f x) (σₙ R a)

Tactic:
exact fun hf_neg ↦ hf <| by simpa using hf_neg.fun_neg

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
hn₀ : n ≠ 0
x : ↑I
S : Finset (Fin (n + 1)) := {k | dist k/ₙ x < δ}
⊢ ∑ k ∈ S, (bernstein n ↑k) x * (1 / 2) = 1 / 2 * ∑ k ∈ S, (bernstein n ↑k) x

Tactic:
rw [mul_comm, Finset.sum_mul]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ A.topologicalClosure

Tactic:
rw [subalgebra_topologicalClosure_eq_top_of_separatesPoints A w]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ ⊤
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : 0 < ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖
this :
  ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ *
      ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖ *
      ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖

Tactic:
exact (mul_le_mul_iff_left₀ h).mp this

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
this : x - (algebraMap 𝕜 A) (ψ x) ∈ RingHom.ker φ
⊢ φ x = ψ x

Tactic:
RingHom.mem_ker,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
this : φ (x - (algebraMap 𝕜 A) (ψ x)) = 0
⊢ φ x = ψ x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ LowerHemicontinuous fun x ↦ {x}

Tactic:
intro x t ⟨ht, hne⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
t : Set α
ht : IsOpen[inst✝] t
hne : ((fun x ↦ {x}) x ∩ t).Nonempty
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x t ↦ IsOpen[inst✝] t ∧ ((fun x ↦ {x}) x ∩ t).Nonempty) x' t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
s : Set α
hs : s ∈ ⋂₀ t
⊢ ∃ v ∈ (fun u ↦ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ v ∧ v ⊆ ⋂₀ t

Tactic:
exists_mem_image

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
s : Set α
hs : s ∈ ⋂₀ t
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsTopologicalBasis ((fun u ↦ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U})

Tactic:
by
  refine isTopologicalBasis_of_subbasis rfl |>.isTopologicalBasis_of_exists_subset ?_ ?_ <;>
    rw [forall_mem_image]
  · intro u ⟨hu₁, hu₂⟩
    simp_rw [ofPred_and, ofPred_forall]
    exact (isOpen_sUnion hu₂).powerset_vietoris.inter <|
      hu₁.isOpen_biInter fun U hU => isOpen_inter_nonempty_of_isOpen (hu₂ U hU)
  · intro t ⟨ht₁, ht₂⟩ s hs
    rw [exists_mem_image]
    rcases eq_empty_or_nonempty s with rfl | _
    · exists ∅; simpa
    obtain ⟨u, v, hu, hv, rfl⟩ : ∃ u v, u ⊆ powerset '' {U | IsOpen U} ∧
        v ⊆ (fun V => {s | (s ∩ V).Nonempty}) '' {U | IsOpen U} ∧ u ∪ v = t := by
      rw [← inter_eq_left, inter_union_distrib_left] at ht₂
      exact ⟨_, _, inter_subset_right, inter_subset_right, ht₂⟩
    rw [finite_union] at ht₁
    obtain ⟨u, hu₁, hu₂, rfl⟩ := exists_subset_image_finite_and.mp ⟨u, hu, ht₁.1, rfl⟩
    obtain ⟨v, hv₁, hv₂, rfl⟩ := exists_subset_image_finite_and.mp ⟨v, hv, ht₁.2, rfl⟩
    let U := ⋂₀ u
    have hU : IsOpen U := hu₂.isOpen_sInter hu₁
    simp_rw [sInter_union, show ⋂₀ (powerset '' u) = U.powerset by ext; simp [U], sInter_image]
      at hs ⊢
    rw [mem_inter_iff, mem_powerset_iff, mem_iInter₂] at hs
    exists insert U ((U ∩ ·) '' v)
    simp_rw [show ⋃₀ (insert U ((U ∩ ·) '' v)) = U by simp, mem_ofPred, finite_insert,
      forall_mem_insert, forall_mem_image, ← inter_assoc, inter_eq_left.mpr hs.1]
    refine ⟨⟨hv₂.image _, hU, fun V hV => hU.inter (hv₁ hV)⟩, by grind,
      fun t ⟨htU, _, ht⟩ => ⟨htU, mem_iInter₂_of_mem ?_⟩⟩
    simpa only [inter_eq_left.mpr htU] using! ht

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ ∃
    v ∈
      (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
        {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
    s ∈ v ∧ v ⊆ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
exists_mem_image

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ ∃ x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
    s ∈ {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} ∧
      {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} ⊆ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ IsUniformInducing closure[inst✝.toTopologicalSpace]

Tactic:
refine ⟨le_antisymm ?_ <| Filter.map_le_iff_le_comap.mp uniformContinuous_closure⟩
  rw [(𝓤 α).basis_sets.uniformity_hausdorff.comap _ |>.le_basis_iff
    (𝓤 α).basis_sets.uniformity_hausdorff, Function.comp_id]
  intro U hU
  obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU
  refine ⟨V, hV, fun ⟨s, t⟩ ⟨hst, hts⟩ => ?_⟩
  simp only [mem_hausdorffEntourage] at *
  constructor
  · grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]
  · grw [subset_closure (s := t), hts, closure_subset_image hV s, ← hVU, SetRel.image_comp]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
simp_rw [nhds_eq_comap_uniformity,
    uniformity_hasBasis_open.uniformity_hausdorff |>.comap _ |>.ge_iff, Function.comp_id,
    hausdorffEntourage, Set.preimage_ofPred_eq, Set.ofPred_and]
  intro U ⟨hU₁, hU₂⟩
  have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
  let := TopologicalSpace.vietoris α
  refine Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
    SetRel.self_subset_image _
  obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁
  obtain ⟨t, ht₁, ht₂⟩ := hs.exists_prodMk_finset_mem_hausdorffEntourage hV₁
  dsimp only at ht₁ ht₂
  filter_upwards [(Filter.eventually_all_finset t).mpr fun x hx =>
    isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (ht₁ hx)]
    with u (hu : ↑t ⊆ V.preimage ↑u)
  grw [ht₂, ← SetRel.preimage_eq_image, hu, ← hVU, SetRel.preimage_comp]

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
hw : w.Finite
huw : u ⊆ w
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
exists_mem_image

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
hw : w.Finite
huw : u ⊆ w
⊢ ∃ x ∈ {u | u.Finite ∧ u ⊆ B},
    K ∈ {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ∧
      {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU :
  ∃ t ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝³] U},
    K ∈ t ∧ t ⊆ U
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s

Tactic:
exists_mem_image

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU :
  ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝³] U},
    K ∈ {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ∧ {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ⊆ U
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
Module: Mathlib.Analysis.Convex.TotallyBounded

Goal state before:
pp: E : Type u_1
s : Set E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
obtain ⟨t', htf', hts'⟩ := totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
    (htf.isCompact_convexHull ℝ).totallyBounded _ hV₁

Goal state after:
E : Type u_1
s : Set E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : (convexHull ℝ) t ⊆ ⋃ y ∈ t', y +ᵥ V
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsOpen (range toCompacts)

Tactic:
rw [range_toCompacts]
    exact Compacts.isClopen_singleton_bot.compl.isOpen

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : ↑K.toCompacts ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, (↑K.toCompacts ∩ U).Nonempty
hu' : u.Nonempty
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}

Tactic:
exists_mem_image

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : ↑K.toCompacts ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, (↑K.toCompacts ∩ U).Nonempty
hu' : u.Nonempty
⊢ ∃ x ∈ {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B},
    K ∈ {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ∧
      {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ⊆ toCompacts ⁻¹' {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module ℝ E
inst✝ : PolynormableSpace ℝ E
S : Subspace ℝ E
f : Dual ℝ ↥S
p : Seminorm ℝ E
hp_cont : Continuous[inst✝², _] ⇑p
hp : ∀ (x : ↥S), f x ≤ p ↑x
g : Dual ℝ E
hg : ∀ (x : ↥S), g ↑x = f x
hl : ∀ (x : E), |g x| ≤ p x
⊢ ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), |g x| ≤ p x

Tactic:
exact ⟨⟨g, (PolynormableSpace.withSeminorms ℝ E).continuous_real_rng g
    ⟨{⟨p, hp_cont⟩}, 1, fun x ↦ by simpa using (le_abs_self _).trans (hl x)⟩⟩, hg, hl⟩

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

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ Continuous[t₁, _] ⇑((normSeminorm 𝕜 𝕜).comp φ) ↔ ∃ s, Continuous[t₂ s, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)

Tactic:
conv in Continuous _ => rw [Seminorm.continuous_iff one_pos, nhds_iInf]

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ ((normSeminorm 𝕜 𝕜).comp φ).ball 0 1 ∈ ⨅ i, 𝓝 0 ↔ ∃ s, Continuous[t₂ s, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
⊢ Continuous[inst✝³, _] ⇑p

Tactic:
have h₁ : ∀ n : ℕ, IsClosed (p.closedBall (0 : E) n) := fun n ↦ by
      simpa [p.closedBall_zero_eq] using! hp.isClosed_preimage n

Goal state after:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
h₁ : ∀ (n : ℕ), IsClosed[inst✝³] (p.closedBall 0 ↑n)
⊢ Continuous[inst✝³, _] ⇑p
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
P : Type u_3
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
⊢ edist (k • x +ᵥ c) (k • y +ᵥ c) = ↑‖k‖₊ * edist x y

Tactic:
rw [show edist (k • x +ᵥ c) (k • y +ᵥ c) = _ from (IsometryEquiv.vaddConst c).isometry ..]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
P : Type u_3
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
⊢ edist (k • x) (k • y) = ↑‖k‖₊ * edist x y
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : x ∈ (setOfIdeal I)ᶜᶜ
⊢ ∃ t_1 ∈ nhdsWithin x t, ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t_1, 0 < g' x

Tactic:
rw [compl_compl, mem_setOfIdeal] at hx

Goal state after:
case refine_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : ∃ f ∈ I, f x ≠ 0
⊢ ∃ t_1 ∈ nhdsWithin x t, ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t_1, 0 < g' x
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (⇑g) 0 (closure sᶜ)
hgx : Set.EqOn (⇑g) 1 {x}
⊢ ∀ ⦃x : X⦄, x ∈ sᶜ → { toFun := fun x ↦ ↑(g x), continuous_toFun := ⋯ } x = 0

Tactic:
simpa only [coe_mk, ofReal_eq_zero] using! fun x hx => hgs (subset_closure hx)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
⊢ I.IsMaximal → ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Tactic:
intro hI'

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : I.IsMaximal
⊢ ∃ x, idealOfSet 𝕜 {x}ᶜ = I