awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
t : Set (R × R)
⊢ t ∈ uniformity R →
    ∀ᶠ (n : { x : X // x ∈ s }) in comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l,
      ∀ x ∈ spectrum R a, (f x, (fun (x : { x : X // x ∈ s }) ↦ F (↑x : X)) n x) ∈ t
have pos : t ∈ uniformity R → ∀ᶠ (b : X) in l, ∀ (a_2 : X) (b_1 : a_2 ∈ s), a_2 = b → ∀ x ∈ spectrum R a, (f x, F a_2 x) ∈ t
Tactic: simp only [eventually_comap, Subtype.forall]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
t : Set (R × R)
⊢ t ∈ uniformity R → ∀ᶠ (b : X) in l, ∀ (a_2 : X) (b_1 : a_2 ∈ s), a_2 = b → ∀ x ∈ spectrum R a, (f x, F a_2 x) ∈ t
have pos : ∀ (ht : t ∈ uniformity R) (x : X) (this : ∀ x_1 ∈ spectrum R a, (f x_1, F x x_1) ∈ t) (a_1 : X) (b : a_1 ∈ s),
  a_1 = x → ∀ x ∈ spectrum R a, (f x, F a_1 x) ∈ t
Tactic: peel h_tendsto t with ht x _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
have inl : ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
  Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) ⊥ (𝓝 (cfc (p := p) f a))
Tactic: open scoped ContinuousFunctionalCalculus in
  obtain (rfl | hl) := l.eq_or_neBot
  · simp
  have hf := h_tendsto.continuousOn hF.frequently
  by_cases ha : p a
  · let s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
    rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
    conv =>
      enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.2)]
    rw [cfc_apply ..]
    apply cfcHom_continuous _ |>.tendsto _ |>.comp
    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
    intro t
    simp only [eventually_comap, Subtype.forall]
    peel h_tendsto t with ht x _
    simp_all
  · simpa [cfc_apply_of_not_predicate a ha] using tendsto_const_nhds
Cleared hypotheses: l, h_tendsto, hF
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) ⊥ (𝓝 (cfc (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
have inr : ∀ (hl : l.NeBot), Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
Tactic: open scoped ContinuousFunctionalCalculus in
  obtain (rfl | hl) := l.eq_or_neBot
  · simp
  have hf := h_tendsto.continuousOn hF.frequently
  by_cases ha : p a
  · let s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
    rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
    conv =>
      enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.2)]
    rw [cfc_apply ..]
    apply cfcHom_continuous _ |>.tendsto _ |>.comp
    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
    intro t
    simp only [eventually_comap, Subtype.forall]
    peel h_tendsto t with ht x _
    simp_all
  · simpa [cfc_apply_of_not_predicate a ha] using tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) ⊥ (𝓝 (cfc (p := p) f a))
inr inr₁ : ∀ (hl : l.NeBot), Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
have inr₂ : ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)),
  Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
Tactic: open scoped ContinuousFunctionalCalculus in
  obtain (rfl | hl) := l.eq_or_neBot
  · simp
  have hf := h_tendsto.continuousOn hF.frequently
  by_cases ha : p a
  · let s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
    rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
    conv =>
      enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.2)]
    rw [cfc_apply ..]
    apply cfcHom_continuous _ |>.tendsto _ |>.comp
    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
    intro t
    simp only [eventually_comap, Subtype.forall]
    peel h_tendsto t with ht x _
    simp_all
  · simpa [cfc_apply_of_not_predicate a ha] using tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) ⊥ (𝓝 (cfc (p := p) f a))
inr inr₁ : ∀ (hl : l.NeBot), Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
inr₂ :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
have pos : ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)) (ha : p a),
  Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
Tactic: open scoped ContinuousFunctionalCalculus in
  obtain (rfl | hl) := l.eq_or_neBot
  · simp
  have hf := h_tendsto.continuousOn hF.frequently
  by_cases ha : p a
  · let s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
    rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
    conv =>
      enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.2)]
    rw [cfc_apply ..]
    apply cfcHom_continuous _ |>.tendsto _ |>.comp
    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
    intro t
    simp only [eventually_comap, Subtype.forall]
    peel h_tendsto t with ht x _
    simp_all
  · simpa [cfc_apply_of_not_predicate a ha] using tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) ⊥ (𝓝 (cfc (p := p) f a))
inr inr₁ : ∀ (hl : l.NeBot), Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
inr₂ :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
pos :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
have neg : ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)) (ha : ¬p a),
  Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
Tactic: open scoped ContinuousFunctionalCalculus in
  obtain (rfl | hl) := l.eq_or_neBot
  · simp
  have hf := h_tendsto.continuousOn hF.frequently
  by_cases ha : p a
  · let s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
    rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
    conv =>
      enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.2)]
    rw [cfc_apply ..]
    apply cfcHom_continuous _ |>.tendsto _ |>.comp
    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
    intro t
    simp only [eventually_comap, Subtype.forall]
    peel h_tendsto t with ht x _
    simp_all
  · simpa [cfc_apply_of_not_predicate a ha] using tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont :
  ContinuousOn.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
    (fun (x : X) ↦ (ofFun {spectrum R a} : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) (f x) a) s
