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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfcₙ f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfcₙ f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : ContinuousStar A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, quasispectrum 𝕜 (a x))
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfcₙ f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : ContinuousStar A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ :
  (f, a) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f, a).2)
hs : IsCompact (quasispectrum ℝ≥0 a)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}
⊢ ContinuousOn (fun fa ↦ cfcₙ ((toFun {k}) ((ofFun {k}) ((toFun {t | IsCompact t ∧ t ⊆ s}) fa.1))) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
        {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)} ∩
      Set.univ ×ˢ {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)})

Tactic:
refine continuousOn_cfcₙ_nnreal_setProd hk |>.comp'
    (uniformContinuous_ofFun_toFun_of_mem _ {t | IsCompact t ∧ t ⊆ s} _ ⟨hk, hks⟩ |>.prodMap
      uniformContinuous_id).continuous.continuousOn ?_

Goal state after:
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ :
  (f, a) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f, a).2)
hs : IsCompact (quasispectrum ℝ≥0 a)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}
⊢ Set.MapsTo (fun fa ↦ fa)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
        {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)} ∩
      Set.univ ×ˢ {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)})
    ({f | ContinuousOn ((toFun {k}) f) k ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ k})
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
  rfl

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfcₙ f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum ℝ≥0 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfcₙ f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : ContinuousOn a Set.univ
ha : ∀ (x : X), quasispectrum ℝ≥0 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹³ : NonUnitalNormedRing A
inst✝¹² : StarRing A
inst✝¹¹ : NormedSpace ℝ A
inst✝¹⁰ : IsScalarTower ℝ A A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : ContinuousStar A
inst✝⁷ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, quasispectrum ℝ≥0 (a x))
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfcₙ f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹³ : NonUnitalNormedRing A
inst✝¹² : StarRing A
inst✝¹¹ : NormedSpace ℝ A
inst✝¹⁰ : IsScalarTower ℝ A A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : ContinuousStar A
inst✝⁷ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: case inr
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : 0 < ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
exact le_of_mul_le_mul_right this h

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ cobounded (CStarMatrix m n A) = cobounded (m → n → A)

Tactic:
have : cobounded (CStarMatrix m n A) = Filter.comap ofMatrix.symm (cobounded _) := by
    refine le_antisymm ?_ ?_
    · exact antilipschitzWith_toMatrixAux.tendsto_cobounded.le_comap
    · exact lipschitzWith_toMatrixAux.comap_cobounded_le
  exact this.trans Filter.comap_id

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
a : A
x : f.PreGNS
this : star (f.ofPreGNS x) * star a * (a * f.ofPreGNS x) ≤ ‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x
⊢ f (‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x) = ↑(‖a‖ ^ 2 * ‖x‖ ^ 2)

Tactic:
simp [← Complex.coe_smul, preGNS_norm_sq, smul_mul_assoc]

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
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ (f ∘ e.invFun) (extend f (↑e) (fun x ↦ Classical.arbitrary Z) x) = x

Tactic:
rw [← hxx₀, hf.injective.extend_apply e, comp_apply]

Goal state after:
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
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ f (e.invFun (↑e x₀)) = f x₀
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
⊢ x ∈ e.target ↔ x.1 ∈ e.baseSet

Tactic:
rw [e.target_eq, prod_univ, mem_preimage]

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
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : ∀ (x : B), Nonempty (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∈ e.baseSet
y : F
⊢ { proj := b, snd := e.symm b y } = ↑e.symm (b, y)

Tactic:
simp only [e.symm_apply hb, TotalSpace.mk_cast (e.proj_symm_apply' hb), TotalSpace.eta]

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
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
x✝ : Z
⊢ x✝ ∈ Subtype.val '' e.source →
    ↑(e.invFun (if h : proj x✝ ∈ s then ↑e ⟨x✝, h⟩ else (proj x✝, Classical.arbitrary (Z → F) x✝))) = x✝

Tactic:
by rintro ⟨⟨z, hzp : proj z ∈ s⟩, hze, rfl⟩; simp [hzp, e.symm_apply_apply hze]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
n : ℕ
a : A
ha : IsStrictlyPositive a
⊢ log (a ^ n) = n • log a

Tactic:
by
  grind [log_pow]

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
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝² : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝³ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝² : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝¹ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝¹ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this✝ : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h✝ : IsOpen[inst✝²] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
e' : E
h : e' ∈ f ⁻¹' s ∩ (φ e).source
e'' : E
left✝ : e'' ∈ V ↑e
mem : e'' ∈ (φ e).source
eq : f e'' = f e'
⊢ ↑(φ e) e'' = ↑(φ e) e'

Tactic:
by rwa [(hφ e).2]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ (Filter.map (⇑exp) (nhds 0)).HasBasis (fun x ↦ True) fun n ↦ centeredArc (π / 2 ^ (n + 1))

Tactic:
simp_rw [centeredArc, abs_lt, Set.Ioo_def, ← Real.ball_zero_eq_Ioo]

Goal state after:
⊢ (Filter.map (⇑exp) (nhds 0)).HasBasis (fun x ↦ True) fun n ↦ ⇑exp '' Metric.ball 0 (π / 2 ^ (n + 1))
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
⊢ ContinuousOn (fun x ↦ ↑x.arg) ((fun x ↦ NormedSpace.exp (I • x)) '' spectrum ℂ ↑x)

Tactic:
refine continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
⊢ (fun x ↦ NormedSpace.exp (I • x)) '' spectrum ℂ ↑x ⊆ slitPlane
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
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
have : DiscreteTopology (f ⁻¹' {x}) :=
    (IsDiscrete.of_openPartialHomeomorph f subset_rfl h).1
  /- for each preimage e of x, choose a homeomorphism φₑ
    from a neighborhood of e to its image -/
  choose φ hφ using fun e : f ⁻¹' {x} ↦ h e e.2
  -- separately, choose pairwise disjoint neighborhoods Vₑ by Hausdorff-ness
  have ⟨V, hV, disj⟩ := fin.t2_separation
  -- let Vₑ' be the intersection Vₑ ∩ dom(φₑ)
  let V' (e : f ⁻¹' {x}) := V e ∩ (φ e).source
  have hV' e : IsOpen (V' e) := (hV e).2.inter (φ e).open_source
  have : ⋃ e, V' e ∈ nhdsSet (f ⁻¹' {x}) :=
    (isOpen_iUnion hV').mem_nhdsSet.2 fun e he ↦ mem_iUnion_of_mem ⟨e, he⟩ ⟨(hV e).1, (hφ _).1⟩
  -- since f is a closed map, the union of the Vₑ' contains the preimage of a neighborhood U of x
  have ⟨W, hWx, hWV⟩ := isClosedMap_iff_comap_nhds_le.mp hf this
  cases isEmpty_or_nonempty (f ⁻¹' {x})
  · exact .of_preimage_eq_empty _ hWx (by simpa using hWV)
  have ⟨U, hUW, hU, hxU⟩ := mem_nhds_iff.mp hWx
  -- show that the intersection of U with the images of Vₑ' is evenly covered
  let U' := U ∩ ⋂ e : f ⁻¹' {x}, f '' (V' e)
  have : Finite (f ⁻¹' {x}) := fin
  have hU' : IsOpen U' := hU.inter <| isOpen_iInter_of_finite fun e ↦ by
    convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right; exact (hφ e).2
  have hUV e : U' ⊆ f '' V' e := inter_subset_right.trans (iInter_subset ..)
  have : Nonempty E := ⟨Classical.arbitrary (f ⁻¹' {x})⟩
  refine .of_trivialization (t := hU'.trivializationDiscrete _ _
    (fun e s hs ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩) (fun e ↦ ?_)
    (fun e ↦ .mono subset_rfl (hUV e) (surjOn_image f _))
    (pairwise_disjoint_mono disj.subtype fun e ↦ inter_subset_left)
    ((preimage_mono (inter_subset_left.trans hUW)).trans hWV))
    ⟨hxU, Set.mem_iInter.mpr fun e ↦ ⟨e, ⟨(hV e).1, (hφ e).1⟩, e.2⟩⟩
  · convert! ((φ e).isOpen_inter_preimage h).inter (hV e).2 using 1
    simp_rw [(hφ e).2, V']; ac_rfl
  · have : s ⊆ (φ e).target := hs.trans <| (hUV e).trans <| by
      rw [← (φ e).image_source_eq_target, (hφ e).2]; exact image_mono inter_subset_right
    rw [← (φ e).isOpen_symm_image_iff_of_subset_target this,
      (φ e).symm_image_eq_source_inter_preimage this, (hφ e).2, inter_comm]
    convert! h using 1
    refine inter_eq_inter_iff_left.mpr ⟨fun e' h ↦ h.2.2, fun e' h ↦ ⟨?_ , h.2⟩⟩
    have ⟨e'', ⟨_, mem⟩, eq⟩ := mem_iInter.mp (hs h.1).2 e
    rwa [← (φ e).injOn mem h.2 (by rwa [(hφ e).2])]
  · convert! ← (φ e).injOn.mono inter_subset_right; exact (hφ e).2

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : x ≠ 0
⊢ let u₁ := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯;
  let u₂ := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯;
  x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))

Tactic:
intro u₁ u₂
  rw [smul_add, smul_comm _ I, Unitary.coe_star, Unitary.coe_star,
    ← realPart_apply_coe (u₁ : A), ← realPart_apply_coe (u₂ : A)]
  simpa only [u₁, u₂, selfAdjoint.realPart_unitarySelfAddISMul, realPart_add_I_smul_imaginaryPart]
    using! Eq.symm <| NormedSpace.norm_smul_normalize x

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
hε : 0 < ε
huε' : dist u 1 < √ε
⊢ ContinuousOn (fun x ↦ ↑x.arg) (sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε})

Tactic:
refine continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
hε : 0 < ε
huε' : dist u 1 < √ε
⊢ sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε} ⊆ slitPlane
Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ
hT : T = c • ContinuousLinearMap.id ℝ ℝ
hcomp : ⇑T ∘ f = c • f
n : ℕ
x : ℝ
hx : x ∈ s
⊢ 0 ≤ c * (p x n) fun x ↦ 1

Tactic:
exact mul_nonneg hc (hp_nn n hx)

Goal state after: