mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
⊢ (fun y ↦ eVariationOn f (s ∩ Icc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))

Tactic:
ext y

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
y : α
⊢ eVariationOn f (s ∩ Icc x y) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
⊢ (fun y ↦ eVariationOn f (s ∩ Icc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))

Tactic:
ext y

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
y : α
⊢ eVariationOn f (s ∩ Icc x y) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
⊢ (fun y ↦ eVariationOn f (s ∩ Iic y)) = fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ici (toDual y))

Tactic:
ext y

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
y : α
⊢ eVariationOn f (s ∩ Iic y) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ici (toDual y))
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ bernsteinPolynomial ℤ 3 2 = 3 * X ^ 2 - 3 * X ^ 3

Tactic:
by
  norm_num [bernsteinPolynomial, choose]
  ring

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

Goal state before:
pp: a b : ℝ
h : a < b
⊢ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) =
    polynomialFunctions (Set.Icc a b)

Tactic:
ext f

Goal state after:
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) ↔
    f ∈ polynomialFunctions (Set.Icc a b)
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((⇑derivative)^[n - ν] (bernsteinPolynomial R n ν)) = (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Tactic:
by
  rw [flip' _ _ _ h]
  simp only [iterate_derivative_comp_one_sub_X, eval_mul, eval_pow, eval_neg, eval_one, eval_comp,
    eval_sub, eval_X, sub_self, iterate_derivative_at_0]
  obtain rfl | h' := h.eq_or_lt
  · simp
  · norm_cast
    congr
    lia

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

Goal state before:
pp: case inl
a b : ℝ
h : a < b
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
let W : C(Set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) :=
      compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm
    -- This operation is itself a homeomorphism
    -- (with respect to the norm topologies on continuous functions).
    let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := (iccHomeoI a b h).arrowCongr (.refl _)
    have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
    -- Thus we take the statement of the Weierstrass approximation theorem for `[0,1]`,
    have p := polynomialFunctions_closure_eq_top'
    -- and pullback both sides, obtaining an equation between subalgebras of `C([a,b], ℝ)`.
    apply_fun fun s => s.comap W at p
    simp only [Algebra.comap_top] at p
    -- Since the pullback operation is continuous, it commutes with taking `topologicalClosure`,
    rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p
    -- and precomposing with an affine map takes polynomial functions to polynomial functions.
    rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p
    -- 🎉
    exact p

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ f a ≤ 0 ↔ ∀ x ∈ σₙ R a, f x ≤ 0

Tactic:
simp_rw [← neg_nonneg, ← cfcₙ_neg]
  exact cfcₙ_nonneg_iff (fun x ↦ -f x) a

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

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
x : ↑(σₙ R a)
hx : ↑x ∈ spectrum R a ∪ {0}
⊢ f x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0}

Tactic:
obtain (hx | hx) := hx

Goal state after:
case mpr.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
x : ↑(σₙ R a)
hx : ↑x ∈ spectrum R a
⊢ f x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0}

case mpr.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
x : ↑(σₙ R a)
hx : ↑x ∈ {0}
⊢ f x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0}
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := { toFun := fun x ↦ |↑x|, continuous_toFun := ⋯ }
⊢ |↑f| ∈ A.topologicalClosure

Tactic:
change abs.comp f' ∈ A.topologicalClosure

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := { toFun := fun x ↦ |↑x|, continuous_toFun := ⋯ }
⊢ abs.comp f' ∈ A.topologicalClosure
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
⊢ φ = ψ

Tactic:
ext f

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
f : C(X, ℝ≥0)
⊢ φ f = ψ f
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
⊢ φ = ψ

Tactic:
ext f

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
f : C(X, ℝ≥0)₀
⊢ φ f = ψ f
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
⊢ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) =
    ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
ext f

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
⊢ f ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) ↔
    f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuous f ↔ ∀ (u : Set β), IsClosed[inst✝] u → IsClosed[inst✝¹] (f ⁻¹' Iic uᶜ)ᶜ

Tactic:
conv_rhs =>
    rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]
  exact upperHemicontinuous_iff_isOpen_preimage_Iic

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

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
⊢ ∀ᶠ (x : A) in map (⇑(val S)) l, Ring.inverse x ∈ ↑S

Tactic:
rw [Filter.eventually_map]

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
⊢ ∀ᶠ (a : ↥S) in l, Ring.inverse ((val S) a) ∈ ↑S
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
⊢ IsPathConnected {0}ᶜ

Tactic:
convert!
        (((convex_halfSpace_im_gt 0).isPathConnected ⟨.I, by simp⟩).union
              ((convex_halfSpace_re_gt 0).isPathConnected ⟨1, by simp⟩) ⟨1 + .I, by simp⟩).union
          (((convex_halfSpace_im_lt 0).isPathConnected ⟨-.I, by simp⟩).union
            ((convex_halfSpace_re_lt 0).isPathConnected ⟨-1, by simp⟩) ⟨-1 - .I, by simp⟩)
          ⟨1 - .I, by simp⟩ using 1

Goal state after:
r : ℝ
⊢ {0}ᶜ = {c | 0 < c.im} ∪ {c | 0 < c.re} ∪ ({c | c.im < 0} ∪ {c | c.re < 0})
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
x : ℂ
⊢ x ∈ {0}ᶜ ↔ x ∈ {c | 0 < c.im} ∪ {c | 0 < c.re} ∪ ({c | c.im < 0} ∪ {c | c.re < 0})

Tactic:
refine ⟨?_, by aesop⟩

Goal state after:
r : ℝ
x : ℂ
⊢ x ∈ {0}ᶜ → x ∈ {c | 0 < c.im} ∪ {c | 0 < c.re} ∪ ({c | c.im < 0} ∪ {c | c.re < 0})
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ spectralRadius ℂ a = ↑‖a‖₊

Tactic:
refine tendsto_nhds_unique ?_ hconst

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 (spectralRadius ℂ a))
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ spectralRadius ℂ a = ↑‖a‖₊

Tactic:
by
  have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds
  refine tendsto_nhds_unique ?_ hconst
  convert!
    (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
      (tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using 1
  refine funext fun n => ?_
  rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_natCast, ← rpow_mul]
  simp

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

Goal state before:
pp: case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ ‖(cfcHom ha) { toFun := (σ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ }‖₊ ≤ c

Tactic:
simp only [← cfc_apply f a, isLUB_le_iff (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.isLUB)]

Goal state after:
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ c ∈ upperBounds (f '' σ ℝ≥0 a)
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 : α → Compacts β
g : α → β → γ
hf : Continuous[inst✝², _] f
hg : Continuous[instTopologicalSpaceProd, inst✝] (Function.uncurry g)
⊢ Continuous[inst✝², _] fun x ↦ Compacts.map (g x) ⋯ (f x)

Tactic:
by
  conv in Compacts.map _ _ _ => equals ({x} ×ˢ f x).map g.uncurry hg => ext; simp
  have := hg.compacts_map
  fun_prop

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✝ : DiscreteTopology α
K : Compacts α
⊢ {K} = {K_1 | ↑K_1 ⊆ ↑K} ∩ ⋂ i ∈ ↑K, {K | (↑K ∩ {i}).Nonempty}

Tactic:
simp_rw [← ofPred_forall, inter_singleton_nonempty, ← Set.subset_def, ← ofPred_and,
    ← subset_antisymm_iff, SetLike.coe_set_eq, ofPred_eq_eq_singleton]

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
x : α
hx₁ : x ∈ ↑K
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {K | ↑K ⊆ W} ∈ 𝓝ˢ {a | (↑a ∩ U).Nonempty}ᶜ

Tactic:
(isOpen_subsets_of_isOpen hW).mem_nhdsSet,

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
x : α
hx₁ : x ∈ ↑K
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {a | (↑a ∩ U).Nonempty}ᶜ ⊆ {K | ↑K ⊆ W}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
h : ⋃ K ∈ S, ↑K ⊆ ⋃ i, U i
⊢ ∃ t, ⋃ K ∈ S, ↑K ⊆ ⋃ i ∈ t, U i

Tactic:
iUnion₂_subset_iff

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
h : ∀ i ∈ S, ↑i ⊆ ⋃ i, U i
⊢ ∃ t, ⋃ K ∈ S, ↑K ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ CompactSpace (Compacts α) ↔ CompactSpace α

Tactic:
refine ⟨fun h => ⟨?_⟩, fun _ => inferInstance⟩
  convert! isCompact_biUnion_coe_of_isCompact (α := α) isCompact_univ
  symm
  simp_rw [biUnion_univ, eq_univ_iff_forall, mem_iUnion]
  exact fun x => ⟨{x}, Set.mem_singleton x⟩

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

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
hKL : K ≤ L
⊢ Icc K L = (fun x ↦ K ⊔ x) '' {K | (↑K).Nonempty ∧ ↑K ⊆ ↑L}

Tactic:
exact subset_antisymm
    (fun M hM => ⟨M, ⟨Compacts.coe_nonempty.mpr (ne_bot_of_le_ne_bot hK hM.1), hM.2⟩,
      sup_eq_right.mpr hM.1⟩)
    (image_subset_iff.mpr fun M ⟨_, hM⟩ => ⟨le_sup_left, sup_le hKL hM⟩)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
⊢ B.polar ↑m = {y | ∀ x ∈ m, (B x) y = 0}

Tactic:
ext y

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
⊢ y ∈ B.polar ↑m ↔ y ∈ {y | ∀ x ∈ m, (B x) y = 0}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ CompactSpace (NonemptyCompacts α) ↔ CompactSpace α

Tactic:
refine ⟨fun h => ⟨?_⟩, fun _ => inferInstance⟩
  convert! isCompact_biUnion_coe_of_isCompact (α := α) isCompact_univ
  symm
  simp_rw [biUnion_univ, eq_univ_iff_forall, mem_iUnion]
  exact fun x => ⟨{x}, Set.mem_singleton x⟩

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace (NonemptyCompacts α)
x : α
U : Set α
x✝ : x ∈ U ∧ IsOpen[inst✝] U
hx : x ∈ U
hU : IsOpen[inst✝] U
V : Set (NonemptyCompacts α)
hV₁ : IsOpen V
hV₂ : IsPreconnected V
hxV : {x} ∈ V
hKV : V ⊆ {K | ↑K ⊆ U}
⊢ ⋃ L ∈ V, ↑L ⊆ U

Tactic:
iUnion₂_subset_iff

Goal state after:
case refine_3
α : Type u_1
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace (NonemptyCompacts α)
x : α
U : Set α
x✝ : x ∈ U ∧ IsOpen[inst✝] U
hx : x ∈ U
hU : IsOpen[inst✝] U
V : Set (NonemptyCompacts α)
hV₁ : IsOpen V
hV₂ : IsPreconnected V
hxV : {x} ∈ V
hKV : V ⊆ {K | ↑K ⊆ U}
⊢ ∀ i ∈ V, ↑i ⊆ U
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f ((lineMap b a) r') ≤ (lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f ((lineMap b a) r') b

Tactic:
simp_rw [lineMap_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul]

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔
    (b - a)⁻¹ • (f b - f a) ≤ (b - (r' * (a - b) + b))⁻¹ • (f b - f (r' * (a - b) + b))
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < (1 - r) * (b - a)
⊢ f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a b ≤ slope f ((lineMap a b) r) b

Tactic:
rw [← lineMap_apply_one_sub, ← lineMap_apply_one_sub _ _ r]
  revert h; generalize 1 - r = r'; clear! r; intro h
  simp_rw [lineMap_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul]
  rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_mul_neg, neg_sub,
    le_inv_smul_iff_of_pos h, smul_smul, mul_inv_cancel_right₀, le_sub_comm, ← neg_sub (f b),
    smul_neg, neg_add_eq_sub]
  · exact right_ne_zero_of_mul h.ne'

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

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a ((lineMap a b) r) ≤ slope f ((lineMap a b) r) b

Tactic:
by
  rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
    lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]

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, 𝕜)
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)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, 0 < g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, 0 < g₂ x
⊢ (↑(algebraMapCLM ℝ≥0 𝕜)).comp (g₁ + g₂) = (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ + (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂

Tactic:
ext y

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, 𝕜)
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)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, 0 < g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, 0 < g₂ x
y : X
⊢ ((↑(algebraMapCLM ℝ≥0 𝕜)).comp (g₁ + g₂)) y = ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ + (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂) y
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_3.refine_2
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)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, 0 < g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, 0 < g₂ x
x : X
hx : x ∈ s₁ ∪ s₂
⊢ 0 < (g₁ + g₂) x

Tactic:
rcases hx with (hx | hx)
        · simpa using add_lt_add_of_lt_of_le (hgt₁ x hx) zero_le
        · simpa using add_lt_add_of_le_of_lt zero_le (hgt₂ x hx)

Goal state after: