mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
⊢ M.map id = M

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
i✝ : m
j✝ : n
⊢ M.map id i✝ j✝ = M i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
B : Type u_6
C : Type u_7
M : Matrix m n A
f : A → B
g : B → C
⊢ (M.map f).map g = M.map (g ∘ f)

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
B : Type u_6
C : Type u_7
M : Matrix m n A
f : A → B
g : B → C
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (g ∘ f) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
⊢ conjTranspose 0 = 0

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
i✝ : n
j✝ : m
⊢ conjTranspose 0 i✝ j✝ = 0 i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : Module R A
inst✝ : Module S B
f : A →ₛₗ[σ] B
M N : CStarMatrix m n A
⊢ (M + N).map ⇑f = M.map ⇑f + N.map ⇑f

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : Module R A
inst✝ : Module S B
f : A →ₛₗ[σ] B
M N : CStarMatrix m n A
i✝ : m
j✝ : n
⊢ (M + N).map (⇑f) i✝ j✝ = (M.map ⇑f + N.map ⇑f) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : Module R A
inst✝ : Module S B
f : A →ₛₗ[σ] B
r : R
M : CStarMatrix m n A
⊢ (r • M).map ⇑f = σ r • M.map ⇑f

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : Module R A
inst✝ : Module S B
f : A →ₛₗ[σ] B
r : R
M : CStarMatrix m n A
i✝ : m
j✝ : n
⊢ (r • M).map (⇑f) i✝ j✝ = (σ r • M.map ⇑f) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
l : Type u_7
o : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
M N : CStarMatrix m n A
⊢ (Matrix.reindex eₘ eₙ).toFun (M + N) = (Matrix.reindex eₘ eₙ).toFun M + (Matrix.reindex eₘ eₙ).toFun N

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
l : Type u_7
o : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
M N : CStarMatrix m n A
i✝ : l
j✝ : o
⊢ (Matrix.reindex eₘ eₙ).toFun (M + N) i✝ j✝ = ((Matrix.reindex eₘ eₙ).toFun M + (Matrix.reindex eₘ eₙ).toFun N) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
l : Type u_7
o : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
r : R
M : CStarMatrix m n A
⊢ (Matrix.reindex eₘ eₙ).toFun (r • M) = (RingHom.id R) r • (Matrix.reindex eₘ eₙ).toFun M

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
l : Type u_7
o : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
r : R
M : CStarMatrix m n A
i✝ : l
j✝ : o
⊢ (Matrix.reindex eₘ eₙ).toFun (r • M) i✝ j✝ = ((RingHom.id R) r • (Matrix.reindex eₘ eₙ).toFun M) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R✝ : Type u_3
S : Type u_4
A✝ : Type u_5
B : Type u_6
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M : CStarMatrix m m A
⊢ (↑(reindexₗ R A e e)).toFun (star M) = star ((↑(reindexₗ R A e e)).toFun M)

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R✝ : Type u_3
S : Type u_4
A✝ : Type u_5
B : Type u_6
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M : CStarMatrix m m A
i✝ j✝ : n
⊢ (↑(reindexₗ R A e e)).toFun (star M) i✝ j✝ = star ((↑(reindexₗ R A e e)).toFun M) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
M N : CStarMatrix n n A
⊢ (mapₗ ↑f) (M * N) = (mapₗ ↑f) M * (mapₗ ↑f) N

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
M N : CStarMatrix n n A
i✝ j✝ : n
⊢ (mapₗ ↑f) (M * N) i✝ j✝ = ((mapₗ ↑f) M * (mapₗ ↑f) N) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
M : CStarMatrix n n A
⊢ (mapₗ ↑f) (star M) = star ((mapₗ ↑f) M)

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
M : CStarMatrix n n A
i✝ j✝ : n
⊢ (mapₗ ↑f) (star M) i✝ j✝ = star ((mapₗ ↑f) M) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ x✝ : A
⊢ (fun x y ↦ x✝¹ * x✝) = (fun x y ↦ x✝¹) * fun x y ↦ x✝

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ x✝ : A
i✝ j✝ : n
⊢ x✝¹ * x✝ = ((fun x y ↦ x✝¹) * fun x y ↦ x✝) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ x✝ : A
⊢ (fun x y ↦ x✝¹ + x✝) = (fun x y ↦ x✝¹) + fun x y ↦ x✝

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ x✝ : A
i✝ j✝ : n
⊢ x✝¹ + x✝ = ((fun x y ↦ x✝¹) + fun x y ↦ x✝) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝ : A
⊢ (fun x y ↦ star x✝) = star fun x y ↦ x✝

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝ : A
i✝ j✝ : n
⊢ star x✝ = star (fun x y ↦ x✝) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ : R
x✝ : A
⊢ (fun x y ↦ x✝¹ • x✝) = x✝¹ • fun x y ↦ x✝

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ : R
x✝ : A
i✝ j✝ : n
⊢ x✝¹ • x✝ = (x✝¹ • fun x y ↦ x✝) i✝ j✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
⊢ { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* (M₁ + M₂)) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
      map_smul' := ⋯, cont := ⋯ } =
    { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* M₁) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
        map_smul' := ⋯, cont := ⋯ } +
      { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* M₂) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
        map_smul' := ⋯, cont := ⋯ }

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
x✝ : C⋆ᵐᵒᵈ(A, m → A)
i✝ : n
⊢ { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* (M₁ + M₂)) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
        map_smul' := ⋯, cont := ⋯ }
      x✝ i✝ =
    ({ toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* M₁) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
          map_smul' := ⋯, cont := ⋯ } +
        { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* M₂) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
          map_smul' := ⋯, cont := ⋯ })
      x✝ i✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝² : Fintype m
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : Fintype n
x✝ y✝ : CStarMatrix n n A
⊢ toCLM (x✝ * y✝) = toCLM y✝ * toCLM x✝

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝² : Fintype m
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : Fintype n
x✝¹ y✝ : CStarMatrix n n A
x✝ : C⋆ᵐᵒᵈ(A, n → A)
i✝ : n
⊢ (toCLM (x✝¹ * y✝)) x✝ i✝ = (toCLM y✝ * toCLM x✝¹) x✝ i✝
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝² : Fintype m
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : DecidableEq m
M : CStarMatrix m n A
i : m
a : A
⊢ (toCLM M) ((equiv A (m → A)).symm (Pi.single i a)) = (equiv A (n → A)).symm fun j ↦ a * M i j

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝² : Fintype m
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : DecidableEq m
M : CStarMatrix m n A
i : m
a : A
i✝ : n
⊢ (toCLM M) ((equiv A (m → A)).symm (Pi.single i a)) i✝ = (equiv A (n → A)).symm (fun j ↦ a * M i j) i✝
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfc x a) = (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}

