mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : (starRingEnd 𝕜) (x.2 - x.1) = x.2 - x.1
⊢ x.2 = x.1 + ↑√(re (x.2 - x.1)) * ↑√(re (x.2 - x.1))

Tactic:
conj_eq_iff_re

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : ↑(re (x.2 - x.1)) = x.2 - x.1
⊢ x.2 = x.1 + ↑√(re (x.2 - x.1)) * ↑√(re (x.2 - x.1))
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
hd : Disjoint s t
P : Set X → Set X → Prop := fun x x_1 ↦ True
⊢ ∀ {c u : Set X},
    IsClosed[inst✝¹] c →
      P c u →
        IsOpen[inst✝¹] u →
          c ⊆ u → ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u ∧ P c v ∧ P (closure[inst✝¹] v) u

Tactic:
by
      rintro c u c_closed - u_open cu
      rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩
      exact ⟨v, v_open, cv, hv, trivial, trivial⟩

Goal state after:
Module: Mathlib.Order.CompleteLattice.Group

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝³ : CompleteLattice α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
u v : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, u i j * v i j ≤ ⨆ i, (⨆ j, u i j) * ⨆ j, v i j

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝³ : CompleteLattice α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
u v : (i : ι) → κ i → α
i : ι
⊢ ⨆ j, u i j * v i j ≤ (⨆ j, u i j) * ⨆ j, v i j
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
⊢ LipschitzWith K f ↔ ∀ (c : α), LipschitzWith K fun x ↦ toFun (f x) c

Tactic:
by
  simp [LipschitzWith, edist_le, forall_comm (α := α)]

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
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
f : C(↑(spectrum ℂ a), ℂ)
⊢ spectrum ℂ (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f) = Set.range ⇑f

Tactic:
simp only [StarAlgHom.comp_apply, StarAlgHom.coe_coe, StarSubalgebra.coe_subtype]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
f : C(↑(spectrum ℂ a), ℂ)
⊢ spectrum ℂ ↑((continuousFunctionalCalculus a) f) = Set.range ⇑f
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖(algebraMap ℝ A) ↑‖a‖₊ - a‖₊ + ‖(algebraMap ℝ A) ↑‖b‖₊ - b‖₊ ≤ ‖a‖₊ + ‖b‖₊

Tactic:
gcongr

Goal state after:
case h₁
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖(algebraMap ℝ A) ↑‖a‖₊ - a‖₊ ≤ ‖a‖₊

case h₂
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖(algebraMap ℝ A) ↑‖b‖₊ - b‖₊ ≤ ‖b‖₊
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ ‖sqrt a‖₊ = NNReal.sqrt ‖a‖₊

Tactic:
rw [sqrt_eq_nnrpow, NNReal.sqrt_eq_rpow]

Goal state after:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ ‖a ^ (1 / 2)‖₊ = ‖a‖₊ ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
⊢ ‖star b * a * b‖ = ‖sqrt a * b‖ ^ 2

Tactic:
rw [sq, ← CStarRing.norm_star_mul_self, star_mul, (CFC.sqrt_nonneg a).star_eq,
    ← mul_assoc _ (CFC.sqrt a), mul_assoc _ _ (CFC.sqrt a), CFC.sqrt_mul_sqrt_self a]

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

Goal state before:
pp: case pos.inr
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
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : 0 < x
⊢ ‖x⁺‖ ≤ ‖a‖

Tactic:
· simp only [posPart_def, max_eq_left h.le]
    exact NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le a hx ha

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 (r / 2)) ≤ span ℂ ({x | 0 ≤ x} ∩ Metric.ball 0 r)

Tactic:
gcongr

Goal state after:
case h₂
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ Metric.closedBall 0 (r / 2) ⊆ Metric.ball 0 r
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
a : A
x y : ℝ
ha : IsUnit a
⊢ a ^ (x + y) = a ^ x * a ^ y

Tactic:
by
  have ha' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha
  simp only [rpow_def]
  rw [← cfc_mul _ _ a]
  refine cfc_congr ?_
  intro z hz
  have : z ≠ 0 := by aesop
  simp [NNReal.rpow_add this _ _]

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
h : x ≠ 0
a : A
⊢ a * ⟪x, x⟫_A * star a - ‖x‖ ^ 2 •> (a * ⟪y, x⟫_A) - ‖x‖ ^ 2 •> (⟪x, y⟫_A * star a) + ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A ≤
    ‖x‖ ^ 2 •> (a * star a) - ‖x‖ ^ 2 •> (a * ⟪y, x⟫_A) - ‖x‖ ^ 2 •> (⟪x, y⟫_A * star a) +
      ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
gcongr

Goal state after:
case h
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
h : x ≠ 0
a : A
⊢ a * ⟪x, x⟫_A * star a ≤ ‖x‖ ^ 2 •> (a * star a)
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, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖

Tactic:
gcongr

Goal state after:
case h₁
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, x⟫ + ⟪y, x⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖
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, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖

Tactic:
gcongr

Goal state after:
case h₂
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
⊢ ‖⟪y, x⟫‖ ≤ ‖y‖ * ‖x‖

case h₂
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⟫‖ ≤ ‖x‖ * ‖y‖
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
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
⊢ ‖w‖ * ‖v‖ ≤ 1 * ‖v‖

Tactic:
gcongr

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
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2

Tactic:
gcongr

Goal state after:
case h₂
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
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ 2 * ‖x.1‖ * ‖x.2‖
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)
⊢ ‖x.1‖ + ‖x.2‖ ≤ ‖(equiv A (E × F)) x‖ + ‖(equiv A (E × F)) x‖

Tactic:
gcongr

Goal state after:
case h₁
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)
⊢ ‖x.1‖ ≤ ‖(equiv A (E × F)) x‖

case h₂
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)
⊢ ‖x.2‖ ≤ ‖(equiv A (E × F)) x‖
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A),
    autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_1_6 →
      cfc (fun x ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (fun x ↦ x⁻¹) (1 + c)
⊢ 1 - cfc (fun x ↦ x⁻¹) (1 + ↑a) ≤ 1 - cfc (fun x ↦ x⁻¹) (1 + ↑b)

Tactic:
gcongr

Goal state after:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A),
    autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_1_6 →
      cfc (fun x ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (fun x ↦ x⁻¹) (1 + c)
⊢ cfc (fun x ↦ x⁻¹) (1 + ↑b) ≤ cfc (fun x ↦ x⁻¹) (1 + ↑a)
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A),
    autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_1_6 →
      cfc (fun x ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (fun x ↦ x⁻¹) (1 + c)
⊢ 1 + ↑a ≤ 1 + ↑b

Tactic:
gcongr

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

Goal state before:
pp: case left
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun x ↦ x * (1 + x)⁻¹) ((fun x ↦ x * (1 - x)⁻¹) x) = x

Tactic:
have : 0 < 1 - x := tsub_pos_of_lt hx
    simp [field, tsub_add_cancel_of_le hx.le]

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

Goal state before:
pp: 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
s : Set R
hs : quasispectrum R a ⊆ s
⊢ LipschitzOnWith 1 (fun f ↦ cfcₙ ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s ∧ f 0 = 0}

Tactic:
by
  have h₂ := lipschitzWith_one_ofFun_toFun' (𝔖 := {quasispectrum R a}) (𝔗 := {s}) (β := R)
    (by simpa)
  have h₃ := h₂.lipschitzOnWith (s := {f | ContinuousOn (toFun {s} f) (s) ∧ f 0 = 0})
  simpa using! lipschitzOnWith_cfcₙ_fun R a |>.comp h₃ (fun f ↦ .imp_left fun hf ↦ hf.mono hs)

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

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2
hy₀ : y ∈ Set.Icc 0 1
hy' : 1 - y ∈ Set.Icc 0 1
⊢ 1 - y ≤ 1 - x

Tactic:
gcongr

Goal state after:
case h
A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2
hy₀ : y ∈ Set.Icc 0 1
hy' : 1 - y ∈ Set.Icc 0 1
⊢ x ≤ y
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: l : Type u_2
m : Type u_3
α : Type u_5
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊

Tactic:
rw [← linfty_opNNNorm_replicateCol (ι := Fin 1) (A *ᵥ v),
    ← linfty_opNNNorm_replicateCol v (ι := Fin 1)]
  exact linfty_opNNNorm_mul A (replicateCol (Fin 1) v)

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

Goal state before:
pp: B₁ : Type u_3
B₂ : Type u_4
inst✝⁴ : CStarAlgebra B₁
inst✝³ : CStarAlgebra B₂
inst✝² : PartialOrder B₁
inst✝¹ : PartialOrder B₂
inst✝ : StarOrderedRing B₁
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : IsSelfAdjoint x
⊢ f x ≤ f ((algebraMap ℝ B₁) ‖x‖)

Tactic:
gcongr

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₁
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : IsSelfAdjoint x
⊢ x ≤ (algebraMap ℝ B₁) ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: 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
⊢ f x ≤ f (↑‖x‖ • 1)

Tactic:
gcongr

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 ≤ ↑‖x‖ • 1
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → ‖f a‖ ≤ ↑C * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i, I ^ ↑i • y i
i : Fin 4
x✝ : i ∈ Finset.univ
⊢ ↑C * ‖y i‖ ≤ ↑C * ‖x‖

Tactic:
gcongr

Goal state after:
case hbc
A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → ‖f a‖ ≤ ↑C * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i, I ^ ↑i • y i
i : Fin 4
x✝ : i ∈ Finset.univ
⊢ ‖y i‖ ≤ ‖x‖
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
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y * ε ^ 2 * (y / (ε ^ 2 + y)) ≤ ε ^ 2 * 1

Tactic:
gcongr

Goal state after:
case h₁
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := ⋯
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y * ε ^ 2 ≤ ε ^ 2

case h₂
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := ⋯
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y / (ε ^ 2 + y) ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
x : ℕ → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), 2 ^ (2 * x_1) < ‖f (x x_1)‖
x_summable : Summable fun n ↦ 2 ^ (-↑n) • x n
n : ℕ
hn : ‖f (∑' (n : ℕ), 2 ^ (-↑n) • x n)‖ < 2 ^ n
this : ∀ (m : ℕ), 0 ≤ 2 ^ (-↑m) • x m
⊢ f (2 ^ (-↑n) • x n) ≤ f (∑' (n : ℕ), 2 ^ (-↑n) • x n)

Tactic:
gcongr

Goal state after:
case a
A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
x : ℕ → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), 2 ^ (2 * x_1) < ‖f (x x_1)‖
x_summable : Summable fun n ↦ 2 ^ (-↑n) • x n
n : ℕ
hn : ‖f (∑' (n : ℕ), 2 ^ (-↑n) • x n)‖ < 2 ^ n
this : ∀ (m : ℕ), 0 ≤ 2 ^ (-↑m) • x m
⊢ 2 ^ (-↑n) • x n ≤ ∑' (n : ℕ), 2 ^ (-↑n) • x n
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: 𝕜 : 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
f : C(↑(quasispectrum 𝕜 a), 𝕜)₀
⊢ Commute ((cfcₙHom ha) f) b

Tactic:
open scoped NonUnitalContinuousFunctionalCalculus in
  induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simp
  | smul r f hf => rw [map_smul]; exact hf.smul_left r
  | id => rwa [cfcₙHom_id ha]
  | star_id => rwa [map_star, cfcₙHom_id]
  | add f g hf hg => rw [map_add]; exact hf.add_left hg
  | mul f g hf hg => rw [map_mul]; exact mul_left hf hg
  | frequently f hf =>
    rw [commute_iff_eq, ← Set.mem_ofPred (p := fun x => x * b = b * x),
      ← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]
    apply mem_closure_of_frequently_of_tendsto hf
    exact cfcₙHom_continuous ha |>.tendsto _

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

Goal state before:
pp: 𝕜 : 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
f : C(↑(quasispectrum 𝕜 a), 𝕜)₀
⊢ Commute ((cfcₙHom ha) f) b

Tactic:
by
  open scoped NonUnitalContinuousFunctionalCalculus in
  induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simp
  | smul r f hf => rw [map_smul]; exact hf.smul_left r
  | id => rwa [cfcₙHom_id ha]
  | star_id => rwa [map_star, cfcₙHom_id]
  | add f g hf hg => rw [map_add]; exact hf.add_left hg
  | mul f g hf hg => rw [map_mul]; exact mul_left hf hg
  | frequently f hf =>
    rw [commute_iff_eq, ← Set.mem_ofPred (p := fun x => x * b = b * x),
      ← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]
    apply mem_closure_of_frequently_of_tendsto hf
    exact cfcₙHom_continuous ha |>.tendsto _

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

Goal state before:
pp: case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
a✝¹ : i ∈ Finset.univ
j : m
a✝ : j ∈ Finset.univ
⊢ ‖M j i‖ * ‖v j‖ ≤ ‖M j i‖ * ‖v‖

Tactic:
gcongr

Goal state after:
case hbc
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
a✝¹ : i ∈ Finset.univ
j : m
a✝ : j ∈ Finset.univ
⊢ ‖v j‖ ≤ ‖v‖