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✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU : U ∈ 𝓝 K
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s

Tactic:
rw [isTopologicalBasis.mem_nhds_iff, exists_mem_image] at hU

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU :
  ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝³] U},
    K ∈ {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ∧ {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ⊆ U
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) =
    ↑⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩⁻¹

Tactic:
← Unitary.val_inv_toUnits_apply,

Goal state after:
case e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) =
    ↑(Unitary.toUnits ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩)⁻¹
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)
⊢ ∃ x,
    (𝓝 0).HasAntitoneBasis x ∧
      ∀ (n : ℕ),
        IsOpen[inst✝⁵] (x n) ∧ AbsConvex 𝕜 (x n) ∧ x (n + 1) + x (n + 1) ⊆ x n ∧ closure[inst✝⁵] (x (n + 1)) ⊆ x n

Tactic:
have hv_nhds (n : ℕ) : v n ∈ 𝓝 0 := (hv_open n).mem_nhds (subset_absConvexHull (hu_zero n))

Goal state after:
𝕜 : 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
⊢ ∃ x,
    (𝓝 0).HasAntitoneBasis x ∧
      ∀ (n : ℕ),
        IsOpen[inst✝⁵] (x n) ∧ AbsConvex 𝕜 (x n) ∧ x (n + 1) + x (n + 1) ⊆ x n ∧ closure[inst✝⁵] (x (n + 1)) ⊆ x n
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : CompactSpace (NonemptyCompacts α)
⊢ ∀ (x : α), ∃ i, x ∈ ↑i

Tactic:
exact fun x => ⟨{x}, Set.mem_singleton x⟩

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

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

Tactic:
by
  refine ⟨fun h => ?_, fun h => inferInstance⟩
  rw [preconnectedSpace_iff_clopen] at h ⊢
  intro s hs
  apply h _ ⟨isClosed_subsets_of_isClosed hs.isClosed, isOpen_subsets_of_isOpen hs.isOpen⟩ |>.imp
  · simp only [Set.eq_empty_iff_forall_notMem]
    exact fun h x hx => h {x} (Set.singleton_subset_iff.mpr hx)
  · simp only [Set.eq_univ_iff_forall]
    exact fun h x => Set.singleton_subset_iff.mp (h {x})

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

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

Tactic:
exact vietoris.isPreconnected_biUnion hV₂ (by fun_prop) ⟨{x}, hxV, isPreconnected_singleton⟩

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : NormedField L
inst✝ : NormedAlgebra K L
F : IntermediateField K L
⊢ ∃ x, 1 < ‖x‖

Tactic:
obtain ⟨k, hk⟩ := @NontriviallyNormedField.non_trivial K _

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : NormedField L
inst✝ : NormedAlgebra K L
F : IntermediateField K L
k : K
hk : 1 < ‖k‖
⊢ ∃ x, 1 < ‖x‖
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r : k
h : a < b
⊢ b ≤ (lineMap a b) r ↔ 1 ≤ r

Tactic:
by
  rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_one]

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

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r : k
h : a < b
⊢ (lineMap a b) r ≤ b ↔ r ≤ 1

Tactic:
by
  rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_one]

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

Goal state before:
pp: A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ I.toCharacterSpace a = 0

Tactic:
unfold Ideal.toCharacterSpace

Goal state after:
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ (CharacterSpace.equivAlgHom.symm ((↑(NormedRing.algEquivComplexOfComplete ⋯).symm).comp (Quotient.mkₐ ℂ I))) a = 0
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c : Urysohns.CU P := { C := closure[inst✝¹] u, U := tᶜ, P_C_U := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ EqOn c.lim 1 t

Tactic:
· intro x hx
    apply Urysohns.CU.lim_of_notMem_U
    exact notMem_compl_iff.mpr hx

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
x : A
φ : ↑(characterSpace ℂ ↥(elemental ℂ x))
⊢ φ ⟨x, ⋯⟩ ∈ spectrum ℂ x

Tactic:
simpa only [StarSubalgebra.spectrum_eq (hS := isClosed ℂ x)
      (a := ⟨x, self_mem ℂ x⟩)] using AlgHom.apply_mem_spectrum φ ⟨x, self_mem ℂ x⟩

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C(↑(σₙ ℂ a), ℂ)₀
⊢ ‖(inrNonUnitalStarAlgHom ℂ A) ((cfcₙHom ha) f)‖ = ‖f‖

Tactic:
← NonUnitalStarAlgHom.comp_apply,

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C(↑(σₙ ℂ a), ℂ)₀
⊢ ‖((inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha)) f‖ = ‖f‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case zero
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ∀ x ∈ spectrum ℝ 0, 0 ≤ x

Tactic:
nontriviality A
      simp

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

Goal state before:
pp: case mpr.add
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝¹ : PartialOrder A := spectralOrder A
x✝ p x y : A
hx✝ : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hy✝ : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : IsSelfAdjoint ↑x ∧ SpectrumRestricts ↑x ⇑ContinuousMap.realToNNReal
hy : IsSelfAdjoint ↑y ∧ SpectrumRestricts ↑y ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint ↑(x + y) ∧ SpectrumRestricts ↑(x + y) ⇑ContinuousMap.realToNNReal

Tactic:
rw [Unitization.inr_add]

Goal state after:
case mpr.add
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝¹ : PartialOrder A := spectralOrder A
x✝ p x y : A
hx✝ : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hy✝ : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : IsSelfAdjoint ↑x ∧ SpectrumRestricts ↑x ⇑ContinuousMap.realToNNReal
hy : IsSelfAdjoint ↑y ∧ SpectrumRestricts ↑y ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint (↑x + ↑y) ∧ SpectrumRestricts (↑x + ↑y) ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case pos
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
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
a✝ : Nontrivial A
hf : ContinuousOn (fun x ↦ x ^ y) (spectrum ℝ≥0 a)
h0 : 0 ∈ spectrum ℝ≥0 a
h : y = 0
⊢ False

Tactic:
exact hy h

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

Goal state before:
pp: A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a

Tactic:
by
  have ha' := QuasispectrumRestricts.nnreal_of_nonneg ha
  have : (σₙ ℝ a).EqOn (fun x ↦ ((f x.toNNReal - g x.toNNReal : ℝ≥0) : ℝ))
      (fun x ↦ f x.toNNReal - g x.toNNReal) :=
    fun x hx ↦ NNReal.coe_sub <| hfg _ <| ha'.apply_mem hx
  rw [cfcₙ_nnreal_eq_real .., cfcₙ_nnreal_eq_real .., cfcₙ_nnreal_eq_real .., cfcₙ_congr this]
  refine cfcₙ_sub _ _ a ?_ (by simpa) ?_
  all_goals
    exact continuous_subtype_val.comp_continuousOn <|
      ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

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

Goal state before:
pp: case pos
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
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : IsUnit a
h₂ : ¬0 ≤ a⁻¹ʳ
⊢ sqrt a⁻¹ʳ = 0

Tactic:
sqrt_of_not_nonneg h₂

Goal state after:
case pos
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
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : IsUnit a
h₂ : ¬0 ≤ a⁻¹ʳ
⊢ 0 = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfc f) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
refine ContinuousOn.congr ?_ this

Goal state after:
A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
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
⊢ ∀ {a : A} {x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)}, ∑ i, ⟪x i, (a • y) i⟫_A = a * ∑ i, ⟪x i, y i⟫_A

Tactic:
simp [mul_sum]

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
⊢ (∀ (m : A), Tendsto (fun x ↦ m * x) l (𝓝 m)) ↔ ∀ (m : A), Tendsto (fun x ↦ x * m) l (𝓝 m)

Tactic:
refine ⟨fun h m ↦ ?_, fun h m ↦ ?_⟩
  all_goals
    apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'
    filter_upwards [hl] with x hx
    simp [hx.star_eq]

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

Goal state before:
pp: case a
B₁ : Type u_3
B₂ : Type u_4
inst✝⁵ : CStarAlgebra B₁
inst✝⁴ : CStarAlgebra B₂
inst✝³ : PartialOrder B₁
inst✝² : PartialOrder B₂
inst✝¹ : StarOrderedRing B₁
inst✝ : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ x ≤ ↑‖x‖ • 1

Tactic:
← Algebra.algebraMap_eq_smul_one

