mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) = 0

Tactic:
convert! ih _ _ (Nat.pred_le_pred h)

Goal state after:
case e'_4.e'_4
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
e_2✝ : inst✝.toSemiring = CommRing.toCommSemiring.toSemiring
⊢ ν = ν.pred + 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case pos
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 : R → R
hf0 : f 0 = 0
⊢ Set.EqOn f 0 (σₙ R 0)

Tactic:
simpa [CFC.quasispectrum_zero_eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X

Tactic:
have pderiv_true_x : pderiv true x = 1 := by rw [pderiv_X]; rfl

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
⊢ ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2

Tactic:
have pderiv_true_x : pderiv true x = 1 := by rw [pderiv_X]; rfl

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

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

Tactic:
sup_eq_half_smul_add_add_abs_sub' ℝ

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ 2⁻¹ • (↑f + ↑g + |↑g - ↑f|) ∈ A.topologicalClosure
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 < δ}
⊢ C * ∑ k ∈ Sᶜ, (bernstein n ↑k) x ≤ C * ∑ k ∈ Sᶜ, (↑x - ↑k/ₙ) ^ 2 / δ ^ 2 * (bernstein n ↑k) x

Tactic:
gcongr with k hk
        conv_lhs => rw [← one_mul (bernstein _ _ _)]
        gcongr
        simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)]
          using! hk

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ 𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)

Tactic:
have key : IsUniformInducing (addEquiv 𝕜 A) :=
    antilipschitzWith_addEquiv.isUniformInducing lipschitzWith_addEquiv.uniformContinuous
  rw [← key.comap_uniformity]
  rfl

Goal state after:
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
⊢ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Tactic:
by
  rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℝ, SpectrumRestricts.nnreal_iff]

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

Goal state before:
pp: case l₂
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 ↑s).NeBot
hxφ : φ x = 0
| 𝓝 (x - 0)

Tactic:
← zero_smul K 1,

Goal state after:
case l₂
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 ↑s).NeBot
hxφ : φ x = 0
| 𝓝 (x - 0 • 1)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
V : Set β
⊢ IsOpen[inst✝.toTopologicalSpace] V → (f x₀ ∩ V).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty

Tactic:
hV

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
⊢ (f x₀ ∩ V).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
a✝ : (Set α × Set α) × Set α × Set α
⊢ a✝ ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U) →
    (a✝.1.1 ∪ a✝.1.2, a✝.2.1 ∪ a✝.2.2) ∈ hausdorffEntourage U

Tactic:
⟨h₁, h₂⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
a✝ : (Set α × Set α) × Set α × Set α
h₁ : (a✝.1.1, a✝.2.1) ∈ hausdorffEntourage U
h₂ : (a✝.1.2, a✝.2.2) ∈ hausdorffEntourage U
⊢ (a✝.1.1 ∪ a✝.1.2, a✝.2.1 ∪ a✝.2.2) ∈ hausdorffEntourage U
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
x✝¹ : Set (α × α) × Set (β × β)
U : Set (α × α)
V : Set (β × β)
x✝ : (U, V).1 ∈ 𝓤 α ∧ (U, V).2 ∈ 𝓤 β
hU : (U, V).1 ∈ 𝓤 α
hV : (U, V).2 ∈ 𝓤 β
s₁ : Set α
s₂ : Set β
t₁ : Set α
t₂ : Set β
⊢ ((s₁, s₂), t₁, t₂) ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage V) →
    (((s₁, s₂), t₁, t₂).1.1 ×ˢ ((s₁, s₂), t₁, t₂).1.2, ((s₁, s₂), t₁, t₂).2.1 ×ˢ ((s₁, s₂), t₁, t₂).2.2) ∈
      (hausdorffEntourage ∘ fun i ↦ entourageProd (id i.1) (id i.2)) (U, V)

Tactic:
⟨h₁, h₂⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
x✝¹ : Set (α × α) × Set (β × β)
U : Set (α × α)
V : Set (β × β)
x✝ : (U, V).1 ∈ 𝓤 α ∧ (U, V).2 ∈ 𝓤 β
hU : (U, V).1 ∈ 𝓤 α
hV : (U, V).2 ∈ 𝓤 β
s₁ : Set α
s₂ : Set β
t₁ : Set α
t₂ : Set β
h₁ : (s₁, t₁) ∈ hausdorffEntourage U
h₂ : (s₂, t₂) ∈ hausdorffEntourage V
⊢ (((s₁, s₂), t₁, t₂).1.1 ×ˢ ((s₁, s₂), t₁, t₂).1.2, ((s₁, s₂), t₁, t₂).2.1 ×ˢ ((s₁, s₂), t₁, t₂).2.2) ∈
    (hausdorffEntourage ∘ fun i ↦ entourageProd (id i.1) (id i.2)) (U, V)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
