awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ¬ContinuousOn g (σₙ R a)
hg' : ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (σₙ S a)
rw : ContinuousOn.{u_1, u_2} (Y := S) ((⇑(algebraMap R S) : (a : R) → S) ∘ g) (σₙ R a)
⊢ ContinuousOn g (σₙ R a)

Tactic:
rw [halg.isEmbedding.continuousOn_iff]

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.continuousOn_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ¬ContinuousOn g (σₙ R a)
hg' : ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (σₙ S a)
⊢ ContinuousOn.{u_1, u_2} (Y := S) ((⇑(algebraMap R S) : (a : R) → S) ∘ g) (σₙ R a)

Tactic:
simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
          hg'.comp halg.isEmbedding.continuous.continuousOn
          (fun _ : R ↦ quasispectrum.algebraMap_mem S)

Premises used: quasispectrum.algebraMap_mem, Continuous.continuousOn, Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.continuousOn_iff, ContinuousOn.comp, Function.comp_def, QuasispectrumRestricts.left_inv, Topology.IsEmbedding.continuous
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ¬ContinuousOn g (σₙ R a)
⊢ ¬ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (σₙ S a)

Tactic:
have : ¬ ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (σₙ S a) := by
        refine fun hg' ↦ hg ?_
        rw [halg.isEmbedding.continuousOn_iff]
        simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
          hg'.comp halg.isEmbedding.continuous.continuousOn
          (fun _ : R ↦ quasispectrum.algebraMap_mem S)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ¬ContinuousOn g (σₙ R a)
this : ¬ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (σₙ S a)
neg : 0 = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
neg₁ neg₂ : Eq.{u_3 + 1} (α := A) 0 0
⊢ cfcₙ (p := p) g a = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a

Tactic:
rw [cfcₙ_apply_of_not_continuousOn a hg, cfcₙ_apply_of_not_continuousOn a this]

Premises used: cfcₙ_apply_of_not_continuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ¬g 0 = 0
⊢ ¬Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) 0)) : S) (0 : S)

Tactic:
simpa [h.map_zero]

Premises used: QuasispectrumRestricts.map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ¬g 0 = 0
neg : 0 = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
neg₁ neg₂ : Eq.{u_3 + 1} (α := A) 0 0
⊢ cfcₙ (p := p) g a = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a

Tactic:
rw [cfcₙ_apply_of_not_map_zero a hg, cfcₙ_apply_of_not_map_zero a (by simpa [h.map_zero])]

Premises used: cfcₙ_apply_of_not_map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : UniqueHom R A
inst_25 : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
⊢ NonUnitalContinuousFunctionalCalculus R A p

Tactic:
have := QuasispectrumRestricts.cfc f halg.isClosedEmbedding h0 h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : UniqueHom R A
inst_25 : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
this : NonUnitalContinuousFunctionalCalculus R A p
rw :
  IsClosedEmbedding.{u_1, u_3} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
rw [cfcₙHom_eq_restrict f ha ((h a).mp ha).1 ((h a).mp ha).2]

Premises used: QuasispectrumRestricts.cfcₙHom_eq_restrict, And.right, And.left, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : UniqueHom R A
inst_25 : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
this : NonUnitalContinuousFunctionalCalculus R A p
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
isClosedEmbedding_nonUnitalStarAlgHom (cfcₙHom_isClosedEmbedding ((h a).mp ha).1)
      ((h a).mp ha).2 halg

Premises used: cfcₙHom_isClosedEmbedding, QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom, And.right, And.left, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
inst_24 : UniqueHom R A
inst_25 : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
this : NonUnitalContinuousFunctionalCalculus R A p
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
exact isClosedEmbedding_nonUnitalStarAlgHom (cfcₙHom_isClosedEmbedding ((h a).mp ha).1)
      ((h a).mp ha).2 halg

Premises used: cfcₙHom_isClosedEmbedding, QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom, And.right, And.left, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
⊢ spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a

Tactic:
have h_spec := AlgHom.spectrum_apply_subset ((φ : A →⋆ₐ[ℂ] B).restrictScalars ℝ) a
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
⊢ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B) = spectrum ℝ a

Tactic:
Set.eq_of_subset_of_subset h_spec fun x hx ↦ ?_

Premises used: Set.eq_of_subset_of_subset
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
refine : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a), x ∈ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
⊢ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B) = spectrum ℝ a

Tactic:
refine Set.eq_of_subset_of_subset h_spec fun x hx ↦ ?_

Premises used: Set.eq_of_subset_of_subset
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
by_contra : ∀ (hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)), False
⊢ x ∈ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)

Tactic:
by_contra hx'
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
⊢ Disjoint (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)) {x}

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
obtain :
  ∀ (f : C(ℝ, ℝ))
    (h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)))
    (h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}), False
⊢ False

Tactic:
obtain ⟨f, h_eqOn, h_eqOn_x, -⟩ := exists_continuous_zero_one_of_isClosed
    (spectrum.isClosed (𝕜 := ℝ) (φ a)) (isClosed_singleton (x := x)) <| by simpa

Premises used: exists_continuous_zero_one_of_isClosed, spectrum.isClosed, isClosed_singleton, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B))
h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}
this : Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) (cfc (R := ℝ) (p := IsSelfAdjoint) (⇑f : (a : ℝ) → ℝ) a) : B) (0 : B)
⊢ Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum ℝ a)

Tactic:
rw [map_eq_zero_iff φ hφ, ← cfc_zero ℝ a, cfc_eq_cfc_iff_eqOn] at this

Premises used: Real, cfc_eq_cfc_iff_eqOn, map_eq_zero_iff, cfc_zero
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B))
h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}
this : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum ℝ a)
⊢ False

Tactic:
zero_ne_one <| calc
      0 = f x := (this hx).symm
      _ = 1 := h_eqOn_x <| Set.mem_singleton x

Premises used: Set.mem_singleton, Trans.trans, zero_ne_one, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B))
h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}
this : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum ℝ a)
⊢ False

Tactic:
exact zero_ne_one <| calc
      0 = f x := (this hx).symm
      _ = 1 := h_eqOn_x <| Set.mem_singleton x

Premises used: Set.mem_singleton, zero_ne_one, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B))
h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}
suffices :
  Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) (cfc (R := ℝ) (p := IsSelfAdjoint) (⇑f : (a : ℝ) → ℝ) a) : B) (0 : B)
⊢ False

Tactic:
suffices φ (cfc f a) = 0 by
    rw [map_eq_zero_iff φ hφ, ← cfc_zero ℝ a, cfc_eq_cfc_iff_eqOn] at this
    exact zero_ne_one <| calc
      0 = f x := (this hx).symm
      _ = 1 := h_eqOn_x <| Set.mem_singleton x
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B))
h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}
⊢ (φ : (a : A) → B) (cfc (R := ℝ) (p := IsSelfAdjoint) (⇑f : (a : ℝ) → ℝ) a) =
    cfc (R := ℝ) (p := IsSelfAdjoint) (⇑f : (a : ℝ) → ℝ) ((φ : (a : A) → B) a)

Tactic:
StarAlgHomClass.map_cfc φ f a

Premises used: DFunLike.coe, StarAlgHomClass.map_cfc