Goal state after:
case a
B₁ : Type u_3
B₂ : Type u_4
inst✝⁵ : CStarAlgebra B₁
inst✝⁴ : CStarAlgebra B₂
inst✝³ : PartialOrder B₁
inst✝² : PartialOrder B₂
inst✝¹ : StarOrderedRing B₁
inst✝ : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ x ≤ (algebraMap ℂ B₁) ↑‖x‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalNormedRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : NormedSpace ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : ContinuousStar A
inst✝⁵ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
hf0 : f 0 = 0
this : Set.EqOn (cfcₙ f) (cfcₙ fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (fun x ↦ cfcₙ f x) {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}

Tactic:
refine ContinuousOn.congr ?_ this

Goal state after:
A : Type u_2
inst✝¹¹ : NonUnitalNormedRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : NormedSpace ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : ContinuousStar A
inst✝⁵ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
hf0 : f 0 = 0
this : Set.EqOn (cfcₙ f) (cfcₙ fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfcₙ fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : ContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (univ ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ HasFiniteIntegral (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ

Tactic:
exact hasFiniteIntegral_mkD_restrict_of_bound f _ this bound bound_int bound_ge

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

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : ContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ HasFiniteIntegral (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) (μ.restrict s)

Tactic:
exact hasFiniteIntegral_mkD_restrict_of_bound f _ this bound bound_int bound_ge

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

Goal state before:
pp: A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (fun x ↦ cfc x a) '' (fun x ↦ cfc x a) ⁻¹' {a | 0 ≤ a} ⊆ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}

Tactic:
rintro _ ⟨f, hf, rfl⟩

Goal state after:
A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : f ∈ (fun x ↦ cfc x a) ⁻¹' {a | 0 ≤ a}
⊢ (fun x ↦ cfc x a) f ∈ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module ℝ A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : SMulCommClass ℝ A A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : IsTopologicalRing A
inst✝⁷ : T2Space A
inst✝⁶ : PartialOrder A
inst✝⁵ : NonnegSpectrumClass ℝ A
inst✝⁴ : StarOrderedRing A
inst✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (fun x ↦ cfcₙ x a) '' (fun x ↦ cfcₙ x a) ⁻¹' {a | 0 ≤ a} ⊆
    (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}

Tactic:
rintro _ ⟨f, hf, rfl⟩

Goal state after:
A : Type u_1
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module ℝ A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : SMulCommClass ℝ A A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : IsTopologicalRing A
inst✝⁷ : T2Space A
inst✝⁶ : PartialOrder A
inst✝⁵ : NonnegSpectrumClass ℝ A
inst✝⁴ : StarOrderedRing A
inst✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : f ∈ (fun x ↦ cfcₙ x a) ⁻¹' {a | 0 ≤ a}
⊢ (fun x ↦ cfcₙ x a) f ∈ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(((rankOne 𝕜) x) y)).rank = 1

Tactic:
LinearMap.rank,

Goal state after:
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ Module.rank 𝕜 ↥(↑(((rankOne 𝕜) x) y)).range = 1
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ((innerₛₗ 𝕜) 0).toAddMonoidHom = 0

Tactic:
ext x; exact inner_zero_left _

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
⊢ a = e

Tactic:
have ⟨ha01, hb01⟩ : (a : A⁺¹) ∈ Icc 0 1 ∧ (b : A⁺¹) ∈ Icc 0 1 := by
      grind [inr_mem_Icc_iff_norm_le]
    suffices t • (e * (1 - a : A⁺¹) * e) = 0 by
      rw [← h0t.ne'.isUnit.smul_left_cancel, ← he.conjugate_of_nonneg_of_le
          (smul_nonneg h0t.le ha) ?hae]
      case hae => simpa [hlin] using le_add_of_nonneg_right (a := t • a) (by positivity : 0 ≤ s • b)
      apply inr_injective (R := ℂ) <| Eq.symm ?_
      simpa only [mul_one_sub_mul, he.inr.isIdempotentElem.eq, smul_sub, sub_eq_zero,
        smul_mul_assoc, mul_smul_comm, smul_sub, inr_mul, inr_smul]
    apply le_antisymm ?_ <| smul_nonneg h0t.le <| he.inr.isSelfAdjoint.conjugate_nonneg <| by
      simpa using ha01.2
    calc
      _ ≤ t • (e * (1 - a : A⁺¹) * e) + s • (e * (1 - b) * e) := by
        refine le_add_of_nonneg_right <| smul_nonneg h0s.le ?_
        simpa [mul_one_sub_mul] using he.inr.isSelfAdjoint.conjugate_le_conjugate <|
          norm_le_one_iff_of_nonneg (b : A⁺¹) (by simpa) |>.mp (by simpa [norm_inr])
      _ = e - e * (t • a + s • b) * e := by
        simp only [mul_one_sub_mul, he.inr.isIdempotentElem.eq, smul_sub, mul_add,
          Algebra.mul_smul_comm, add_mul, Algebra.smul_mul_assoc]
        match_scalars <;> grind
      _ = 0 := by simp [← inr_smul, ← inr_add, hlin, ← inr_mul, he.isIdempotentElem.eq]

Goal state after: