mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ f a
h : ¬ContinuousOn f (quasispectrum ℝ a)
⊢ ∀ x ∈ quasispectrum ℝ a, 0 ≤ 0 x

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f (↑x.im).re)) a

Tactic:
simp

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f x.im)) a
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✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ f a
h : ¬f 0 = 0
⊢ ∀ x ∈ quasispectrum ℝ a, 0 ≤ 0 x

Tactic:
simp

Goal state after:
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
x✝ : N
⊢ { toLinearMap := p (x + y), cont := ⋯ } x✝ =
    ({ toLinearMap := p x, cont := ⋯ } + { toLinearMap := p y, cont := ⋯ }) x✝

Tactic:
simp

Goal state after:
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
x✝ : N
⊢ { toLinearMap := p (r • x), cont := ⋯ } x✝ = ((RingHom.id R) r • { toLinearMap := p x, cont := ⋯ }) x✝

Tactic:
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✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ f a
h : ¬IsSelfAdjoint a
⊢ ∀ x ∈ quasispectrum ℝ a, 0 ≤ 0 x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
x✝ y : E
⊢ { toLinearMap := (innerₗ E).flip x✝, cont := ⋯ } y = ((toDual ℝ E) x✝) y

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : IsOrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
⊢ ⇑f '' extremePoints 𝕜 s = extremePoints 𝕜 (⇑f '' s)

Tactic:
ext b

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : IsOrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
b : F
⊢ b ∈ ⇑f '' extremePoints 𝕜 s ↔ b ∈ extremePoints 𝕜 (⇑f '' s)
Module: Mathlib.Analysis.CStarAlgebra.Hom

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))
h_eqOn_x : Set.EqOn (⇑f) 1 {x}
⊢ cfc 0 (φ a) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
⊢ ∀ (m : ℂ) (x : A), (f.leftMulMapPreGNS (m • x)).completion = (MonoidHom.id ℂ) m • (f.leftMulMapPreGNS x).completion

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: case ih
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
c : f.PreGNS
⊢ (f.leftMulMapPreGNS (x✝¹ * x✝)).completion ↑c =
    ((f.leftMulMapPreGNS x✝¹).completion * (f.leftMulMapPreGNS x✝).completion) ↑c

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
⊢ f.gnsNonUnitalStarAlgHom 1 = 1

Tactic:
ext b

Goal state after:
A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
b : f.GNS
⊢ (f.gnsNonUnitalStarAlgHom 1) b = 1 b
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A✝ : Type u_1
inst✝⁵ : NonUnitalCStarAlgebra A✝
inst✝⁴ : PartialOrder A✝
f✝ : A✝ →ₚ[ℂ] ℂ
inst✝³ : StarOrderedRing A✝
A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
⊢ f.gnsNonUnitalStarAlgHom.toFun 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.BallSphere

Goal state before:
pp: E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
w : E
⊢ w ∈ sphere 0 r → -w ∈ sphere 0 r

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.BallSphere

Goal state before:
pp: E : Type u_1
i : SeminormedAddCommGroup E
r✝ r : ℝ
w : E
⊢ w ∈ ball 0 r → -w ∈ ball 0 r

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.BallSphere

Goal state before:
pp: E : Type u_1
i : SeminormedAddCommGroup E
r✝ r : ℝ
w : E
⊢ w ∈ closedBall 0 r → -w ∈ closedBall 0 r

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : Zero 𝕜
inst✝ : PseudoMetricSpace 𝕜
⊢ 0 ∈ ball 0 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : Zero 𝕜
inst✝ : PseudoMetricSpace 𝕜
⊢ 0 ∈ closedBall 0 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖v i‖ = ‖toLp 2 (diagonal v *ᵥ Pi.single i 1)‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖T‖ * ‖toLp 2 (Pi.single i 1)‖ ≤ ‖T‖

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
a : X
b : Y
ha : IsOpen[inst✝⁵] {a}
hb : IsOpen[inst✝³] {b}
⊢ ContinuousOn (↑(PartialEquiv.single a b)) (PartialEquiv.single a b).source

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
a : X
b : Y
ha : IsOpen[inst✝⁵] {a}
hb : IsOpen[inst✝³] {b}
⊢ ContinuousOn (PartialEquiv.single a b).invFun (PartialEquiv.single a b).target

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
e f : OpenPartialHomeomorph X Y
e' f' : OpenPartialHomeomorph X' Y'
⊢ (e.prod e').symm.trans (f.prod f') = (e.symm.trans f).prod (e'.symm.trans f')

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : Y
hx : x ∈ ((e.restr s).symm.trans e').source
⊢ (↑e' ∘ ↑e.symm) x = (↑e' ∘ ↑e.symm) x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.openPartialHomeomorphSubtypeCoe hV).symm (↑e.symm y) ∈ (V.openPartialHomeomorphSubtypeCoe hV).source

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case inl
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
heq : a = c
⊢ c ∈ s

pp: case inr
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
hlt : a < c
⊢ c ∈ s

Tactic:
· rwa [← heq]

Goal state after:
case inr
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
hlt : a < c
⊢ c ∈ s
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p.1 ∈ Z.baseSet i ∩ Z.baseSet j ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (star x✝¹)).toProd.1 x✝ = x✝¹.toProd.1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (star x✝¹)).toProd.2 x✝ = x✝¹.toProd.2 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² + x✝¹)).toProd.1 x✝ = (star x✝² + star x✝¹).toProd.1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² + x✝¹)).toProd.2 x✝ = (star x✝² + star x✝¹).toProd.2 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² * x✝¹)).toProd.1 x✝ = (star x✝¹ * star x✝²).toProd.1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² * x✝¹)).toProd.2 x✝ = (star x✝¹ * star x✝²).toProd.2 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b✝ : B
y : E b✝
T✝ : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ ∀ (x : ↑T.source × ↑T.baseSet), ↑x.1 ∈ T.source

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
x✝ : I
⊢ (fun e ↦ (H ⟨↑e, ⋯⟩).2) ((fun i ↦ ⟨↑(H.symm (⟨x, hxU⟩, i)), ⋯⟩) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
e : ↑(f ⁻¹' {x})
⊢ (H (Set.inclusion ⋯ ((fun i ↦ ⟨↑(H.symm (⟨x, hxU⟩, i)), ⋯⟩) ((fun e ↦ (H ⟨↑e, ⋯⟩).2) e)))).2 =
    (H (Set.inclusion ⋯ e)).2

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x y : X
x✝ : y ∈ (hf.localInverseAt x).target
⊢ f y = ↑(hf.localInverseAt x).symm y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ ↑(hf.localInverseAt x) (f x) ∈ (hf.localInverseAt x).target

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
x✝ : ↑(f ⁻¹' t.baseSet)
⊢ ↑({ toFun := fun e ↦ (⟨f ↑e, ⋯⟩, (↑t ↑e).2), invFun := fun xi ↦ ⟨t.invFun (↑xi.1, xi.2), ⋯⟩, left_inv := ⋯,
            right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
          x✝).1 =
    f ↑x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G E
Y : Type u_4
inst✝ : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap (⇑φ ∘ f) G
x✝ : E
⊢ f x✝ = (⇑φ.symm ∘ ⇑φ ∘ f) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case h
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
x : X
e : ↑(f ⁻¹' {x})
this✝ : MulAction G ↑(f ⁻¹' {x}) := ⋯
this : MulAction.IsPretransitive G ↑(f ⁻¹' {x})
g : G
⊢ ↑(((hf.toPermFiber x) g) e) = ↑(g • e)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
hxs : x ∈ s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
x✝ : ↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U)
⊢ (fun x ↦ ⟨⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩, ⋯⟩) ((fun e ↦ (⟨⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩, ⋯⟩, (H ⟨↑↑e, ⋯⟩).2)) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
hxs : x ∈ s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
x✝ : ↑(Subtype.val ⁻¹' U) × I
⊢ (fun e ↦ (⟨⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩, ⋯⟩, (H ⟨↑↑e, ⋯⟩).2)) ((fun x ↦ ⟨⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩, ⋯⟩) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
x : ↑s
f : E → ↑s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set ↑s
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
x✝ : E
⊢ x✝ ∈ Subtype.val ∘ f ⁻¹' Subtype.val '' U ↔ x✝ ∈ f ⁻¹' U

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
E' : Type u_4
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsEvenlyCovered (f ∘ ⇑g) x I
x✝ : E
⊢ f x✝ = ((f ∘ ⇑g) ∘ ⇑g.symm) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case e'_5
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
x✝ : E
⊢ f x✝ = (⇑g.symm ∘ ⇑g ∘ f) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case e'_6
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ x = g.symm (g x)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: case e'_5
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
x✝¹ x✝ : AddCircle p
⊢ n • x✝ = ↑n • x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: case e'_6
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
x✝¹ : AddCircle p
x✝ : 𝕜
⊢ ((nsmulAddMonoidHom n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝ =
    ((zsmulAddGroupHom ↑n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: case e'_7
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
e_6✝ : ↥(nsmulAddMonoidHom n).ker = ↥(zsmulAddGroupHom ↑n).ker
x✝ : 𝕜
⊢ ((nsmulAddMonoidHom n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝ =
    ((zsmulAddGroupHom ↑n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝

Tactic:
simp

Goal state after: