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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this✝ : 0 < s.card
u : ℕ → α := fun n ↦ (s.orderEmbOfFin ⋯) ⟨min n (s.card - 1), ⋯⟩
this : ↑s = u '' Iic (s.card - 1)
⊢ BoundedVariationOn f ↑s

Tactic:
have hmono : Monotone u := fun _ _ _ ↦ OrderEmbedding.monotone _ (by grind)

Goal state after:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this✝ : 0 < s.card
u : ℕ → α := fun n ↦ (s.orderEmbOfFin ⋯) ⟨min n (s.card - 1), ⋯⟩
this : ↑s = u '' Iic (s.card - 1)
hmono : Monotone u
⊢ BoundedVariationOn f ↑s
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✝¹⁴ : Semifield S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalSemiring S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra S A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousFunctionalCalculus S A q
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∃ φ,
    Continuous[_, inst✝¹] ⇑φ ∧
      Function.Injective ⇑φ ∧
        φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a ∧
          (∀ (f : C(↑(spectrum R a), R)), spectrum R (φ f) = range ⇑f) ∧ ∀ (f : C(↑(spectrum R a), R)), p (φ f)

Tactic:
refine ⟨((h a).mp ha).2.starAlgHom (cfcHom ((h a).mp ha).1 (R := S)),
      ?hom_continuous, ?hom_injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
    case hom_continuous =>
      exact ((h a).mp ha).2.continuous_starAlgHom (cfcHom_continuous ((h a).mp ha).1)
    case hom_injective =>
      exact ((h a).mp ha).2.starAlgHom_injective (cfcHom_injective ((h a).mp ha).1) halg.injective
    case hom_id => exact ((h a).mp ha).2.starAlgHom_id <| cfcHom_id ((h a).mp ha).1
    case hom_map_spectrum =>
      simp only [SpectrumRestricts.starAlgHom_apply, ← @spectrum.preimage_algebraMap (R := R) S,
        cfcHom_map_spectrum, Set.ext_iff, Set.mem_preimage, Set.mem_range, ContinuousMap.comp_apply,
        ContinuousMap.coe_mk, StarAlgHom.ofId_apply, halg.injective.eq_iff]
      exact fun _ _ ↦ ((h a).mp ha).2.homeomorph.exists_congr fun _ ↦ Iff.rfl
    case predicate_hom =>
      intro g
      rw [h]
      refine ⟨cfcHom_predicate _ _, ?_⟩
      refine .of_rightInvOn (((h a).mp ha).2.left_inv) fun s hs ↦ ?_
      rw [SpectrumRestricts.starAlgHom_apply, cfcHom_map_spectrum] at hs
      obtain ⟨r, rfl⟩ := hs
      simp [((h a).mp ha).2.left_inv _]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : IsSemitopologicalSemiring A
inst✝² : ContinuousStar A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
x y✝ : A
hy✝¹ : y✝ ∈ elemental R x
P : (u : A) → u ∈ elemental R x → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A) r) ⋯
add : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u + v) ⋯
mul : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ ↑(elemental R x)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst✝⁶] s), P v ⋯
y : A
hy✝ : y ∈ ↑(adjoin R {x})
hy : y ∈ Algebra.adjoin R ({x} ∪ star {x})
⊢ P y ⋯

Tactic:
induction hy using Algebra.adjoin_induction with
  | mem u hu =>
    obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu
    · exact self
    · simp_rw [← hu, star_star] at star_self
      exact star_self
  | algebraMap r => exact algebraMap r
  | add u v hu_mem hv_mem hu hv =>
    exact add u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
  | mul u v hu_mem hv_mem hu hv =>
    exact mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Set.Icc a b
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) =
    ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i))

Tactic:
refine sum_congr rfl fun i hi => ?_

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Set.Icc a b
i : ℕ
hi : i ∈ Finset.range n
⊢ edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))
Module: Mathlib.RingTheory.Polynomial.Bernstein

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

Tactic:
by
    simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
      Polynomial.derivative_mul, Polynomial.derivative_natCast, zero_mul,
      Nat.cast_add, algebraMap.coe_one, Polynomial.derivative_X, mul_one, zero_add,
      Polynomial.derivative_sub, Polynomial.derivative_one, zero_sub, mul_neg, Nat.sub_zero,
      bernsteinPolynomial, map_add, map_natCast, Nat.cast_one]

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

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

Tactic:
rw [Nat.lt_succ_iff]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
simp_rw [unitization_norm_def, ofLp_smul, fst_smul, snd_smul, norm_smul, mul_add]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖ ≤ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed[TopologicalSpace.vietoris α] {s | (s ∩ Fᶜᶜ).Nonempty}

Tactic:
inter_compl_nonempty_iff,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed[TopologicalSpace.vietoris α] {s | ¬s ⊆ Fᶜ}
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : ℕ → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
⊢ ∀ᶠ (x : ℕ) in atTop, y x ∈ K

Tactic:
filter_upwards [hx hf] with n hn

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : ℕ → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
n : ℕ
hn : n ∈ x ⁻¹' {x | f x ⊆ K}
⊢ y n ∈ K
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
a : A
k : 𝕜
h : ‖a‖ * ‖1‖ < ‖k‖
a✝ : Nontrivial A
hk : k ≠ 0
ku : Aˣ := (Units.map ↑↑ₐ) (Units.mk0 k hk)
⊢ IsUnit (k • 1 - a)

Tactic:
← inv_inv ‖(1 : A)‖,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * ‖1‖⁻¹⁻¹ < ‖k‖
a✝ : Nontrivial A
hk : k ≠ 0
ku : Aˣ := (Units.map ↑↑ₐ) (Units.mk0 k hk)
⊢ IsUnit (k • 1 - a)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ s ⊆ SetRel.preimage U t

pp: case right
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ t ⊆ SetRel.image U s

Tactic:
· grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]

Goal state after:
case right
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ t ⊆ SetRel.image U s
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ ∀ᶠ (z : 𝕜) in cobounded 𝕜, IsUnit (resolvent a z)

Tactic:
by
  rw [atTop_basis_Ioi.cobounded_of_norm.eventually_iff]
  exact ⟨‖a‖ * ‖(1 : A)‖, trivial, fun _ ↦ isUnit_resolvent.mp ∘ mem_resolventSet_of_norm_lt_mul⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : DiscreteUniformity α
⊢ DiscreteUniformity (Set α)

Tactic:
discreteUniformity_iff_setRelId_mem_uniformity

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : DiscreteUniformity α
⊢ SetRel.id ∈ 𝓤 (Set α)
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_2 | t_2 ⊆ t} ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ hausdorffEntourage i}

Tactic:
Set.ofPred_subset,

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : U ∈ {U | IsOpen[inst✝.toTopologicalSpace] U}
hs' : s ∈ 𝒫 U
⊢ 𝒫 U ∈ 𝓝 s

Tactic:
obtain ⟨V : SetRel α α, hV₁, hV₂⟩ :=
      hs.nhdsSet_basis_uniformity (𝓤 α).basis_sets |>.mem_iff.mp (hU.mem_nhdsSet.mpr hs')
    filter_upwards [UniformSpace.ball_mem_nhds _ (Filter.mem_lift' hV₁)]
      with t ⟨_, ht⟩
    exact ht.trans fun x ⟨y, hy, hxy⟩ => hV₂ <| Set.mem_biUnion hy hxy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
K : Compacts α
⊢ Filter.comap SetLike.coe (𝓝 ↑K) = Filter.comap SetLike.coe (𝓝 ↑K)

Tactic:
K.isCompact.nhds_hausdorff_eq_nhds_vietoris

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
K : NonemptyCompacts α
⊢ Filter.comap SetLike.coe (𝓝 ↑K) = Filter.comap SetLike.coe (𝓝 ↑K)

Tactic:
K.isCompact.nhds_hausdorff_eq_nhds_vietoris

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

Goal state before:
pp: case right.left
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ QuasispectrumRestricts (cfcₙ (fun x ↦ √x) a) ⇑ContinuousMap.realToNNReal

Tactic:
simpa only [QuasispectrumRestricts.nnreal_iff, cfcₙ_map_quasispectrum (√·) a,
      Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
        using fun x _ ↦ Real.sqrt_nonneg x

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} = {a | a = K}

Tactic:
ofPred_eq_eq_singleton

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

Goal state before:
pp: 𝕜 : 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 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
hv_basis : (𝓝 0).HasAntitoneBasis v
m : ℕ
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, v n + v n ⊆ v m

Tactic:
by
      obtain ⟨W, hW_open, hW_zero, hW_add⟩ := exists_open_nhds_zero_add_subset (hv_nhds m)
      obtain ⟨N, hN⟩ := hv_basis.mem_iff.mp (hW_open.mem_nhds hW_zero)
      filter_upwards [Filter.eventually_ge_atTop N] with M hM
      exact (add_subset_add ((hv_basis.antitone hM).trans hN)
        ((hv_basis.antitone hM).trans hN)).trans hW_add

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

Goal state before:
pp: X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
this : ContinuousAt Ring.inverse (f x)
⊢ ContinuousAt (fun x ↦ Ring.inverse (f x)) x

Tactic:
exact this.comp (f.continuousAt x)

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
⊢ CompactSpace ↑(characterSpace 𝕜 A)

Tactic:
rw [← isCompact_iff_compactSpace]
  have h : characterSpace 𝕜 A ⊆ toStrongDual ⁻¹' Metric.closedBall 0 ‖(1 : A)‖ := by
    intro φ hφ
    rw [Set.mem_preimage, mem_closedBall_zero_iff]
    exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ :)
  exact (isCompact_closedBall 0 _).of_isClosed_subset CharacterSpace.isClosed h

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
⊢ approx n c x ≤ approx (n + 1) c x

Tactic:
induction n generalizing c with
  | zero =>
    simp only [approx, right_U, right_le_midpoint]
    exact (approx_mem_Icc_right_left c 0 x).2
  | succ n ihn =>
    rw [approx, approx]
    exact midpoint_le_midpoint (ihn _) (ihn _)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
⊢ a⁺ - (- -a)⁺ = 0

Tactic:
neg_neg,

Goal state after:
A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
⊢ a⁺ - a⁺ = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²³ : CommSemiring R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Ring A
inst✝¹⁵ : Ring B
inst✝¹⁴ : Algebra S A
inst✝¹³ : Algebra S B
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : IsScalarTower R S A
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : StarRing A
inst✝⁷ : StarRing B
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : ContinuousFunctionalCalculus R (A × B) pab
inst✝³ : ContinuousFunctionalCalculus R A pa
inst✝² : ContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMap.UniqueHom R A
inst✝ : ContinuousMap.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (spectrum R a ∪ spectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
⊢ cfc f (a, b) = (cfc f a, cfc f b)

Tactic:
by
  ext
  case fst =>
    let φ := StarAlgHom.fst S A B
    exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_fst hab ha
  case snd =>
    let φ := StarAlgHom.snd S A B
    exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_snd hab hb

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ -a⁻ = - -a ↔ a ≤ 0

Tactic:
neg_neg,

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ -a⁻ = a ↔ a ≤ 0
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ ⨅ i, ⨅ (_ : 0 < i), 𝓟 ((UniformFun.gen α β ∘ fun ε ↦ {p | edist p.1 p.2 ≤ ε}) i) =
    ⨅ i, ⨅ (_ : 0 < i), 𝓟 ((fun x ↦ edist x.1 x.2) ⁻¹' Set.Iic i)

Tactic:
simp [UniformFun.gen, edist_le, Set.Iic]

Goal state after:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ UniformEquicontinuousOn f s

Tactic:
uniformEquicontinuousOn_iff_uniformContinuousOn

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ UniformContinuousOn (⇑ofFun ∘ Function.swap f) s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case add
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a x y : A
x_mem : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
y_mem : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1
hy : ∀ x ∈ spectrum ℝ y, 0 ≤ x
⊢ ∀ x_1 ∈ spectrum ℝ (x + y), 0 ≤ x_1

Tactic:
| add x y x_mem y_mem hx hy =>

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left✝ : QuasispectrumRestricts s ⇑ContinuousMap.realToNNReal
hs₂ : s * s = y - x
⊢ y = x + s * s

Tactic:
eq_sub_iff_add_eq',

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left✝ : QuasispectrumRestricts s ⇑ContinuousMap.realToNNReal
hs₂ : x + s * s = y
⊢ y = x + s * s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
ha' : ¬0 ≤ ↑a
⊢ cfcₙ ⇑NNReal.sqrt ↑a = ↑0

Tactic:
cfcₙ_apply_of_not_predicate _ ha',

Goal state after:
case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
ha' : ¬0 ≤ ↑a
⊢ 0 = ↑0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
⊢ [IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * sqrt a,
      ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b,
      ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a,
      IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE

Tactic:
tfae_have 1 ↔ 8 := IsStrictlyPositive.iff_of_unital
  tfae_have 1 ↔ 9 := ⟨fun h => ⟨h.isSelfAdjoint,
      StarOrderedRing.isStrictlyPositive_iff_spectrum_pos a |>.mp h⟩,
    fun h => (StarOrderedRing.isStrictlyPositive_iff_spectrum_pos a).mpr h.2⟩
  tfae_have 1 → 2 := fun h => ⟨h.sqrt, sqrt_mul_sqrt_self a |>.symm⟩
  tfae_have 2 → 3 := fun h => ⟨h.1.isUnit, h.2⟩
  tfae_have 3 → 4 := fun h => ⟨sqrt a, h.1.isStrictlyPositive (sqrt_nonneg _), h.2⟩
  tfae_have 4 → 5 := fun ⟨b, hb, hab⟩ => ⟨b, hb.isUnit, hb.isSelfAdjoint, hab⟩
  tfae_have 5 → 6 := fun ⟨b, hb, hbsa, hab⟩ => ⟨b, hb, hbsa.symm ▸ hab⟩
  tfae_have 6 → 7 := fun ⟨b, hb, hab⟩ => ⟨star b, hb.star, star_star b |>.symm ▸ hab⟩
  tfae_have 7 → 8 := fun ⟨b, hb, hab⟩ => ⟨hab ▸ mul_star_self_nonneg _, hab ▸ hb.mul hb.star⟩
  tfae_finish

Goal state after: