awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ ‖cfcₙ (p := p) f a‖ < c ↔ ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c

Tactic:
⟨fun h _ hx ↦ norm_apply_le_norm_cfcₙ f a hx hf hf₀ ha |>.trans_lt h, norm_cfcₙ_lt⟩

Premises used: norm_cfcₙ_lt, Iff.intro, norm_apply_le_norm_cfcₙ, LE.le.trans_lt
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ ≤ c
⊢ ‖cfcₙ (p := p) f a‖₊ ≤ c

Tactic:
norm_cfcₙ_le h

Premises used: norm_cfcₙ_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ≥0
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ ‖cfcₙ (p := p) f a‖₊ ≤ c ↔ ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ ≤ c

Tactic:
norm_cfcₙ_le_iff f a c.1 hf hf₀ ha

Premises used: Subtype.val, norm_cfcₙ_le_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ < c
⊢ ‖cfcₙ (p := p) f a‖₊ < c

Tactic:
norm_cfcₙ_lt h

Premises used: norm_cfcₙ_lt
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ≥0
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ ‖cfcₙ (p := p) f a‖₊ < c ↔ ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ < c

Tactic:
norm_cfcₙ_lt_iff f a c.1 hf hf₀ ha

Premises used: norm_cfcₙ_lt_iff, Subtype.val
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖x‖) '' σₙ 𝕜 a) ‖a‖

Tactic:
simpa only [cfcₙ_id 𝕜 a] using IsGreatest.norm_cfcₙ (id : 𝕜 → 𝕜) a

Premises used: IsGreatest.norm_cfcₙ, id, cfcₙ_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σₙ 𝕜 a
ha : p a
⊢ ‖x‖ ≤ ‖a‖

Tactic:
simpa only [cfcₙ_id 𝕜 a] using norm_apply_le_norm_cfcₙ (id : 𝕜 → 𝕜) a hx

Premises used: id, cfcₙ_id, norm_apply_le_norm_cfcₙ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖x‖₊) '' σₙ 𝕜 a) ‖a‖₊

Tactic:
simpa only [cfcₙ_id 𝕜 a] using IsGreatest.nnnorm_cfcₙ (id : 𝕜 → 𝕜) a

Premises used: IsGreatest.nnnorm_cfcₙ, id, cfcₙ_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σₙ 𝕜 a
ha : p a
⊢ ‖x‖₊ ≤ ‖a‖₊

Tactic:
simpa only [cfcₙ_id 𝕜 a] using nnnorm_apply_le_nnnorm_cfcₙ (id : 𝕜 → 𝕜) a hx

Premises used: nnnorm_apply_le_nnnorm_cfcₙ, id, cfcₙ_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
⊢ q a

Tactic:
obtain ⟨ha', haf⟩ := h a |>.mp ha

Premises used: Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
⊢ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)

Tactic:
obtain ⟨ha', haf⟩ := h a |>.mp ha

Premises used: Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
⊢ NonUnitalContinuousFunctionalCalculus R A p

Tactic:
have := QuasispectrumRestricts.cfc f halg.isClosedEmbedding h0 h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
rw :
  Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)
⊢ Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
    (⇑(cfcₙHom (p := p) ha) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)

Tactic:
rw [cfcₙHom_eq_restrict f ha ha' haf]

Premises used: QuasispectrumRestricts.cfcₙHom_eq_restrict
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
⊢ Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)

Tactic:
.of_dist_eq fun g₁ g₂ ↦ ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
refine :
  ∀ (g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R),
    dist.{u_3} (α := A)
        ((nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A) g₁ : A)
        ((nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A) g₂ :
          A) =
      dist g₁ g₂
⊢ Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)

Tactic:
refine .of_dist_eq fun g₁ g₂ ↦ ?_
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R
simp :
  dist (α := ContinuousMapZero (↑(σₙ S a) : Type u_2) S)
      (ContinuousMapZero.comp
        { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ :
          ContinuousMapZero R S }
        (g₁.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }))
      (ContinuousMapZero.comp
        { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ :
          ContinuousMapZero R S }
        (g₂.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) =
    dist g₁ g₂
⊢ dist.{u_3} (α := A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A) g₁ : A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A) g₂ : A) =
    dist g₁ g₂

Tactic:
simp only [nonUnitalStarAlgHom_apply, isometry_cfcₙHom a ha' |>.dist_eq]

Premises used: isometry_cfcₙHom, QuasispectrumRestricts.nonUnitalStarAlgHom_apply, Isometry.dist_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R
⊢ dist (α := ContinuousMapZero (↑(σₙ S a) : Type u_2) S)
      (ContinuousMapZero.comp
        { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ :
          ContinuousMapZero R S }
        (g₁.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }))
      (ContinuousMapZero.comp
        { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ :
          ContinuousMapZero R S }
        (g₂.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) =
    dist g₁ g₂

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R
⊢ dist (α := ContinuousMapZero (↑(σₙ S a) : Type u_2) S)
      (ContinuousMapZero.comp
        { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ :
          ContinuousMapZero R S }
        (g₁.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }))
      (ContinuousMapZero.comp
        { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ :
          ContinuousMapZero R S }
        (g₂.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) ≤
    dist g₁ g₂

Tactic:
ContinuousMap.dist_le dist_nonneg |>.mpr fun x ↦ ?_

Premises used: Iff.mpr, ContinuousMap.dist_le, setOf, dist_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{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
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R
⊢ dist g₁ g₂ ≤
    dist (α := ContinuousMapZero (↑(σₙ S a) : Type u_2) S)
      (ContinuousMapZero.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
        (g₁.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }))
      (ContinuousMapZero.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
        (g₂.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }))

Tactic:
ContinuousMap.dist_le dist_nonneg |>.mpr fun x ↦ ?_

Premises used: Iff.mpr, ContinuousMap.dist_le, setOf, dist_nonneg