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
f : α → E
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : ∀ ⦃a b : ℕ⦄, a ≤ b → u a ≤ u b
u_mem : ∀ (i : ℕ), u i ∈ s
v : ℕ → α := fun i ↦ min (u i) (u n)
⊢ ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))

Tactic:
grind [Finset.sum_congr]

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 : α → E
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)

Tactic:
obtain ⟨n, u, ⟨u_mono, u_mem⟩, hu⟩ : ∃ n u, (Monotone u ∧ ∀ (i : ℕ), u i ∈ s) ∧
      ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) := by
    simpa [eVariationOn, lt_iSup_iff] using h
  have A : ε < eVariationOn f (s ∩ Icc (u 0) (u n)) := by
    apply hu.trans_le
    simp only [Monotone] at u_mono
    let v (i : ℕ) := min (u i) (u n)
    calc ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
    _ = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr]
    _ ≤ eVariationOn f (s ∩ Icc (u 0) (u n)) :=
      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn]) (by grind)
  refine ⟨u 0, u_mem _, u n, u_mem _, ?_, A⟩
  by_contra!
  have : Set.Subsingleton (s ∩ Icc (u 0) (u n)) := by
    intro a ha b hb
    simp only [mem_inter_iff, mem_Icc] at ha hb
    order
  simp [this] at A

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

Goal state before:
pp: 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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
x✝¹ : R
x✝ : x✝¹ ∈ spectrum R a
⊢ f x✝¹ * (f x✝¹)⁻¹ = 1 x✝¹

Tactic:
aesop

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

Goal state before:
pp: 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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
x✝¹ : R
x✝ : x✝¹ ∈ spectrum R a
⊢ (f x✝¹)⁻¹ * f x✝¹ = 1 x✝¹

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
hf_neg : ContinuousOn (fun x ↦ -f x) (spectrum R a)
⊢ ContinuousOn f (spectrum R a)

Tactic:
by simpa using hf_neg.fun_neg

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : UniqueHom R A
inst✝ : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
this : NonUnitalContinuousFunctionalCalculus R A p
⊢ IsClosedEmbedding ⇑(cfcₙHom ha)

Tactic:
rw [cfcₙHom_eq_restrict f ha ((h a).mp ha).1 ((h a).mp ha).2]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : UniqueHom R A
inst✝ : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
this : NonUnitalContinuousFunctionalCalculus R A p
⊢ IsClosedEmbedding ⇑(nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯)
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsSemitopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁴] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁴] ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
this : DenseRange (Set.inclusion ⋯)
⊢ ⇑φ = ⇑ψ

Tactic:
refine Continuous.ext_on this hφ hψ ?_

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsSemitopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁴] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁴] ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
this : DenseRange (Set.inclusion ⋯)
⊢ Set.EqOn (⇑φ) (⇑ψ) (Set.range (Set.inclusion ⋯))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : p a
⊢ a ≤ (algebraMap R A) r

Tactic:
rw [← cfc_id R a]

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : p a
⊢ cfc id a ≤ (algebraMap R A) r
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : p a
⊢ (algebraMap R A) r ≤ a

Tactic:
rw [← cfc_id R a]

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : p a
⊢ (algebraMap R A) r ≤ cfc id a
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν))

Tactic:
simp only [← mul_assoc]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * ↑(ν + 1) * X ^ ν * (1 - X) ^ (n - ν) =
    ↑(n + 1) * ↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r) ∈ R[(toContinuousMapOnAlgHom s) X]

Tactic:
rw [Polynomial.C_eq_algebraMap, AlgHomClass.commutes]
    exact Subalgebra.algebraMap_mem _ r

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✝¹¹ : 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)
hf_neg : ContinuousOn (fun x ↦ -f x) (σₙ R a)
⊢ ContinuousOn f (σₙ R a)

Tactic:
by simpa using hf_neg.fun_neg

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x ∈ Finset.range (n + 1),
    (↑(x * (x - 1)) * bernsteinPolynomial R n x + (1 - ↑(2 * n) * X) * (↑x * bernsteinPolynomial R n x) +
      ↑(n ^ 2) * X ^ 2 * bernsteinPolynomial R n x)

Tactic:
simp only [← mul_assoc]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x ∈ Finset.range (n + 1),
    (↑(x * (x - 1)) * bernsteinPolynomial R n x + (1 - ↑(2 * n) * X) * ↑x * bernsteinPolynomial R n x +
      ↑(n ^ 2) * X ^ 2 * bernsteinPolynomial R n x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case neg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r✝ : ℝ
f : C(X, ℝ)₀
r : ℝ≥0
hr : 0 < ↑r
⊢ φ (-↑r • f).toNNReal - φ (↑r • f).toNNReal = -↑r • (φ f.toNNReal - φ (-f).toNNReal)

Tactic:
simp only [neg_smul, ← smul_def, toNNReal_neg_smul, map_smul, toNNReal_smul, smul_sub,
        sub_neg_eq_add]

Goal state after:
case neg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r✝ : ℝ
f : C(X, ℝ)₀
r : ℝ≥0
hr : 0 < ↑r
⊢ r • φ (-f).toNNReal - r • φ f.toNNReal = -(r • φ f.toNNReal) + r • φ (-f).toNNReal
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✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}

Tactic:
Set.ofPred_and

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed ({a | a 1 = 1} ∩ {a | ∀ (x y : A), a (x * y) = a x * a y})
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
frequently : ∀ (f : C(↑s, 𝕜)₀), (∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g) → p f
f : C(↑s, 𝕜)₀
⊢ p f

Tactic:
by
  refine f.induction_on zero id star_id add mul smul fun h f ↦ frequently f ?_
  have := (ContinuousMapZero.adjoin_id_dense s).closure_eq ▸ Set.mem_univ (x := f)
  exact mem_closure_iff_frequently.mp this |>.mp <| .of_forall h

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ {u : Set α}, IsOpen[inst✝¹] u → IsOpen[inst✝] (kernImage f u)) ↔
    ∀ (u : Set α), IsOpen[inst✝¹] u → IsOpen[inst✝] ((fun x ↦ f ⁻¹' {x}) ⁻¹' Iic u)

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ {u : Set α}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)) ↔
    ∀ (u : Set α), IsClosed[inst✝¹] u → IsClosed[inst✝] ((fun x ↦ f ⁻¹' {x}) ⁻¹' Iic u)

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
x : α
hf : ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
hg : ∀ t ∈ 𝓝ˢ (g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (g x')
⊢ ∀ t ∈ 𝓝ˢ (f x ∪ g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x' ∪ g x')

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuousWithinAt (fun x ↦ f x ∩ u) univ x

Tactic:
exact hf.inter hu

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

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

Tactic:
simp_rw [← isOpen_compl_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : α → Set β
⊢ HasOpenLowerSections f ↔ ∀ (b : β), IsOpen[inst✝] (f ⁻¹' Iic {b}ᶜ)ᶜ
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
F : Set α
hF : IsClosed[inst✝.toTopologicalSpace] F
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 F)

Tactic:
Set.powerset,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
F : Set α
hF : IsClosed[inst✝.toTopologicalSpace] F
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {t | t ⊆ F}
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
⊢ ∃ k ∈ σ a, ↑‖k‖₊ = spectralRadius 𝕜 a

Tactic:
by
  obtain ⟨k, hk, h⟩ := (spectrum.isCompact a).exists_isMaxOn ha continuous_nnnorm.continuousOn
  exact ⟨k, hk, le_antisymm (le_iSup₂ (α := ℝ≥0∞) k hk) (iSup₂_le <| mod_cast h)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ ∀ i ∈ 𝓤 α, ∃ t_1, t_1.Finite ∧ 𝒫 t ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ hausdorffEntourage i}

Tactic:
Set.powerset,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ ∀ i ∈ 𝓤 α, ∃ t_1, t_1.Finite ∧ {t_2 | t_2 ⊆ t} ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ hausdorffEntourage i}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a | s ⊆ i'.preimage a ∧ a ⊆ i'.image s} ∈ 𝓝 s

Tactic:
Set.ofPred_and

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a | s ⊆ i'.preimage a} ∩ {a | a ⊆ i'.image s} ∈ 𝓝 s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ Set.range ⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) = (fun x ↦ x.toProd.1) ⁻¹' {?refine_2.convert_3}

pp: case refine_2.convert_3
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ 𝕜

Tactic:
aesop

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ Function.Injective ⇑ψ

Tactic:
have h₁ : Function.Injective ⇑(codRestrict (cfcₙAux hp₁ a ha) _
          (cfcₙAux_mem_range_inr hp₁ a ha)) :=
        (Set.injective_codRestrict _).mpr (cfcₙAux_injective hp₁ a ha)
      simpa [ψ] using (inrRangeEquiv 𝕜 A).symm.injective.comp h₁

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
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
this :
  ∀ (w : Set (Set α)),
    ↑K ⊆ ⋃₀ w →
      w ⊆ B →
        ⋃₀ w ⊆ V →
          (∀ W ∈ w, (↑K ∩ W).Nonempty) →
            ∃ 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}
hwK : ¬∀ W ∈ w, (↑K ∩ W).Nonempty
⊢ ∃ 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:
refine this {W ∈ w | (↑K ∩ W).Nonempty} (fun x hx => ?_) (by grind) (by grind) (by grind)
      obtain ⟨W, hWw, hxW⟩ := mem_sUnion.mp (hKV hx)
      exact mem_sUnion_of_mem hxW ⟨hWw, x, hx, hxW⟩

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

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

Tactic:
aesop

Goal state after: