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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hx : x ∈ σ 𝕜 a
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ‖f x‖₊ ≤ ‖cfc (p := p) f a‖₊

Tactic:
norm_apply_le_norm_cfc f a hx

Premises used: 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
inl : Subsingleton A → ‖cfc (p := p) f a‖ ≤ c
inr : Nontrivial A → ‖cfc (p := p) f a‖ ≤ c
⊢ ‖cfc (p := p) f a‖ ≤ c

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h_1 : Subsingleton A
⊢ ‖cfc (p := p) f a‖ ≤ c

Tactic:
simpa [Subsingleton.elim (cfc f a) 0]

Premises used: cfc, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h_1 : Nontrivial A
⊢ (fun (x : A) ↦ ‖x‖ ≤ c) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h_1 : Nontrivial A
inr :
  ∀ (hf : ContinuousOn f (σ 𝕜 a)) (ha : p a),
    (fun (x : A) ↦ ‖x‖ ≤ c)
      ((cfcHom (p := p) ha : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A)
        { toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) })
⊢ ‖cfc (p := p) f a‖ ≤ c

Tactic:
refine cfc_cases (‖·‖ ≤ c) a f (by simpa) fun hf ha ↦ ?_

Premises used: Norm.norm, LE.le, cfc_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h_1 : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
inr : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a)) c
⊢ norm.{u_2} (E := A)
      ((cfcHom (p := p) ha : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A)
          { toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) } :
        A) ≤
    c

Tactic:
simp only [← cfc_apply f a, isLUB_le_iff (IsGreatest.norm_cfc f a hf ha |>.isLUB)]

Premises used: IsGreatest.norm_cfc, isLUB_le_iff, IsGreatest.isLUB, cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h_1 : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x ≤ c

Tactic:
h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h_1 : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x ≤ c

Tactic:
exact h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
hf : ContinuousOn f (σ 𝕜 a)
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 ha |>.trans h, norm_cfc_le hc⟩

Premises used: norm_cfc_le, Iff.intro, norm_apply_le_norm_cfc, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
inl : Subsingleton A → ‖cfc (p := p) f a‖ < c
inr : Nontrivial A → ‖cfc (p := p) f a‖ < c
⊢ ‖cfc (p := p) f a‖ < c

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h_1 : Subsingleton A
⊢ ‖cfc (p := p) f a‖ < c

Tactic:
simpa [Subsingleton.elim (cfc f a) 0]

Premises used: cfc, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h_1 : Nontrivial A
⊢ (fun (x : A) ↦ ‖x‖ < c) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h_1 : Nontrivial A
inr :
  ∀ (hf : ContinuousOn f (σ 𝕜 a)) (ha : p a),
    (fun (x : A) ↦ ‖x‖ < c)
      ((cfcHom (p := p) ha : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A)
        { toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) })
⊢ ‖cfc (p := p) f a‖ < c

Tactic:
refine cfc_cases (‖·‖ < c) a f (by simpa) fun hf ha ↦ ?_

Premises used: Norm.norm, LT.lt, cfc_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h_1 : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
inr : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) x → x < c
⊢ norm.{u_2} (E := A)
      ((cfcHom (p := p) ha : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A)
          { toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) } :
        A) <
    c

Tactic:
simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)]

Premises used: IsGreatest.lt_iff, IsGreatest.norm_cfc, cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h_1 : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x < c

Tactic:
h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h_1 : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x < c

Tactic:
exact h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
hf : ContinuousOn f (σ 𝕜 a)
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 ha |>.trans_lt h, norm_cfc_lt hc⟩

Premises used: Iff.intro, norm_apply_le_norm_cfc, LE.le.trans_lt, norm_cfc_lt
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ≥0
h : ∀ x ∈ σ 𝕜 a, ‖f x‖₊ ≤ c
⊢ ‖cfc (p := p) f a‖₊ ≤ c

Tactic:
norm_cfc_le c.2 h

Premises used: norm_cfc_le, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ≥0
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ‖cfc (p := p) f a‖₊ ≤ c ↔ ∀ x ∈ σ 𝕜 a, ‖f x‖₊ ≤ c

Tactic:
norm_cfc_le_iff f a c.2

Premises used: norm_cfc_le_iff, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖₊ < c
⊢ ‖cfc (p := p) f a‖₊ < c

Tactic:
norm_cfc_lt hc 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ≥0
hc : 0 < c
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ‖cfc (p := p) f a‖₊ < c ↔ ∀ x ∈ σ 𝕜 a, ‖f x‖₊ < c

Tactic:
norm_cfc_lt_iff f a hc

Premises used: norm_cfc_lt_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 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: id, nnnorm_apply_le_nnnorm_cfc, 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.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 ∧ SpectrumRestricts.{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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
⊢ SpectrumRestricts.{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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
⊢ ContinuousFunctionalCalculus R A p

Tactic:
have := SpectrumRestricts.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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
rw :
  Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(starAlgHom (cfcHom (p := q) ha') haf) : (a : C((↑(σ R a) : Type u_1), R)) → A)
⊢ Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(cfcHom (p := p) ha) : (a : C((↑(σ R a) : Type u_1), R)) → A)

Tactic:
rw [cfcHom_eq_restrict f ha ha' haf]

Premises used: SpectrumRestricts.cfcHom_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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
⊢ Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(starAlgHom (cfcHom (p := q) ha') haf) : (a : C((↑(σ 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
refine :
  ∀ (g₁ g₂ : C((↑(σ R a) : Type u_1), R)),
    dist.{u_3} (α := A) ((starAlgHom (cfcHom (p := q) ha') haf : (a : C((↑(σ R a) : Type u_1), R)) → A) g₁ : A)
        ((starAlgHom (cfcHom (p := q) ha') haf : (a : C((↑(σ R a) : Type u_1), R)) → A) g₂ : A) =
      dist g₁ g₂
⊢ Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(starAlgHom (cfcHom (p := q) ha') haf) : (a : C((↑(σ 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
g₁ g₂ : C((↑(σ R a) : Type u_1), R)
simp :
  dist.{u_2} (α := C((↑(σ S a) : Type u_2), S))
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(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 := ⋯ : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) }))
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(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 := ⋯ : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) })) =
    dist g₁ g₂
⊢ dist.{u_3} (α := A) ((starAlgHom (cfcHom (p := q) ha') haf : (a : C((↑(σ R a) : Type u_1), R)) → A) g₁ : A)
      ((starAlgHom (cfcHom (p := q) ha') haf : (a : C((↑(σ R a) : Type u_1), R)) → A) g₂ : A) =
    dist g₁ g₂

Tactic:
simp only [starAlgHom_apply, isometry_cfcHom a ha' |>.dist_eq]

Premises used: SpectrumRestricts.starAlgHom_apply, Isometry.dist_eq, isometry_cfcHom