awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (hypothesis)
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)
⊢ cfcₙ (p := p) g a = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
have this : ¬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)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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)
⊢ cfcₙ (p := p) g a = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
have neg : 0 = 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
⊢ cfcₙ (p := p) g a = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
have neg₁ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [cfcₙ_apply_of_not_continuousOn a hg, cfcₙ_apply_of_not_continuousOn a this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
⊢ cfcₙ (p := p) g a = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
have neg : 0 = 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])]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
⊢ cfcₙ (p := p) g a = cfcₙ (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
have neg₁ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [cfcₙ_apply_of_not_map_zero a hg, cfcₙ_apply_of_not_map_zero a (by simpa [h.map_zero])]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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)
    (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
have rw : IsClosedEmbedding.{u_1, u_3} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
  (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry) : (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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (hypothesis)
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) ((φ : (a : A) → B) a : B) = spectrum ℝ a
have h_spec : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
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
have refine : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a), x ∈ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
Tactic: refine Set.eq_of_subset_of_subset h_spec fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
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
⊢ x ∈ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
have by_contra : ∀ (hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)), False
Tactic: by_contra hx'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
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)
⊢ False
have 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
Tactic: obtain ⟨f, h_eqOn, h_eqOn_x, -⟩ := exists_continuous_zero_one_of_isClosed
    (spectrum.isClosed (𝕜 := ℝ) (φ a)) (isClosed_singleton (x := x)) <| by simpa
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (hypothesis)
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)
⊢ False
have this₁ : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum ℝ a)
Tactic: rw [map_eq_zero_iff φ hφ, ← cfc_zero ℝ a, cfc_eq_cfc_iff_eqOn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
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}
⊢ False
have suffices : Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) (cfc (R := ℝ) (p := IsSelfAdjoint) (⇑f : (a : ℝ) → ℝ) a) : B) (0 : B)
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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
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}
⊢ Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) (cfc (R := ℝ) (p := IsSelfAdjoint) (⇑f : (a : ℝ) → ℝ) a) : B) (0 : B)
have calc : cfc (R := ℝ) (p := IsSelfAdjoint) 0 ((φ : (a : A) → B) a) = 0
Tactic: calc φ (cfc f a) = cfc f (φ a) := StarAlgHomClass.map_cfc φ f a
    _ = cfc (0 : ℝ → ℝ) (φ a) := cfc_congr h_eqOn
    _ = 0 := by simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a : A
⊢ norm.{u_3} (E := B) ((φ : (a : A) → B) a : B) = ‖a‖
have suffices : ∀ {ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)},
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
      (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B) →
    ∀ (a : Unitization ℂ A),
      norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B) = ‖a‖
Tactic: suffices ∀ {ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B} (_ : Function.Injective ψ)
      (a : Unitization ℂ A), ‖ψ a‖ = ‖a‖ by
    simpa [norm_inr] using this (starMap_injective (φ := (φ : A →⋆ₙₐ[ℂ] B)) hφ) a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
⊢ norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B) = ‖a‖
have rw : HPow.hPow (β := ℕ)
    (norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B)) 2 =
  HPow.hPow (β := ℕ) ‖a‖ 2
Tactic: rw [← sq_eq_sq₀ (by positivity) (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
⊢ HPow.hPow (β := ℕ)
      (norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B)) 2 =
    HPow.hPow (β := ℕ) ‖a‖ 2
have simp : norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B) =
  ‖star a * a‖
Tactic: simp only [sq, ← CStarRing.norm_star_mul_self, ← map_star, ← map_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (hypothesis)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
⊢ norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B) =
    ‖star a * a‖
have ha : IsSelfAdjoint (star a * a)
Tactic: have ha : IsSelfAdjoint (star a * a) := .star_mul_self a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Hom (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
ha : IsSelfAdjoint (star a * a)
⊢ norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B) =
    ‖star a * a‖
have calc : (spectralRadius.{0, u_3} ℝ (A := Unitization ℂ B)
      ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B)).toReal =
  (spectralRadius ℝ (star a * a)).toReal
Tactic: calc ‖ψ (star a * a)‖ = (spectralRadius ℝ (ψ (star a * a))).toReal :=
      ha.map ψ |>.toReal_spectralRadius_eq_norm.symm
    _ = (spectralRadius ℝ (star a * a)).toReal := by
      simp only [spectralRadius, ha.map_spectrum_real ψ hψ]
    _ = ‖star a * a‖ := ha.toReal_spectralRadius_eq_norm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f' : F
x v : E
h : HasLineDerivAt 𝕜 f f' x v
⊢ lineDeriv 𝕜 f x v = f'
have rw : lineDeriv 𝕜 f x v = lineDeriv 𝕜 f x v
Tactic: rw [h.unique h.lineDifferentiableAt.hasLineDerivAt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ HasLineDerivWithinAt 𝕜 f f' s x v
have apply : Membership.mem (γ := Filter 𝕜) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
Tactic: apply HasDerivWithinAt.mono_of_mem_nhdsWithin h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ Membership.mem (γ := Filter 𝕜) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
have apply : ContinuousWithinAt.{u_1, u_3} (Y := E) (fun (t : 𝕜) ↦ x + t • v) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
Tactic: apply ContinuousWithinAt.preimage_mem_nhdsWithin'' _ hst (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt.{u_1, u_3} (Y := E) (fun (t : 𝕜) ↦ x + t • v) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
have h₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun (t : 𝕜) ↦ x + t • v
Tactic: apply Continuous.continuousWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s : Set E
x : E
L : E →L[𝕜] F_1
hf : HasFDerivWithinAt f L s x
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F_1) v) s x v
have hf₁ : HasFDerivWithinAt f L s (F 0)
Tactic: rw [show x = F (0 : 𝕜) by simp [F]] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s : Set E
x : E
L : E →L[𝕜] F_1
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
hf : HasFDerivWithinAt f L s (F 0)
⊢ HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F_1) v) s x v
have A : HasDerivWithinAt F (0 + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 1 v) (F ⁻¹' s) 0
Tactic: have A : HasDerivWithinAt F (0 + (1 : 𝕜) • v) (F ⁻¹' s) 0 :=
    ((hasDerivAt_const (0 : 𝕜) x).add ((hasDerivAt_id' (0 : 𝕜)).smul_const v)).hasDerivWithinAt