⊢ (s, t) ∈ hausdorffEntourage ((fun x ↦ (f x.1, f x.2)) ⁻¹' U) → (f '' (s, t).1, f '' (s, t).2) ∈ hausdorffEntourage U

Tactic:
⟨h₁, h₂⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
h₁ : (s, t).1 ⊆ SetRel.preimage ((fun x ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).2
h₂ : (s, t).2 ⊆ SetRel.image ((fun x ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).1
⊢ (f '' (s, t).1, f '' (s, t).2) ∈ hausdorffEntourage U
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
⊢ IsOpen[inst✝] V → ⋃₀ s ⊆ U ∪ V → (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty

Tactic:
hV

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
⊢ ⋃₀ s ⊆ U ∪ V → (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : ProperSpace 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ UpperHemicontinuous (quasispectrum 𝕜)

Tactic:
by
  convert!
    upperHemicontinuous_spectrum 𝕜 (WithLp 1 (Unitization 𝕜 A)) |>.comp
      unitization_isometry_inr.continuous
  ext1 a
  rw [Unitization.quasispectrum_eq_spectrum_inr,
    ← AlgEquiv.spectrum_eq (unitizationAlgEquiv 𝕜 (𝕜 := 𝕜) (A := A) |>.symm)]
  congr

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsSemitopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
ha : 0 ≤ a
⊢ cfc f a = cfc (fun x ↦ ↑(f x.toNNReal)) a

Tactic:
apply (SpectrumRestricts.nnreal_of_nonneg ha).cfc_eq_restrict _
    NNReal.isClosedEmbedding_coe ha (.of_nonneg ha)

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ HasDerivAt (fun x ↦ resolvent x k) (resolvent a k ^ 2) a

Tactic:
convert! hasFDerivAt_resolvent (𝕜 := A) hk |>.hasDerivAt

Goal state after:
case e'_9
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ resolvent a k ^ 2 =
    (((ContinuousLinearMap.mulLeftRight A A) (resolvent a ((↑↑(algebraMap 𝕜 A)).1 k)))
        (resolvent a ((↑↑(algebraMap 𝕜 A)).1 k)))
      1
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
⊢ (spectralRadius ℂ (a * a⋆)).toReal = ‖a‖ ^ 2

Tactic:
by
  rw [← norm_star a, ← toReal_spectralRadius_star_mul_self_eq_norm_sq, star_star]

Goal state after:
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 (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ∧ IsCompact s

Tactic:
obtain ⟨L, hL, hLK, hLu⟩ := exists_compact_between K.isCompact (isOpen_sUnion hu₂) hKu₁

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 (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ∧ IsCompact s
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
⊢ expMulMulExp a b x z = x

Tactic:
have hf : Differentiable ℂ (expMulMulExp a b x : ℂ → A) := by unfold expMulMulExp; fun_prop

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
⊢ expMulMulExp a b x z = x
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
⊢ SemiconjBy x (star a) (star b)

Tactic:
suffices key : ∀ z : ℂ, x * exp (z • star a) = exp (z • star b) * x by
    have (a : A) : HasDerivAt (fun z : ℂ ↦ exp (z • a)) a 0 := by
      simpa using hasDerivAt_exp_smul_const a (0 : ℂ)
    apply (this (star a)).const_mul x |>.unique
    simpa [key] using (this (star b)).mul_const x
  intro z
  let _ : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
  let _ := invertibleExp (z • star a)
  simpa [← mul_assoc, ← invOf_exp, expMulMulExp] using
    congr($(expMulMulExp_const h z) * exp (z • star a)).symm

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
⊢ IsClosed (range toBCF)

Tactic:
refine isClosed_iff_clusterPt.mpr fun f hf => ?_
  rw [clusterPt_principal_iff] at hf
  have : Tendsto f (cocompact α) (𝓝 0) := by
    refine Metric.tendsto_nhds.mpr fun ε hε => ?_
    obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
    refine (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp
      (Eventually.of_forall fun x hx => ?_)
    calc
      dist (f x) 0 ≤ dist (g.toBCF x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
      _ < dist g.toBCF f + ε / 2 := add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx
      _ ≤ ε := by grw [mem_ball.1 hg, add_halves ε]
  exact ⟨⟨f.toContinuousMap, this⟩, rfl⟩

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ZeroLEOneClass 𝕜
⊢ ∀ (i : Set E), i ∈ 𝓝 0 ∧ AbsConvex 𝕜 i → ∃ i', (0 ∈ i' ∧ IsOpen[inst✝⁴] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id i

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ZeroLEOneClass 𝕜
⊢ ∀ (i' : Set E), 0 ∈ i' ∧ IsOpen[inst✝⁴] i' ∧ AbsConvex 𝕜 i' → ∃ i, (i ∈ 𝓝 0 ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id i'

Tactic:
· intro s ⟨hs_nhds, hs_balanced, hs_convex⟩
    refine ⟨interior s, ?_, interior_subset⟩
    exact
      ⟨mem_interior_iff_mem_nhds.mpr hs_nhds, isOpen_interior,
        hs_balanced.interior (mem_interior_iff_mem_nhds.mpr hs_nhds), hs_convex.interior⟩

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ZeroLEOneClass 𝕜
⊢ ∀ (i' : Set E), 0 ∈ i' ∧ IsOpen[inst✝⁴] i' ∧ AbsConvex 𝕜 i' → ∃ i, (i ∈ 𝓝 0 ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id i'
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
fr : Dual ℝ E
p : Seminorm 𝕜 E
hp : ∀ (x : E), |fr x| ≤ p x
x : E
hx : ¬fr.extendRCLike x = 0
⊢ ‖(starRingEnd 𝕜) (fr.extendRCLike x)‖ * p x = ‖fr.extendRCLike x‖ * p x

Tactic:
rw [norm_conj]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhds : s ∈ 𝓝 0
⊢ IsBounded (polar 𝕜 s)

Tactic:
by
  obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜
  obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhds
  exact isBounded_closedBall.subset
    (((topDualPairing 𝕜 E).flip.polar_antitone r_ball).trans <|
      polar_ball_subset_closedBall_div ha r_pos)

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist p₁ ((homothety p₁ c) p₂) = ‖c‖ * dist p₁ p₂

Tactic:
by
  simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∈ c.Uᶜ
⊢ approx 0 c x = 1

Tactic:
exact indicator_of_mem hx _

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

Goal state before:
pp: case ha
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a ≤ a'
hr : r ≤ 1
⊢ 0 ≤ 1 - r

Tactic:
exact sub_nonneg.2 hr

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
s : Set (WeakDual 𝕜 E)
⊢ IsVonNBounded 𝕜 s → Bornology.IsBounded s

Tactic:
intro h_vN
    have h_ptwise := (withSeminorms 𝕜 E).isVonNBounded_iff_seminorm_bounded.mp h_vN
    obtain ⟨C, hC⟩ := banach_steinhaus (g := fun i : s ↦ WeakDual.toStrongDual i.val) fun x ↦
      let ⟨M, _, hM⟩ := h_ptwise x
      ⟨M, fun i ↦ le_of_lt (hM i.val i.property)⟩
    rw [← isBounded_toWeakDual_preimage_iff_isBounded, isBounded_iff_forall_norm_le]
    exact ⟨C, fun f hf ↦ hC ⟨StrongDual.toWeakDual f, hf⟩⟩

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
hd : Disjoint s t
P : Set X → Set X → Prop := fun x x_1 ↦ True
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
set c : Urysohns.CU P :=
  { C := s
    U := tᶜ
    P_C_U := trivial
    closed_C := hs
    open_U := ht.isOpen_compl
    subset := disjoint_left.1 hd
    hP := by
      rintro c u c_closed - u_open cu
      rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩
      exact ⟨v, v_open, cv, hv, trivial, trivial⟩ }

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
hd : Disjoint s t
P : Set X → Set X → Prop := fun x x_1 ↦ True
c : Urysohns.CU P := { C := s, U := tᶜ, P_C_U := trivial, closed_C := hs, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
⊢ ∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
obtain ⟨k, k_comp, k_closed, sk, kt⟩ : ∃ k, IsCompact k ∧ IsClosed k ∧ s ⊆ interior k ∧ k ⊆ tᶜ :=
    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left
  rcases exists_continuous_zero_one_of_isCompact hs isOpen_interior.isClosed_compl
    (disjoint_compl_right_iff_subset.mpr sk) with ⟨⟨f, hf⟩, hfs, hft, h'f⟩
  have A : t ⊆ (interior k)ᶜ := subset_compl_comm.mpr (interior_subset.trans kt)
  refine ⟨⟨fun x ↦ 1 - f x, by fun_prop⟩, fun x hx ↦ by simpa using hfs hx,
    fun x hx ↦ by simpa [sub_eq_zero] using (hft (A hx)).symm, ?_, fun x ↦ ?_⟩
  · apply HasCompactSupport.intro' k_comp k_closed (fun x hx ↦ ?_)
    simp only [ContinuousMap.coe_mk, sub_eq_zero]
    apply (hft _).symm
    contrapose hx
    simp only [mem_compl_iff, not_not] at hx
    exact interior_subset hx
  · have : 0 ≤ f x ∧ f x ≤ 1 := by simpa using h'f x
    simp [this]

Goal state after: