awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : IsSelfAdjoint a
⊢ a⁺ = 0 ↔ -(a⁺ - a⁻) = a⁻

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
⊢ IsSelfAdjoint b

Tactic:
have hb' : IsSelfAdjoint b := .of_nonneg hb
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
⊢ IsSelfAdjoint (-c)

Tactic:
have hc' : IsSelfAdjoint (-c) := .neg <| .of_nonneg hc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
⊢ IsSelfAdjoint a

Tactic:
have ha : IsSelfAdjoint a := habc ▸ hb'.sub <| .of_nonneg hc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
rw : a⁺ = b
rw₁ : a⁺ = b → a⁻ = c
⊢ a⁺ = b ∧ a⁻ = c

Tactic:
rw [and_iff_left_of_imp ?of_b_eq]

Premises used: and_iff_left_of_imp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a c : A
hc : 0 ≤ c
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
habc : a = a⁺ - c
hbc : a⁺ * c = 0
hb : 0 ≤ a⁺
hb' : IsSelfAdjoint a⁺
⊢ a⁻ = c

Tactic:
negPart_eq_of_eq_PosPart_sub habc hc

Premises used: CFC.negPart_eq_of_eq_PosPart_sub
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a c : A
hc : 0 ≤ c
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
habc : a = a⁺ - c
hbc : a⁺ * c = 0
hb : 0 ≤ a⁺
hb' : IsSelfAdjoint a⁺
⊢ a⁻ = c

Tactic:
exact negPart_eq_of_eq_PosPart_sub habc hc

Premises used: CFC.negPart_eq_of_eq_PosPart_sub
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
⊢ a⁺ = b → a⁻ = c

Tactic:
case of_b_eq =>
    rintro rfl
    exact negPart_eq_of_eq_PosPart_sub habc hc

Premises used: CFC.negPart_eq_of_eq_PosPart_sub, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ CompactSpace (↑s : Type)

Tactic:
isCompact_iff_compactSpace.mp <| (IsCompact.union ?_ ?_).union ?_

Premises used: isCompact_iff_compactSpace, Iff.mp, IsCompact.union
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
refine_1 : IsCompact (σₙ ℝ a)
refine_2 : IsCompact (σₙ ℝ b)
refine_3 : IsCompact (σₙ ℝ (-c))
⊢ CompactSpace (↑s : Type)

Tactic:
refine isCompact_iff_compactSpace.mp <| (IsCompact.union ?_ ?_).union ?_

Premises used: isCompact_iff_compactSpace, Iff.mp, IsCompact.union
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ IsCompact (σₙ ℝ a)

Tactic:
isCompact_quasispectrum _

Premises used: NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ IsCompact (σₙ ℝ a)

Tactic:
exact isCompact_quasispectrum _

Premises used: NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ IsCompact (σₙ ℝ b)

Tactic:
isCompact_quasispectrum _

Premises used: NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ IsCompact (σₙ ℝ b)

Tactic:
exact isCompact_quasispectrum _

Premises used: NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ IsCompact (σₙ ℝ (-c))

Tactic:
isCompact_quasispectrum _

Premises used: NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ IsCompact (σₙ ℝ (-c))

Tactic:
exact isCompact_quasispectrum _

Premises used: NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ CompactSpace (↑s : Type)

Tactic:
have hs : CompactSpace s := by
    refine isCompact_iff_compactSpace.mp <| (IsCompact.union ?_ ?_).union ?_
    all_goals exact isCompact_quasispectrum _
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
⊢ σₙ ℝ a ⊆ s ∧ σₙ ℝ b ⊆ s ∧ σₙ ℝ (-c) ⊆ s

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
⊢ σₙ ℝ a ⊆ s

Tactic:
obtain ⟨has, hbs, hcs⟩ : σₙ ℝ a ⊆ s ∧ σₙ ℝ b ⊆ s ∧ σₙ ℝ (-c) ⊆ s := by grind

Premises used: Real, quasispectrum, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
⊢ σₙ ℝ b ⊆ s

Tactic:
obtain ⟨has, hbs, hcs⟩ : σₙ ℝ a ⊆ s ∧ σₙ ℝ b ⊆ s ∧ σₙ ℝ (-c) ⊆ s := by grind

Premises used: Real, quasispectrum, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
⊢ σₙ ℝ (-c) ⊆ s

Tactic:
obtain ⟨has, hbs, hcs⟩ : σₙ ℝ a ⊆ s ∧ σₙ ℝ b ⊆ s ∧ σₙ ℝ (-c) ⊆ s := by grind

Premises used: Real, quasispectrum, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
⊢ 0 ∈ s

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
⊢ Fact (0 ∈ s)

Tactic:
have : Fact (0 ∈ s) := ⟨by aesop⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C((↑s : Type), ℝ)₀
⊢ HMul.hMul (α := A) (β := A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          f :
        A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          g :
        A) =
    0

Tactic:
f.nonUnitalStarAlgHom_apply_mul_eq_zero _ _ ?id ?star_id
      (cfcₙHomSuperset_continuous hb' hbs)

Premises used: cfcₙHomSuperset_continuous, ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C((↑s : Type), ℝ)₀
id :
  HMul.hMul (α := A) (β := A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          (ContinuousMapZero.id s) :
        A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          g :
        A) =
    0
star_id :
  HMul.hMul (α := A) (β := A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          (star (ContinuousMapZero.id s)) :
        A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          g :
        A) =
    0
⊢ HMul.hMul (α := A) (β := A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          f :
        A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          g :
        A) =
    0

Tactic:
refine f.nonUnitalStarAlgHom_apply_mul_eq_zero _ _ ?id ?star_id
      (cfcₙHomSuperset_continuous hb' hbs)

Premises used: cfcₙHomSuperset_continuous, ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C((↑s : Type), ℝ)₀
star_id :
  HMul.hMul (α := A) (β := A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          (ContinuousMapZero.id s) :
        A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          g :
        A) =
    0
⊢ HMul.hMul (α := A) (β := A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          (star (ContinuousMapZero.id s)) :
        A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          g :
        A) =
    0

Tactic:
rw [star_trivial]

Premises used: TrivialStar.star_trivial
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C((↑s : Type), ℝ)₀
star_id :
  HMul.hMul (α := A) (β := A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          (ContinuousMapZero.id s) :
        A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          g :
        A) =
    0
⊢ HMul.hMul (α := A) (β := A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          (star (ContinuousMapZero.id s)) :
        A)
      (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
            (a : C((↑s : Type), ℝ)₀) → A)
          g :
        A) =
    0

Tactic:
case' star_id => rw [star_trivial]

Premises used: TrivialStar.star_trivial