-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
lemma inr_comp_cfcₙHom_eq_cfcₙAux {A : Type*} [NonUnitalCStarAlgebra A] (a : A)
    [ha : IsStarNormal a] : (inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) =
      cfcₙAux (isStarNormal_inr (R := ℂ) (A := A)) a ha

Proof state:
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ ((inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha))
      { toContinuousMap := ContinuousMap.restrict (σₙ ℂ a) (ContinuousMap.id ℂ), map_zero' := ⋯ } =
    ↑a

Tactic:
congrm(inr $(cfcₙHom_id ha))

Result:
no goals

Proof state:
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ (inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha

Tactic:
refine @ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id
  _ _ _ _ _ _ _ _ _ _ _ inferInstance inferInstance _ (σₙ ℂ a) _ _ rfl _ _ ?_ ?_ ?_

Result:
case refine_1
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ Continuous ⇑((inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha))

case refine_2
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ Continuous ⇑(cfcₙAux ⋯ a ha)

case refine_3
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ ((inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha))
      { toContinuousMap := ContinuousMap.restrict (σₙ ℂ a) (ContinuousMap.id ℂ), map_zero' := ⋯ } =
    (cfcₙAux ⋯ a ha) { toContinuousMap := ContinuousMap.restrict (σₙ ℂ a) (ContinuousMap.id ℂ), map_zero' := ⋯ }

Proof state:
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ ↑a = (cfcₙAux ⋯ a ha) { toContinuousMap := ContinuousMap.restrict (σₙ ℂ a) (ContinuousMap.id ℂ), map_zero' := ⋯ }

Tactic:
exact cfcₙAux_id @(h) a ha |>.symm

Result:
no goals

Proof state:
case refine_3
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ ((inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha))
      { toContinuousMap := ContinuousMap.restrict (σₙ ℂ a) (ContinuousMap.id ℂ), map_zero' := ⋯ } =
    (cfcₙAux ⋯ a ha) { toContinuousMap := ContinuousMap.restrict (σₙ ℂ a) (ContinuousMap.id ℂ), map_zero' := ⋯ }

Tactic:
trans (a : A⁺¹)

Result:
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ ((inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha))
      { toContinuousMap := ContinuousMap.restrict (σₙ ℂ a) (ContinuousMap.id ℂ), map_zero' := ⋯ } =
    ↑a

A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ ↑a = (cfcₙAux ⋯ a ha) { toContinuousMap := ContinuousMap.restrict (σₙ ℂ a) (ContinuousMap.id ℂ), map_zero' := ⋯ }

Proof state:
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
⊢ (inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha

Tactic:
have h (a : A) := isStarNormal_inr (R := ℂ) (A := A) (a := a)

Result:
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ (inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha

Proof state:
case refine_1
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ Continuous ⇑((inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha))

Tactic:
show Continuous (fun f ↦ (cfcₙHom ha f : A⁺¹))

Result:
case refine_1
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ Continuous fun f => ↑((cfcₙHom ha) f)

Proof state:
case refine_2
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ Continuous ⇑(cfcₙAux ⋯ a ha)

Tactic:
exact isClosedEmbedding_cfcₙAux @(h) a ha |>.continuous

Result:
no goals

Proof state:
case refine_1
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
h : ∀ (a : A), IsStarNormal ↑a ↔ IsStarNormal a
⊢ Continuous fun f => ↑((cfcₙHom ha) f)

Tactic:
fun_prop

Result:
no goals