have h_cont₁ : ∀ x ∈ s,
  ContinuousWithinAt.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
    (fun (x : X) ↦ (ofFun {spectrum R a} : (a_2 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) s x
Tactic: rw [ContinuousOn] at h_cont ⊢
Cleared hypotheses: h_cont, hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont :
  ∀ x ∈ s,
    ContinuousWithinAt.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
      (fun (x : X) ↦ (ofFun {spectrum R a} : (a_2 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) s x
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
⊢ ∀ x ∈ s, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) (f x) a) s x
have h_cont₁ : ∀ x ∈ s, TendstoUniformlyOn (fun (x : X) ↦ f x) (f x) (𝓝[s] x) (spectrum R a)
Tactic: simp only [ContinuousWithinAt, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Set.mem_singleton_iff,
    Function.comp_def, toFun_ofFun, forall_eq] at h_cont
Cleared hypotheses: h_cont
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun (x : X) ↦ f x) (f x) (𝓝[s] x) (spectrum R a)
⊢ ∀ x ∈ s, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) (f x) a) s x
have refine : ∀ (x : X) (hx : x ∈ s), ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (spectrum R a)
Tactic: refine fun x hx ↦ continuousWithinAt_cfc_fun (h_cont x hx) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
h_cont :
  Continuous[inst_10, topologicalSpace R R {spectrum R a}] fun (x : X) ↦
    (ofFun {spectrum R a} : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)
hf : ∀ (x : X), ContinuousOn (f x) (spectrum R a)
⊢ Continuous[inst_10, inst_7] fun (x : X) ↦ cfc (p := p) (f x) a
have rw : ∀
  (h_cont :
    ContinuousOn.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
      (fun (x : X) ↦ (ofFun {spectrum R a} : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) Set.univ)
  (hf : ∀ (x : X), ContinuousOn (f x) (spectrum R a)),
  ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) (f x) a) Set.univ
Tactic: rw [← continuousOn_univ] at h_cont ⊢
Cleared hypotheses: h_cont, hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
⊢ LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{spectrum R a}] R) ↦
      cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
have pos : ∀ (ha : p a),
  LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{spectrum R a}] R) ↦
      cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
Tactic: by_cases ha : p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
pos :
  ∀ (ha : p a),
    LipschitzOnWith.{u_2, u_3} (β := A) 1
      (fun (f : R →ᵤ[{spectrum R a}] R) ↦
        cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
      {f : R →ᵤ[{spectrum R a}] R |
        ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
⊢ LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{spectrum R a}] R) ↦
      cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
have neg : ∀ (ha : ¬p a),
  LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{spectrum R a}] R) ↦
      cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
Tactic: by_cases ha : p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
    f
g : R →ᵤ[{spectrum R a}] R
hg :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
    g
⊢ edist (cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
      (cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g) a) ≤
    (↑1 : ENNReal) * edist f g
have pos : edist
    {
      toFun :=
        (spectrum R a).restrict (π := fun (a : R) ↦ R)
          ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f),
      continuous_toFun := sorry : C((↑(spectrum R a) : Type u_2), R) }
    {
      toFun :=
        (spectrum R a).restrict (π := fun (a : R) ↦ R)
          ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g),
      continuous_toFun := sorry : C((↑(spectrum R a) : Type u_2), R) } ≤
  (↑1 : ENNReal) * edist f g
Tactic: rw [cfc_apply .., cfc_apply .., isometry_cfcHom (R := R) a ha |>.edist_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
    f
g : R →ᵤ[{spectrum R a}] R
hg :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
    g
⊢ edist
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) }
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) } ≤
    (↑1 : ENNReal) * edist f g
have pos : edist
    {
      toFun :=
        (spectrum R a).restrict (π := fun (a : R) ↦ R)
          ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f),
      continuous_toFun := sorry : C((↑(spectrum R a) : Type u_2), R) }
    {
      toFun :=
        (spectrum R a).restrict (π := fun (a : R) ↦ R)
          ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g),
      continuous_toFun := sorry : C((↑(spectrum R a) : Type u_2), R) } ≤
  edist f g
Tactic: simp only [ENNReal.coe_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
    f
g : R →ᵤ[{spectrum R a}] R
hg :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
    g
⊢ edist
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) }
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) } ≤
    edist f g
have pos : edist f g ≤ edist f g
Tactic: rw [edist_continuousRestrict_of_singleton hf hg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : spectrum R a ⊆ s
⊢ LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{s}] R) ↦ cfc.{u_2, u_3} (R := R) (p := p) ((toFun {s} : (a : R →ᵤ[{s}] R) → R → R) f) a)
    {f : R →ᵤ[{s}] R | ContinuousOn (Y := R) ((toFun {s} : (a : R →ᵤ[{s}] R) → R → R) f) s}
have h₁ : LipschitzOnWith.{u_2, u_3} (β := A) 1
  (fun (f : R →ᵤ[{spectrum R a}] R) ↦
    cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
  {f : R →ᵤ[{spectrum R a}] R |
    ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
Tactic: have h₁ := lipschitzOnWith_cfc_fun R a