mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ =
    generateFrom
      ((preimage fun x ↦ {x}) '' powerset '' {U | IsOpen[inst✝] U} ∪
        (preimage fun x ↦ {x}) '' (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U})

Tactic:
image_image,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ =
    generateFrom
      ((fun x ↦ (fun x ↦ {x}) ⁻¹' 𝒫 x) '' {U | IsOpen[inst✝] U} ∪
        (fun x ↦ (fun x ↦ {x}) ⁻¹' {s | (s ∩ x).Nonempty}) '' {U | IsOpen[inst✝] U})
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < ↑‖a‖₊⁻¹
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1

Tactic:
coe_lt_coe,

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : r < ‖a‖₊⁻¹
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Module: Mathlib.Topology.UniformSpace.Closeds

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
this : {U | IsOpen[inst✝¹] U} = (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}
⊢ generateFrom
      (powerset '' (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V} ∪
        (fun V ↦ {s | (s ∩ V).Nonempty}) '' (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}) =
    generateFrom
      ((preimage fun x ↦ f '' x) '' powerset '' {V | IsOpen[inst✝] V} ∪
        (preimage fun x ↦ f '' x) '' (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V})

Tactic:
image_image,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
this : {U | IsOpen[inst✝¹] U} = (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}
⊢ generateFrom
      ((fun x ↦ 𝒫 (f ⁻¹' x)) '' {V | IsOpen[inst✝] V} ∪
        (fun x ↦ {s | (s ∩ f ⁻¹' x).Nonempty}) '' {V | IsOpen[inst✝] V}) =
    generateFrom
      ((fun x ↦ (fun x ↦ f '' x) ⁻¹' 𝒫 x) '' {V | IsOpen[inst✝] V} ∪
        (fun x ↦ (fun x ↦ f '' x) ⁻¹' {s | (s ∩ x).Nonempty}) '' {V | IsOpen[inst✝] V})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case pos
α : 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
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty

Tactic:
wlog htU : t ⊆ U generalizing U V

Goal state after:
case pos.inr
α : 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
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
this :
  ∀ (U V : Set α),
    IsOpen[inst✝] U →
      IsOpen[inst✝] V →
        ⋃₀ s ⊆ U ∪ V → t ⊆ U ∨ t ⊆ V → t ⊆ U → (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty
htU : ¬t ⊆ U
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty

α : 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
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
htU : t ⊆ U
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}

Tactic:
simp_rw [ofPred_and, ofPred_forall]

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen ({a | ↑a ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x | (↑x ∩ i).Nonempty})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
⊢ ∀
    t ∈
      preimage SetLike.coe '' powerset '' {U | IsOpen[inst✝³] U} ∪
        preimage SetLike.coe '' (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝³] U},
    ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
image_image,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
⊢ ∀
    t ∈
      (fun x ↦ SetLike.coe ⁻¹' 𝒫 x) '' {U | IsOpen[inst✝³] U} ∪
        (fun x ↦ SetLike.coe ⁻¹' {s | (s ∩ x).Nonempty}) '' {U | IsOpen[inst✝³] U},
    ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Module: Mathlib.Analysis.CStarAlgebra.Exponential

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)

Tactic:
Commute,

Goal state after:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ SemiconjBy (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b) (selfAdjoint.expUnitary b)
Module: Mathlib.Analysis.CStarAlgebra.Exponential

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ SemiconjBy (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b) (selfAdjoint.expUnitary b)

Tactic:
SemiconjBy,

Goal state after:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
Module: Mathlib.Topology.Sets.VietorisTopology

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

Tactic:
⟨hK₁, hK₂⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : ↑K.toCompacts ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, (↑K.toCompacts ∩ U).Nonempty
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}
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 𝕜
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
⊢ ∀ (i : ℕ), True → ∃ i', True ∧ v i' ⊆ u i

Tactic:
intro n _

Goal state after:
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 𝕜
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
n : ℕ
a✝ : True
⊢ ∃ i', True ∧ v i' ⊆ u n
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
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 𝕜
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
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ u i ⊆ v i'

Tactic:
intro n _

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 𝕜
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
n : ℕ
a✝ : True
⊢ ∃ i, True ∧ u i ⊆ v n
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
W : Type u_3
Q : Type u_4
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : P := Classical.arbitrary P
x y : V
⊢ (⇑(AffineEquiv.vaddConst ℝ (f c)).symm ∘ f ∘ ⇑(AffineEquiv.vaddConst ℝ c)) (midpoint ℝ x y) =
    midpoint ℝ ((⇑(AffineEquiv.vaddConst ℝ (f c)).symm ∘ f ∘ ⇑(AffineEquiv.vaddConst ℝ c)) x)
      ((⇑(AffineEquiv.vaddConst ℝ (f c)).symm ∘ f ∘ ⇑(AffineEquiv.vaddConst ℝ c)) y)

Tactic:
by simp [h]

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
ha : a = -a⁻
⊢ -a⁻ ≤ 0

Tactic:
neg_nonpos

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
ha : a = -a⁻
⊢ 0 ≤ a⁻
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt (a * a) = a

Tactic:
rw [← nnrpow_two _, sqrt_nnrpow_two _]

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

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a = cfcₙ Real.sqrt a

Tactic:
suffices cfcₙ (fun x : ℝ ↦ √x * √x) a = cfcₙ (fun x : ℝ ↦ x) a by
    rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] at this

Goal state after:
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ cfcₙ (fun x ↦ √x * √x) a = cfcₙ (fun x ↦ x) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case frequently
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
⊢ 0 < ε →
    ∃ F,
      Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
        ∀ (y : X), ((cfcHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ ε}

Tactic:
hε

Goal state after:
case frequently
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
⊢ ∃ F,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X), ((cfcHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ ε}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfc f (a x)) t x

Tactic:
refine fun x hx ↦ (ha_cont x hx).cfc (hs x hx) f hx ?_ ?_ (hf x hx)

Goal state after:
case refine_1
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
x : X
hx : x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝[t] x, spectrum 𝕜 (a x_1) ⊆ s x

case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
x : X
hx : x ∈ t
⊢ ∀ᶠ (x : X) in 𝓝[t] x, p (a x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
ha' : 0 ≤ ↑a
⊢ CFC.sqrt ↑a = ↑(CFC.sqrt a)

Tactic:
rw [CFC.sqrt_eq_iff .., ← inr_mul, CFC.sqrt_mul_sqrt_self a]

Goal state after:
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
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
by
  by_cases ha : IsStrictlyPositive a
  · rw [sqrt_eq_rpow, sqrt_eq_rpow, inverse_rpow _ _ (by grind),
        inverse_eq_rpow_neg_one, rpow_rpow _ _ _ (by grind)]
    grind only
  · have ha' : ¬IsUnit (sqrt a) := by rwa [CFC.isUnit_sqrt_iff_isStrictlyPositive]
    obtain (H | H) : ¬0 ≤ a ∨ ¬IsUnit a := by grind
    · rw [sqrt_of_not_nonneg H, inverse_zero]
      by_cases hunit : IsUnit a
      · have h₂ : ¬0 ≤ inverse a := by grind [CFC.ringInverse_nonneg_iff_nonneg_of_isUnit]
        rw [sqrt_of_not_nonneg h₂]
      · simp [inverse_non_unit _ hunit]
    · simp [inverse_non_unit _ ha', inverse_non_unit _ H]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ Unitization.inr '' {a | 0 ≤ a} = {a | 0 ≤ a} ∩ Set.range Unitization.inr

Tactic:
ext a

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
a : Unitization ℂ A
⊢ a ∈ Unitization.inr '' {a | 0 ≤ a} ↔ a ∈ {a | 0 ≤ a} ∩ Set.range Unitization.inr
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
this : sqrt a * (1 - e) = 0
⊢ a * e = a

Tactic:
simpa [← mul_assoc, sqrt_mul_sqrt_self a, mul_sub, sub_eq_zero, eq_comm (a := a)]
      using congr(sqrt a * $this)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ ‖x‖ ^ 2 = √‖x * star x‖ ^ 2

Tactic:
simpa [sq] using Eq.symm <| CStarRing.norm_self_mul_star

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : x = 0
⊢ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
h : x = 0
⊢ ∑ i, ⟪x i, x i⟫_A = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ
⊢ 0 < ε → ∃ ia, (0 ≤ ia ∧ ‖ia‖ < 1) ∧ ∀ x ∈ {x | ia ≤ x} ∩ closedBall 0 1, x * m ∈ closedBall m ε

Tactic:
hε

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ
hε : 0 < ε
⊢ ∃ ia, (0 ≤ ia ∧ ‖ia‖ < 1) ∧ ∀ x ∈ {x | ia ≤ x} ∩ closedBall 0 1, x * m ∈ closedBall m ε
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case frequently
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)₀
hf :
  ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
ε : ℝ
⊢ 0 < ε →
    ∃ F,
      Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
        ∀ (y : X), ((cfcₙHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ ε}

Tactic:
hε

Goal state after:
case frequently
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)₀
hf :
  ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
⊢ ∃ F,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X), ((cfcₙHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ ε}