Tactic:
ext

Goal state after:
A : Type u_1
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ (x✝ ∈ Set.range fun x ↦ cfc x a) ↔ x✝ ∈ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ (x✝ ∈ Set.range fun x ↦ cfc x a) ↔ x✝ ∈ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}

Tactic:
constructor

Goal state after:
case mp
A : Type u_1
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ (x✝ ∈ Set.range fun x ↦ cfc x a) → x✝ ∈ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}

case mpr
A : Type u_1
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ x✝ ∈ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} → x✝ ∈ Set.range fun x ↦ cfc x a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ cfcₙ (fun x ↦ ↑(f x.re)) a = cfcₙ f ↑(ℜ a)

Tactic:
by
  have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((re · : ℂ → ℂ) '' quasispectrum ℂ a) := by
    rw [quasispectrum_realPart' a] at hf
    refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_
    simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..
  conv_rhs =>
    rw [cfcₙ_real_eq_complex, ← cfcₙ_re_id a, ← cfcₙ_comp' ..]
    simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfcₙ x a) = (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}

Tactic:
ext

Goal state after:
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ (x✝ ∈ Set.range fun x ↦ cfcₙ x a) ↔ x✝ ∈ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ (x✝ ∈ Set.range fun x ↦ cfcₙ x a) ↔ x✝ ∈ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}

Tactic:
constructor

Goal state after:
case mp
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ (x✝ ∈ Set.range fun x ↦ cfcₙ x a) → x✝ ∈ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}

case mpr
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ x✝ ∈ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} → x✝ ∈ Set.range fun x ↦ cfcₙ x a
Module: Mathlib.Topology.Algebra.Module.PerfectPairing

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x✝ : M
y✝ : N
inst✝¹ : p.IsContPerfPair
inst✝ : IsTopologicalRing R
x y : M
⊢ { toLinearMap := p (x + y), cont := ⋯ } = { toLinearMap := p x, cont := ⋯ } + { toLinearMap := p y, cont := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x✝¹ : M
y✝ : N
inst✝¹ : p.IsContPerfPair
inst✝ : IsTopologicalRing R
x y : M
x✝ : N
⊢ { toLinearMap := p (x + y), cont := ⋯ } x✝ =
    ({ toLinearMap := p x, cont := ⋯ } + { toLinearMap := p y, cont := ⋯ }) x✝
Module: Mathlib.Topology.Algebra.Module.PerfectPairing

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x✝ : M
y : N
inst✝¹ : p.IsContPerfPair
inst✝ : IsTopologicalRing R
r : R
x : M
⊢ { toLinearMap := p (r • x), cont := ⋯ } = (RingHom.id R) r • { toLinearMap := p x, cont := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x✝¹ : M
y : N
inst✝¹ : p.IsContPerfPair
inst✝ : IsTopologicalRing R
r : R
x : M
x✝ : N
⊢ { toLinearMap := p (r • x), cont := ⋯ } x✝ = ((RingHom.id R) r • { toLinearMap := p x, cont := ⋯ }) x✝
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2
x₁ : E × F
hx₁ : x₁ ∈ s ×ˢ t
x₂ : E × F
hx₂ : x₂ ∈ s ×ˢ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : a • x₁ + b • x₂ = (x, y)
⊢ x₁ = (x, y)

Tactic:
ext

Goal state after:
case refine_1.fst
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2
x₁ : E × F
hx₁ : x₁ ∈ s ×ˢ t
x₂ : E × F
hx₂ : x₂ ∈ s ×ˢ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : a • x₁ + b • x₂ = (x, y)
⊢ x₁.1 = (x, y).1

case refine_1.snd
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2
x₁ : E × F
hx₁ : x₁ ∈ s ×ˢ t
x₂ : E × F
hx₂ : x₂ ∈ s ×ˢ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : a • x₁ + b • x₂ = (x, y)
⊢ x₁.2 = (x, y).2
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
Module: Mathlib.Topology.Algebra.LinearMapCompletion

Goal state before:
pp: α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : UniformSpace α
inst✝¹² : AddCommGroup α
inst✝¹¹ : IsUniformAddGroup α
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Module R₁ α
inst✝⁸ : UniformContinuousConstSMul R₁ α
inst✝⁷ : Semiring R₂
inst✝⁶ : UniformSpace β
inst✝⁵ : AddCommGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : Module R₂ β
inst✝² : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
inst✝¹ : T0Space β
inst✝ : CompleteSpace β
f : α →SL[σ] β
g : Completion α →SL[σ] β
h : ∀ (e : α), f e = g ↑e
⊢ f.fromCompletion = g

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : UniformSpace α
inst✝¹² : AddCommGroup α
inst✝¹¹ : IsUniformAddGroup α
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Module R₁ α
inst✝⁸ : UniformContinuousConstSMul R₁ α
inst✝⁷ : Semiring R₂
inst✝⁶ : UniformSpace β
inst✝⁵ : AddCommGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : Module R₂ β
inst✝² : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
inst✝¹ : T0Space β
inst✝ : CompleteSpace β
f : α →SL[σ] β
g : Completion α →SL[σ] β
h : ∀ (e : α), f e = g ↑e
x✝ : Completion α
⊢ f.fromCompletion x✝ = g x✝