mathlib-initiative/mathlib-tactics huggingface dataset:
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 : 0 ≤ a
⊢ cfcₙ (fun x ↦ x⁺) a = cfcₙ id a

Tactic:
refine cfcₙ_congr (fun x hx ↦ ?_)

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 : 0 ≤ a
x : ℝ
hx : x ∈ quasispectrum ℝ a
⊢ x⁺ = id x
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
h : LipschitzWith K fun x ↦ ofFun fun c ↦ f c x
⊢ UniformContinuous (⇑ofFun ∘ Function.swap f)

Tactic:
exact h.uniformContinuous

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst✝ : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) fun x ↦ (toFun 𝔖) (f x) c
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, topologicalSpace α β 𝔖] f

Tactic:
rw [UniformOnFun.continuous_rng_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst✝ : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) fun x ↦ (toFun 𝔖) (f x) c
⊢ ∀ s ∈ 𝔖,
    Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, UniformFun.topologicalSpace (↑s) β]
      (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖) ∘ f)
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst✝ : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) fun x ↦ (toFun 𝔖) (f x) c
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, topologicalSpace α β 𝔖] f

Tactic:
rw [UniformOnFun.continuous_rng_iff]
  refine fun s hs ↦ LipschitzWith.continuous (K := K s) ?_
  rw [UniformFun.lipschitzWith_iff]
  rintro ⟨y, hy⟩
  exact h s hs y hy

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))

Tactic:
exact isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ ‖a⁺‖ ≤ ‖a‖

Tactic:
by_cases ha : IsSelfAdjoint a

Goal state after:
case pos
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖a⁺‖ ≤ ‖a‖

case neg
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ ‖a⁺‖ ≤ ‖a‖
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
h : 0 ^ y ≠ 0
hf : ContinuousOn (fun x ↦ x ^ y) (spectrum ℝ≥0 a)
h0 : 0 ∈ spectrum ℝ≥0 a
⊢ False

Tactic:
simp only [ne_eq, NNReal.rpow_eq_zero_iff, true_and, Decidable.not_not] at 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
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
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 b : A
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * a = b * b ↔ a = b

Tactic:
mul_self_eq_mul_self_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 : A
⊢ 0 ≤ ↑a ↔ 0 ≤ a

Tactic:
by_cases ha : IsSelfAdjoint a

Goal state after:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ 0 ≤ ↑a ↔ 0 ≤ a

case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ ↑a ↔ 0 ≤ a
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 : ContinuousOn a t
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)
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
rw [ContinuousOn] at ha_cont ⊢
  refine fun x hx ↦ (ha_cont x hx).cfc (hs x hx) f hx ?_ ?_ (hf x hx)
  all_goals filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt
  exacts [hx, ha' x hxt]

Goal state after:
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 : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum 𝕜 (a x) ⊆ s
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
refine ContinuousOn.cfc _ (fun _ _ ↦ hs) ha_cont (fun _ _ ↦ ?_) ha'
  filter_upwards [self_mem_nhdsWithin] with x hx
  exact ha x hx

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
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
⊢ ConvexOn ℝ s (cfcₙ f)

Tactic:
by
  let inrl : A →ₗ[ℝ] A⁺¹ := inrHom ℝ ℂ A
  by_cases hf₀ : f 0 = 0
  case neg =>
    have : (cfcₙ f : A → A) = fun _ => 0 := by
      ext x
      simp [cfcₙ_apply_of_not_map_zero _ hf₀]
    rw [this]
    refine convexOn_const _ ?_
    have : Convex ℝ (inrl ⁻¹' inrl '' s) := Convex.linear_preimage hf.1 _
    rwa [Set.preimage_image_eq _ inrHom_injective] at this
  refine convexOn_of_convexOn_inr_comp (fun _ => IsSelfAdjoint.cfcₙ) ?_
  have h₁ : inr (R := ℂ) ∘ (cfcₙ f) = fun x : A => ((cfcₙ f x : A) : A⁺¹) := rfl
  have h₂ : (fun x : A => ((cfcₙ f x : A) : A⁺¹))
      = fun x : A => cfc f (x : A⁺¹) := by ext1; rw [real_cfcₙ_eq_cfc_inr ..]
  rw [h₁, h₂]
  have h₃ : ConvexOn ℝ (inrl ⁻¹' inrl '' s) ((cfc f) ∘ inrl) :=
    ConvexOn.comp_linearMap (g := inrl) hf
  rwa [Set.preimage_image_eq _ inrHom_injective] at h₃

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

Goal state before:
pp: 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
x y : E
⊢ ‖⟪x, y⟫_A‖ ≤ ‖x‖ * ‖y‖

Tactic:
have := calc ‖⟪x, y⟫‖ ^ 2 = ‖⟪x, y⟫ * ⟪y, x⟫‖ := by
                rw [← star_inner x, CStarRing.norm_self_mul_star, pow_two]
    _ ≤ ‖‖x‖ ^ 2 • ⟪y, y⟫‖ := by
                refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le
                rw [← star_inner x]
                exact mul_star_self_nonneg ⟪x, y⟫_A
    _ = ‖x‖ ^ 2 * ‖⟪y, y⟫‖ := by simp [norm_smul]
    _ = ‖x‖ ^ 2 * ‖y‖ ^ 2 := by
                simp only [norm_eq_sqrt_norm_inner_self (A := A), norm_nonneg, Real.sq_sqrt]
    _ = (‖x‖ * ‖y‖) ^ 2 := by simp only [mul_pow]
  refine (pow_le_pow_iff_left₀ (norm_nonneg ⟪x, y⟫_A) ?_ (by simp)).mp this
  exact mul_nonneg (CStarModule.norm_nonneg A) (CStarModule.norm_nonneg A)

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‖ = √‖x * star x‖

Tactic:
← sq_eq_sq₀ (norm_nonneg _) (by positivity)

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ ‖x‖ ^ 2 = √‖x * star x‖ ^ 2
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
inst✝ : DecidableEq ι
i : ι
y : E i
⊢ ‖(equiv A ((j : ι) → E j)).symm (Pi.single i y)‖ = ‖y‖

Tactic:
let _ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, Π i, E i) := normedAddCommGroup A

Goal state after:
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
inst✝ : DecidableEq ι
i : ι
y : E i
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ‖(equiv A ((j : ι) → E j)).symm (Pi.single i y)‖ = ‖y‖
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)
i : ι
⊢ ‖x i‖ ≤ ‖x‖

Tactic:
let _ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, Π i, E i) := normedAddCommGroup A

Goal state after:
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)
i : ι
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ‖x i‖ ≤ ‖x‖
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)
⊢ ‖(equiv A ((i : ι) → E i)) x‖ ≤ ‖x‖

Tactic:
let _ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, Π i, E i) := normedAddCommGroup A

Goal state after:
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)
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ‖(equiv A ((i : ι) → E i)) x‖ ≤ ‖x‖
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✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist
      { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) f), continuous_toFun := ⋯,
        map_zero' := hf0 }
      { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) g), continuous_toFun := ⋯,
        map_zero' := hg0 } ≤
    edist f g

Tactic:
← ContinuousMapZero.isometry_toContinuousMap.edist_eq,

Goal state after:
case pos
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✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist
      { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) f), continuous_toFun := ⋯,
          map_zero' := hf0 }.toContinuousMap
      { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) g), continuous_toFun := ⋯,
          map_zero' := hg0 }.toContinuousMap ≤
    edist f g
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst✝¹³ : NonUnitalCStarAlgebra A₁
inst✝¹² : NonUnitalCStarAlgebra A₂
inst✝¹¹ : PartialOrder A₁
inst✝¹⁰ : StarOrderedRing A₁
inst✝⁹ : PartialOrder A₂
inst✝⁸ : StarOrderedRing A₂
inst✝⁷ : CStarAlgebra B₁
inst✝⁶ : CStarAlgebra B₂
inst✝⁵ : PartialOrder B₁
inst✝⁴ : PartialOrder B₂
inst✝³ : StarOrderedRing B₁
F : Type u_5
inst✝² : FunLike F A₁ A₂
inst✝¹ : LinearMapClass F ℂ A₁ A₂
inst✝ : OrderHomClass F A₁ A₂
f : F
⊢ ∃ C, ∀ (a : A₁), ‖f a‖ ≤ C * ‖a‖

Tactic:
obtain ⟨C, h⟩ := exists_norm_apply_le (.ofClass f)

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst✝¹³ : NonUnitalCStarAlgebra A₁
inst✝¹² : NonUnitalCStarAlgebra A₂
inst✝¹¹ : PartialOrder A₁
inst✝¹⁰ : StarOrderedRing A₁
inst✝⁹ : PartialOrder A₂
inst✝⁸ : StarOrderedRing A₂
inst✝⁷ : CStarAlgebra B₁
inst✝⁶ : CStarAlgebra B₂
inst✝⁵ : PartialOrder B₁
inst✝⁴ : PartialOrder B₂
inst✝³ : StarOrderedRing B₁
F : Type u_5
inst✝² : FunLike F A₁ A₂
inst✝¹ : LinearMapClass F ℂ A₁ A₂
inst✝ : OrderHomClass F A₁ A₂
f : F
C : ℝ≥0
h : ∀ (a : A₁), ‖(ofClass f) a‖ ≤ ↑C * ‖a‖
⊢ ∃ C, ∀ (a : A₁), ‖f a‖ ≤ C * ‖a‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case id
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
⊢ Commute ((cfcₙHom ha) (ContinuousMapZero.id (quasispectrum 𝕜 a))) b

Tactic:
cfcₙHom_id ha

Goal state after:
case id
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
⊢ Commute a b
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
s : Set X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
⊢ AEStronglyMeasurable (fun x ↦ mkD (f x) g) (μ.restrict s)

Tactic:
by
  rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
  refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry hs 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.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
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
inst✝ : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum ℝ≥0 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfcₙ f (a x)

Tactic:
by
  rw [← continuousOn_univ] at ha_cont ⊢
  exact ha_cont.cfcₙ_nnreal' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' x)

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

Goal state before:
pp: 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✝² : 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
⊢ IntegrableOn (fun x ↦ cfc (f x) a) s μ

Tactic:
refine integrableOn_cfc' _ _ ⟨?_, ?_⟩ ha
  · exact aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs _ _ hf
  · refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ bound bound_int bound_ge
    exact ae_restrict_of_forall_mem hs fun x hx ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ ‖star (M i j) * M i j‖ = 0

Tactic:
← toCLM_apply_single_apply

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ ‖(toCLM M) ((WithCStarModule.equiv A (m → A)).symm (Pi.single i (star (M i j)))) j‖ = 0
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ ‖star (M i j) * M i j‖ ≤ ‖M‖ * ‖M i j‖

Tactic:
← toCLM_apply_single_apply

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ ‖(toCLM M) ((equiv A (m → A)).symm (Pi.single i (star (M i j)))) j‖ ≤ ‖M‖ * ‖M i j‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ spectrum ℂ ↑(ℜ a) = (fun x ↦ ↑x.re) '' spectrum ℂ a

Tactic:
by
  rw [← cfc_re_id a, cfc_map_spectrum ..]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (B v) w
⊢ f = B♯ v

Tactic:
refine ext_inner_right 𝕜 ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (B v) w
⊢ ∀ (v_1 : E), ⟪f, v_1⟫ = ⟪B♯ v, v_1⟫
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ ↑‖(↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x‖ ^ 2 ≤ ↑(‖a‖ ^ 2 * ‖x‖ ^ 2)

Tactic:
RCLike.ofReal_eq_complex_ofReal,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ ↑‖(↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x‖ ^ 2 ≤ ↑(‖a‖ ^ 2 * ‖x‖ ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:

Tactic:
_ ≤ f (‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x) := by
        simpa using OrderHomClass.mono f this
      _ = _ := by simp [← Complex.coe_smul, preGNS_norm_sq, smul_mul_assoc]

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
⊢ (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)

Tactic:
simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, RCLike.mul_conj]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
⊢ ∑ j, ↑‖U i j‖ ^ 2 = ↑(∑ x, ‖U i x‖ ^ 2)
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: x y : ℝ
⊢ ↑(exp (x + y)) = ↑(exp x * exp y)

Tactic:
simp only [coe_exp, ofReal_add, add_mul, Complex.exp_add, coe_mul]

Goal state after: