mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : LocallyConnectedSpace α
⊢ LocallyConnectedSpace (Compacts α)

Tactic:
by
  rw [locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected]
  have basis := IsTopologicalBasis.isOpen_isPreconnected.compacts (α := α)
  -- We show that the basic open sets induced by a connected basis are connected.
  refine basis.of_isOpen_of_subset (by grind) (fun U hU => ⟨basis.isOpen hU, ?_⟩)
  -- By density, it is enough to show connectedness for finite sets in the basic open set.
  suffices IsPreconnected (U ∩ {K | (K : Set α).Finite}) by
    refine this.subset_closure inter_subset_left ?_
    grw [← (basis.isOpen hU).inter_closure, dense_setOfPred_finite.closure_eq, inter_univ]
  obtain ⟨u, ⟨hu', hu⟩, rfl⟩ := hU
  simp_rw [← ofPred_and, and_assoc]
  let := hu'.fintype
  /- The finite sets in the basic open set are can be written as the unions of finite sets from
  each connected neighborhood. By the continuity of union, these form a connected set. -/
  suffices {K : Compacts α | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (K : Set α).Finite} =
    Finset.univ.sup '' Set.pi univ fun U : u =>
      {K : Compacts α | (K : Set α).Nonempty ∧ (K : Set α).Finite ∧ (K : Set α) ⊆ U} by
    rw [this]
    exact .image
      (isPreconnected_univ_pi fun U => isPreconnected_nonempty_finite_subsets (hu U.2).2)
      _ (by fun_prop)
  apply subset_antisymm
  · exact fun K ⟨hK₁, hK₂, hK₃⟩ => ⟨fun U => ⟨K ∩ U, (hK₃.inter_of_left _).isCompact⟩,
      fun U _ => ⟨hK₂ U U.2, hK₃.inter_of_left _, inter_subset_right⟩, by aesop⟩
  · simp_rw [image_subset_iff, preimage_ofPred_eq, coe_finset_sup, Finset.sup_eq_iSup,
      iSup_eq_iUnion, Finset.mem_univ, iUnion_true, iUnion_subset_iff]
    refine fun f hf => ⟨by grind, fun U hU => ?_, finite_iUnion (by grind)⟩
    obtain ⟨h₁, -, h₂⟩ := hf ⟨U, hU⟩ trivial
    exact h₁.mono (subset_inter (subset_iUnion _ _) h₂)

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

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

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

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ balancedHull ℝ s ⊆ (convexHull ℝ) (s ∪ -s)

Tactic:
intro a ha

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : E
ha : a ∈ balancedHull ℝ s
⊢ a ∈ (convexHull ℝ) (s ∪ -s)
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
S : Subspace ℝ E
f : Dual ℝ ↥S
p : Seminorm ℝ E
hp : ∀ (x : ↥S), f x ≤ p ↑x
⊢ ∀ (x y : E), p (x + y) ≤ p x + p y

Tactic:
· exact fun x y => map_add_le_add p x y

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

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
this : Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ
⊢ φ ∈ ⨆ i, 𝕜 ∙ f i ↔ ∃ s, φ ∈ ⨆ i, 𝕜 ∙ f ↑i

Tactic:
iSup_subtype

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
this : Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ
⊢ φ ∈ ⨆ i, 𝕜 ∙ f i ↔ ∃ s, φ ∈ ⨆ i ∈ s, 𝕜 ∙ f i
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
x : X
f : C(X, R)
⊢ f ∈ idealOfSet R {x}ᶜ ↔ f x = 0

Tactic:
simp only [mem_idealOfSet, compl_compl, Set.mem_singleton_iff, forall_eq]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
x : X
hx : x ∈ mᶜ
n : ℕ
⊢ mᶜ ⊆ (U n ∩ interior m)ᶜ

Tactic:
simpa using inter_subset_right.trans interior_subset

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, 𝕜)
hI : IsClosed ↑I
hI' : I.IsMaximal
x : X
hx : setOfIdeal I = {x}ᶜ
⊢ idealOfSet 𝕜 {x}ᶜ = I

Tactic:
simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using
        congr_arg (idealOfSet 𝕜) hx.symm

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsSelfAdjoint (f i)) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
this : f j * ∑ i ∈ s, f i = 0
⊢ ‖∑ i ∈ insert j s, f i‖₊ = (insert j s).sup fun x ↦ ‖f x‖₊

Tactic:
by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]

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

Goal state before:
pp: A : Type u_2
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
r : ℝ
hr : 0 ≤ r
⊢ SpectrumRestricts (r • a) ⇑ContinuousMap.realToNNReal

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha ⊢

Goal state after:
A : Type u_2
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
⊢ ∀ x ∈ spectrum ℝ (r • a), 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
have h_eq_negPart_a : -(star c * c) = a⁻ ^ 3 := calc
    -(star c * c) = - a⁻ * a * a⁻ := by
      simp only [star_mul, c, mul_assoc, ← mul_assoc (star b), ← a_def, CFC.negPart_def,
        neg_mul, IsSelfAdjoint.cfcₙ (f := (·⁻)).star_eq]
    _ = - a⁻ * (a⁺ - a⁻) * a⁻ :=
      congr(- a⁻ * $(CFC.posPart_sub_negPart a ha) * a⁻).symm
    _ = a⁻ ^ 3 := by simp [mul_sub, pow_succ]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x y z : A
hxy : IsSelfAdjoint (y - x) ∧ QuasispectrumRestricts (y - x) ⇑ContinuousMap.realToNNReal
hyz : IsSelfAdjoint (z - y) ∧ QuasispectrumRestricts (z - y) ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint (z - x) ∧ QuasispectrumRestricts (z - x) ⇑ContinuousMap.realToNNReal

Tactic:
simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
      quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hxy hyz ⊢
    exact ⟨by simpa using hyz.1.add hxy.1, by simpa using hyz.2.nnreal_add hyz.1 hxy.1 hxy.2⟩

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
⊢ Set.EqOn (fun a ↦ a ^ 0) (fun x ↦ 1) (Set.Ici 0)

Tactic:
intro a ha

Goal state after:
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
a : A
ha : a ∈ Set.Ici 0
⊢ (fun a ↦ a ^ 0) a = (fun x ↦ 1) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ LipschitzOnWith 1 (fun f ↦ cfc ((toFun {spectrum R a}) f) a)
    {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}

Tactic:
intro f hf g hg
    simp only
    rw [cfc_apply .., cfc_apply .., isometry_cfcHom (R := R) a ha |>.edist_eq]
    simp only [ENNReal.coe_one, one_mul]
    rw [edist_continuousRestrict_of_singleton hf hg]

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

Goal state before:
pp: case id
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
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦
    (cfcHomSuperset ⋯ ⋯) (ContinuousMap.restrict s (ContinuousMap.id 𝕜))

Tactic:
simp only [cfcHomSuperset_id]
    fun_prop

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
x : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
have : IsStrictlyPositive a := by grind

Goal state after:
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
x : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
this : IsStrictlyPositive a
⊢ sqrt (a ^ x) = a ^ (x / 2)
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
x : ℝ
h : IsUnit a
ha : 0 ≤ a
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
have : IsStrictlyPositive a := by grind

Goal state after:
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
x : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ sqrt a ^ x = a ^ (x / 2)
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
x y z : E
⊢ ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

Tactic:
rw [← star_star (r := ⟪x + y, z⟫)]
  simp only [inner_add_right, star_add, star_inner]

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
a b : A
ha : 0 ≤ a
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
⊢ ‖a‖ ≤ ‖b‖

Tactic:
have hb := ha.trans hab
    simpa only [ge_iff_le, Unitization.norm_inr] using
      this a b (by simpa) (by rwa [Unitization.inr_le_iff a b])

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
a b : A
hb : IsSelfAdjoint b
⊢ a * b * star a ≤ ‖b‖ • (a * star a)

Tactic:
by
  simpa using star_left_conjugate_le_norm_smul (a := star a)

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

Goal state before:
pp: case refine_2
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖⟪‖v‖⁻¹ •> v, v⟫_A‖ = ‖v‖

pp: case refine_3
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖v‖ ∈ upperBounds {x | ∃ w, ∃ (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}

Tactic:
· simp [norm_smul, ← norm_sq_eq, pow_two, ← mul_assoc]

Goal state after:
case refine_3
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖v‖ ∈ upperBounds {x | ∃ w, ∃ (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case pos
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto
    (fun x ↦ (cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict (F ↑x), continuous_toFun := ⋯, map_zero' := ⋯ })
    (comap Subtype.val l) (𝓝 (cfcₙ f a))

Tactic:
rw [cfcₙ_apply ..]

Goal state after:
case pos
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto
    (fun x ↦ (cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict (F ↑x), continuous_toFun := ⋯, map_zero' := ⋯ })
    (comap Subtype.val l)
    (𝓝 ((cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ }))
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖v‖₊

Tactic:
simp_rw [nnnorm_def, Pi.nnnorm_def]
  congr 1 with i : 1
  refine le_antisymm (Finset.sup_le fun j hj => ?_) ?_
  · obtain rfl | hij := eq_or_ne i j
    · rw [diagonal_apply_eq]
    · simp [hij]
  · refine Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))
    rw [diagonal_apply_eq]

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
⊢ ‖fun j ↦ unitOf (A i j)‖₊ = 1

Tactic:
Pi.nnnorm_def,

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
⊢ (Finset.univ.sup fun b ↦ ‖unitOf (A i b)‖₊) = 1
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hN : ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N
hxn : ‖x‖₊ = 1
⊢ ∑ j, ‖A i j‖₊ ≤ N

Tactic:
Pi.nnnorm_def,

Goal state after:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hN : (Finset.univ.sup fun b ↦ ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x b‖₊) ≤ N
hxn : ‖x‖₊ = 1
⊢ ∑ j, ‖A i j‖₊ ≤ N
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case pos
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
⊢ ContinuousOn (fun x ↦ cfcₙ f x) {a | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
rw [continuousOn_iff_continuous_domRestrict]

Goal state after:
case pos
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ({a | p a ∧ quasispectrum 𝕜 a ⊆ s}.domRestrict fun x ↦ cfcₙ f x)
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ᶠ (x : A) in approximateUnit A, IsSelfAdjoint x

Tactic:
· rw [(hasBasis_approximateUnit A).eventually_iff]
      peel (hasBasis_approximateUnit A).ex_mem with x hx
      exact ⟨hx, fun y hy ↦ (hx.1.trans hy.1).isSelfAdjoint⟩

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
⊢ AEStronglyMeasurable (fun x ↦ mkD (f x) g) μ

Tactic:
by
  rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
  refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry f g f_cont
  filter_upwards [f_zero] with x zero_x
  rw [mkD_eq_mkD_of_map_zero _ _ zero_x]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
⊢ { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* (c • M)) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
      map_smul' := ⋯, cont := ⋯ } =
    (RingHom.id ℂ) c •
      { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* M) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
        map_smul' := ⋯, cont := ⋯ }

Tactic:
ext x i
    simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
      WithCStarModule.equiv_symm_pi_apply, _root_.smul_apply,
      WithCStarModule.smul_apply, RingHom.id_apply]
    rw [Matrix.vecMul_smul, Pi.smul_apply]

Goal state after: