mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : NontriviallyNormedField 𝕜₁
inst✝¹⁶ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁵ : RingHomIsometric σ₁₂
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformSpace F
inst✝⁸ : IsUniformAddGroup E
inst✝⁷ : IsUniformAddGroup F
inst✝⁶ : ContinuousSMul 𝕜₁ E
inst✝⁵ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝⁴ : PolynormableSpace 𝕜₂ F
inst✝³ : ContinuousSMul 𝕜₂ F
inst✝² : T2Space F
l : Filter α
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x ↦ (g n) x) l (𝓝 f)
⊢ Continuous[inst✝¹⁰.toTopologicalSpace, inst✝⁹.toTopologicalSpace] (linearMapOfTendsto f (fun a ↦ ↑(g a)) h).toFun

Tactic:
rcases l.exists_seq_tendsto with ⟨u, hu⟩
    -- We claim that the limit is continuous because it's a limit of an equicontinuous family.
    -- By the Banach-Steinhaus theorem, this equicontinuity will follow from pointwise boundedness.
    refine (h.comp hu).continuous_of_equicontinuous
      (PolynormableSpace.banach_steinhaus ?_).equicontinuous
    -- For `x` fixed, we need to show that the range of `(i : ℕ) ↦ g i x` is bounded.
    intro x
    -- This follows from the fact that this sequence converges (to `f x`) by hypothesis.
    rw [tendsto_pi_nhds] at h
    exact ((h x).comp hu).isVonNBounded_range 𝕜₂

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ c.Uᶜ.indicator 1 x ≤ c.left.Uᶜ.indicator 1 x

Tactic:
left_U_subset

Goal state after:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ c.Uᶜ.indicator 1 x ≤ c.Uᶜ.indicator 1 x

case hf
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ 0 ≤ 1 x
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SeparableSpace E
inst✝ : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
⊢ IsSeqCompact s

Tactic:
have b_isCompact' : CompactSpace s :=
    isCompact_iff_compactSpace.mp <| isCompact_of_bounded_of_closed hb hc
  have b_isMetrizable : TopologicalSpace.MetrizableSpace s :=
    metrizable_of_isCompact 𝕜 E s <| isCompact_of_bounded_of_closed hb hc
  have seq_cont_phi : SeqContinuous (fun φ : s ↦ (φ : WeakDual 𝕜 E)) :=
    continuous_iff_seqContinuous.mp continuous_subtype_val
  simpa using IsSeqCompact.range seq_cont_phi

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
hbf : 0 < slope f x₀ b
hf : f x₀ = 0
⊢ f b < 0

Tactic:
slope_pos_iff_gt,

Goal state after:
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
hbf : f b < f x₀
hf : f x₀ = 0
⊢ f b < 0

𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
hbf : 0 < slope f x₀ b
hf : f x₀ = 0
⊢ b < x₀
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case neg
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✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
⊢ (-a)⁺ = a⁻

Tactic:
rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha,
      cfcₙ_apply_of_not_predicate _ ha']

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : (i : ι) → Ring (A i)
inst✝⁷ : (i : ι) → Algebra S (A i)
inst✝⁶ : (i : ι) → Algebra R (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMap.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, spectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
⊢ cfc f a = fun i ↦ cfc f (a i)

Tactic:
by
  ext i
  let φ := Pi.evalStarAlgHom S A i
  exact φ.map_cfc f a (by rwa [Pi.spectrum_eq]) (continuous_apply i) ha (ha' i)

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

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

Tactic:
rw [ha, neg_nonpos]; exact negPart_nonneg a

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

Goal state before:
pp: case a.hx
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℜ x))⁺ ∈ {a | 0 ≤ a}

Tactic:
apply CFC.negPart_nonneg

Goal state after:
case a.hx
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℜ x))⁺ ∈ {a | 0 ≤ a}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case a.hy
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℜ x))⁻ ∈ {a | 0 ≤ a}

Tactic:
apply CFC.negPart_nonneg

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

Goal state before:
pp: case a.hx
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℑ x))⁺ ∈ {a | 0 ≤ a}

Tactic:
apply CFC.negPart_nonneg

Goal state after:
case a.hx
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℑ x))⁺ ∈ {a | 0 ≤ a}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case a.hy
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℑ x))⁻ ∈ {a | 0 ≤ a}

Tactic:
apply CFC.negPart_nonneg

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

Goal state before:
pp: case mp
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left✝ : QuasispectrumRestricts s ⇑ContinuousMap.realToNNReal
hs₂ : s * s = y - x
⊢ s * s ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)

Tactic:
exact AddSubmonoid.subset_closure ⟨s, by simp [hs₁.star_eq]⟩

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
⊢ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' _ ℂ]
    -- should this actually be an instance on the `Unitization`? (probably scoped)
    let _ := CStarAlgebra.spectralOrder A⁺¹
    have := CStarAlgebra.spectralOrderedRing A⁺¹
    apply spectrum_nonneg_of_nonneg
    rw [StarOrderedRing.nonneg_iff] at ha ⊢
    have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A) ha
    rw [AddMonoidHom.map_mclosure, ← Set.range_comp] at this
    apply AddSubmonoid.closure_mono ?_ this
    rintro _ ⟨s, rfl⟩
    exact ⟨s, by simp⟩

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
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
⊢ rpow (a, b) x = (a ^ x, b ^ x)

Tactic:
have hb'' : 0 ∉ spectrum ℝ≥0 b := spectrum.zero_notMem _ hb

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
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
⊢ rpow (a, b) x = (a ^ x, b ^ x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

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

Tactic:
exact inr_zero ℂ (A := A) ▸ inr_le_iff 0 a

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
simp_rw [algebraMap_le_iff_le_spectrum (a := a)]

Goal state after:
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, 0 < x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ a ≤ ↑b ↔ ‖sqrt a * sqrt ↑b⁻¹‖ ≤ 1

Tactic:
CFC.sqrt_eq_rpow (a := (↑b⁻¹ : A)),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ a ≤ ↑b ↔ ‖sqrt a * ↑b⁻¹ ^ (1 / 2)‖ ≤ 1
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 * ⟪y, x⟫_A ≤ ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
by
  rcases eq_or_ne x 0 with h | h
  · simp [h, CStarModule.norm_zero A (E := E)]
  · have h₁ : ∀ (a : A),
        (0 : A) ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := fun a => by
      calc (0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by
                      exact inner_self_nonneg
            _ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      simp only [inner_sub_right, inner_op_smul_right, inner_sub_left,
                        inner_op_smul_left, inner_smul_left_real, mul_sub, mul_smul_comm,
                        inner_smul_right_real, smul_sub, mul_assoc]
                      abel
            _ ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      gcongr
                      calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
    specialize h₁ ⟪x, y⟫
    simp only [star_inner, sub_self, zero_sub, le_neg_add_iff_add_le, add_zero] at h₁
    rwa [smul_le_smul_iff_of_pos_left (pow_pos (CStarModule.norm_pos A h) _)] at h₁

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

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
⊢ uniformity C⋆ᵐᵒᵈ(A, E × F) = uniformity C⋆ᵐᵒᵈ(A, E × F)

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
⊢ ∀ (s : Set C⋆ᵐᵒᵈ(A, E × F)), Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
finally
  exacts [uniformity_prod_eq_aux, isBounded_prod_iff_aux]

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

Goal state before:
pp: 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)

Tactic:
← CFC.rpow_neg_one_eq_cfc_inv,

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)
⊢ (1 + ↑b) ^ (-1) ≤ cfc (fun x ↦ x⁻¹) (1 + ↑a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case refine_1
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
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (quasispectrum R a)

pp: case refine_2
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
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, f x 0 = 0

Tactic:
all_goals filter_upwards [self_mem_nhdsWithin] with x hx

Goal state after:
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
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
x✝ : X
hx✝ : x✝ ∈ s
x : X
hx : x ∈ s
⊢ ContinuousOn (f x) (quasispectrum R a)

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
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
x✝ : X
hx✝ : x✝ ∈ s
x : X
hx : x ∈ s
⊢ f x 0 = 0
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
⊢ ‖star z * (1 - star y) * ((1 - y) * z)‖₊ ≤ c ^ 2

Tactic:
have hy₀ : y ∈ Set.Icc 0 1 := ⟨hx₀.trans hy.1, hy.2⟩

Goal state after:
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
⊢ ‖star z * (1 - star y) * ((1 - y) * z)‖₊ ≤ c ^ 2
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ ‖replicateRow ι v‖ = ‖toLp 2 v‖

Tactic:
by
  rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]
  simp only [replicateRow_apply, Real.rpow_two]

Goal state after:
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₂
h_nonneg : ∃ C, ∀ (a : A₁), 0 ≤ a → ‖f a‖ ≤ ↑C * ‖a‖
⊢ ∃ C, ∀ (a : A₁), ‖f a‖ ≤ ↑C * ‖a‖

Tactic:
by
    obtain ⟨C, hmain⟩ := h_nonneg
    refine ⟨4 * C, fun x ↦ ?_⟩
    obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg x
    conv_lhs => rw [hy]
    simp only [map_sum, map_smul]
    apply norm_sum_le _ _ |>.trans
    simp only [norm_smul, norm_pow, norm_I, one_pow, one_mul]
    apply Finset.sum_le_sum (g := fun _ ↦ C * ‖x‖) (fun i _ ↦ ?_) |>.trans <| by simp [mul_assoc]
    apply hmain _ (hy_nonneg i) |>.trans
    gcongr
    exact hy_norm i

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✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), p (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ₙ f (fun x _ ↦ hs x) (fun x _ ↦ by simpa using ha x) (fun x _ ↦ ha' x)

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
this : cfcₙ (fun z ↦ ↑z.re + I * ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfcₙ (fun x ↦ ↑x.im) a = ↑(ℑ a)

Tactic:
cfcₙ_add ..,

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
this : cfcₙ (fun z ↦ ↑z.re) a + cfcₙ (fun z ↦ I * ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfcₙ (fun x ↦ ↑x.im) a = ↑(ℑ a)