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✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : C(↑s, 𝕜)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) f

Tactic:
by
  open scoped ContinuousFunctionalCalculus in
  have : CompactSpace s := by rwa [isCompact_iff_compactSpace] at hs
  induction f using ContinuousMap.induction_on_of_compact with
  | const r =>
    have : ContinuousMap.const s r = algebraMap 𝕜 C(s, 𝕜) r := rfl
    simpa only [this, AlgHomClass.commutes] using! continuous_const
  | id =>
    simp only [cfcHomSuperset_id]
    fun_prop
  | star_id =>
    simp only [map_star, cfcHomSuperset_id]
    fun_prop
  | add f g hf hg => simpa using! hf.add hg
  | mul f g hf hg => simpa using! hf.mul hg
  | frequently f hf =>
    apply continuous_of_uniform_approx_of_continuous
    rw [Metric.uniformity_basis_dist_le.forall_iff (by aesop)]
    intro ε hε
    simp only [Set.mem_ofPred_eq, dist_eq_norm]
    obtain ⟨g, hg, g_cont⟩ := frequently_iff.mp hf (Metric.closedBall_mem_nhds f hε)
    simp only [Metric.mem_closedBall, dist_comm g, dist_eq_norm] at hg
    refine ⟨_, g_cont, fun x ↦ ?_⟩
    rw [← map_sub, cfcHomSuperset_apply]
    rw [isometry_cfcHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcHom (ha' x)))]
    rw [ContinuousMap.norm_le _ hε.le] at hg ⊢
    aesop

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : a * star a ≤ (algebraMap ℝ A) (‖a‖ * ‖a‖)
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
← pow_two

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : star a * a ≤ (algebraMap ℝ A) (‖a‖ * ‖a‖)
⊢ star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
← pow_two

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
⊢ star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
a : A
ha : (IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal) ∧ spectrum ℝ≥0 a ⊆ s
⊢ spectrum ℝ a ⊆ NNReal.toReal '' s

Tactic:
← ha.1.2.algebraMap_image

Goal state after:
A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
a : A
ha : (IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal) ∧ spectrum ℝ≥0 a ⊆ s
⊢ ⇑(algebraMap ℝ≥0 ℝ) '' spectrum ℝ≥0 a ⊆ NNReal.toReal '' s
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: x : ℝ≥0
⊢ x * (1 + x)⁻¹ = 1 - (1 + x)⁻¹

Tactic:
simp [field, mul_tsub]

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

Goal state before:
pp: case pos
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfcₙ f a) b

Tactic:
rw [cfcₙ_nnreal_eq_real ..]

Goal state after:
case pos
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfcₙ (fun x ↦ ↑(f x.toNNReal)) a) b
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf0 : f 0 = 0
this : Set.EqOn (cfcₙ f) (cfcₙ fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
a : A
ha : (IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) ∧ quasispectrum ℝ≥0 a ⊆ s
⊢ quasispectrum ℝ a ⊆ NNReal.toReal '' s

Tactic:
← ha.1.2.algebraMap_image

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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf0 : f 0 = 0
this : Set.EqOn (cfcₙ f) (cfcₙ fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
a : A
ha : (IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) ∧ quasispectrum ℝ≥0 a ⊆ s
⊢ ⇑(algebraMap ℝ≥0 ℝ) '' quasispectrum ℝ≥0 a ⊆ NNReal.toReal '' s
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
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
rw [ContinuousOn] at ha_cont ⊢
  refine fun x hx ↦ (ha_cont x hx).cfcₙ_nnreal (hs x hx) f hx ?_ ?_ (hf x hx)
  all_goals filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt
  exacts [hx, ha' x hxt]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : ↑e ≤ 1
⊢ 0 ≤ 2 - ↑e

Tactic:
sub_nonneg,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : ↑e ≤ 1
⊢ ↑e ≤ 2
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∀ x ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val, 0 ≤ x

Tactic:
intro x h_x

Goal state after:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : x ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val
⊢ 0 ≤ x
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: 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✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
⊢ ContinuousWithinAt (fun x ↦ TotalSpace.mk' F x (s x)) a x₀ ↔
    ContinuousWithinAt (fun x ↦ (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) a x₀

Tactic:
simp_rw [continuousWithinAt_totalSpace, and_iff_right_iff_imp]
  intro; exact continuousWithinAt_id

Goal state after:
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 e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv

Tactic:
rw [PartialEquiv.trans_symm_eq_symm_trans_symm, PartialEquiv.symm_symm]

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

Goal state before:
pp: case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ x ∈ Z.baseSet (Z.indexAt x)

Tactic:
apply_rules [mem_baseSet_at, mem_inter]

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

Goal state before:
pp: case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ x ∈ Z.baseSet (Z.indexAt x) ∩ Z.baseSet i ∩ Z.baseSet (Z.indexAt x)

Tactic:
apply_rules [mem_baseSet_at, mem_inter]

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

Goal state before:
pp: case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x ∈ Z.baseSet i ∧ True) ∧ x ∈ Z.baseSet j
⊢ True ∧ Z.coordChange (Z.indexAt x) j x (Z.coordChange i (Z.indexAt x) x v) = Z.coordChange i j x v

Tactic:
simp only [Z.coordChange_comp, hx, mem_inter_iff, and_self_iff, mem_baseSet_at]

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 →
    (if h : proj x✝ ∈ s then ↑e ⟨x✝, h⟩ else (proj x✝, Classical.arbitrary (Z → F) x✝)) ∈ e.target

Tactic:
by
    rintro ⟨⟨z, hzp : proj z ∈ s⟩, hze, rfl⟩
    simpa [hzp, e.coe_fst hze] using e.map_source hze

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case refine_1
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝¹ : f x₁ = f x₂
x✝ : x₁ ≠ x₂
h : Disjoint (𝓝 x₁) (𝓝 x₂)
⊢ (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)

Tactic:
← compl_diagonal_mem_prod

Goal state after:
case refine_1
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝¹ : f x₁ = f x₂
x✝ : x₁ ≠ x₂
h : (diagonal X)ᶜ ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
⊢ (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
k : 𝕜
x y : A
⊢ ((algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k).2 x * y = x * ((algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k).1 y

Tactic:
Prod.algebraMap_apply,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
k : 𝕜
x y : A
⊢ ((algebraMap 𝕜 (A →L[𝕜] A)) k) x * y = x * ((algebraMap 𝕜 (A →L[𝕜] A)) k) y
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
f : OpenPartialHomeomorph X Y
hx : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ∃ U, IsOpen[inst✝¹] U ∧ x ∈ U ∧ Set.InjOn (↑f) U

Tactic:
exact ⟨f.source, f.open_source, hx, f.injOn⟩

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

Goal state before:
pp: case refine_2.refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
key : ∀ (x y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : sqrt r < sSup ((fun x ↦ ‖a.toProd.1 x‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : sqrt r < (fun x ↦ ‖a.toProd.1 x‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ BddAbove ((fun x_1 ↦ ‖a.toProd.2 (star (a.toProd.1 (star (star x)))) * x_1‖₊) '' Metric.closedBall 0 1)

Tactic:
refine ⟨‖a‖₊ * ‖a‖₊, ?_⟩

Goal state after:
case refine_2.refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
key : ∀ (x y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : sqrt r < sSup ((fun x ↦ ‖a.toProd.1 x‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : sqrt r < (fun x ↦ ‖a.toProd.1 x‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ ‖a‖₊ * ‖a‖₊ ∈
    upperBounds ((fun x_1 ↦ ‖a.toProd.2 (star (a.toProd.1 (star (star x)))) * x_1‖₊) '' Metric.closedBall 0 1)
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℤ
hn : IsUnit ↑n
⊢ IsAddQuotientCoveringMap (fun x ↦ n • x) ↥(zsmulAddGroupHom n).ker

Tactic:
refine hn.isQuotientMap_zsmul (QuotientAddGroup.mk' _) isQuotientMap_quotient_mk'
    |>.isAddQuotientCoveringMap_of_isDiscrete_ker_addMonoidHom
    (f := zsmulAddGroupHom (α := AddCircle p) n)
    (Set.Finite.isDiscrete <| finite_torsion_of_isSMulRegular_int _ _ fun _ ↦ ?_)
  simp_rw [zsmul_eq_mul]
  apply hn.isSMulRegular 𝕜

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
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap (⇑g ∘ f)
⊢ IsCoveringMap f

Tactic:
convert! h.homeomorph_comp g.symm; ext; simp

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ Disjoint (⇑(x.path y) '' Ioc 0 1) (⇑(y.path x) '' Ioc 0 1)

Tactic:
have hdisj : Disjoint (Ioc x.val.arg (angleDiff x y + x.val.arg))
      (Ioc y.val.arg (angleDiff y x + y.val.arg)) := by grind [angleDiff]

Goal state after:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
⊢ Disjoint (⇑(x.path y) '' Ioc 0 1) (⇑(y.path x) '' Ioc 0 1)
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)
⊢ f '' V' e ⊆ (φ e).target

Tactic:
rw [← (φ e).image_source_eq_target, (hφ e).2]; exact image_mono inter_subset_right

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' ∈ V ↑e

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

Goal state after:
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 ?_
    rwa [expUnitary_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul ..,
      cfc_map_spectrum ..] at this

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
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ 0 ≤ 1 - a ^ 2

Tactic:
sub_nonneg,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a ^ 2 ≤ 1
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖A x‖ ^ 2 = re ⟪(adjoint A ∘SL A) x, x⟫_𝕜

Tactic:
by
  have h : ⟪(A† ∘L A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; rfl
  rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

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

Goal state before:
pp: case h.right
A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) := ⋯
u₂ : ↥(unitary A) := ⋯
this : x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))
⊢ ∀ (i : Fin 4), ‖![↑‖x‖ * 2⁻¹, ↑‖x‖ * 2⁻¹, ↑‖x‖ * 2⁻¹ * I, ↑‖x‖ * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2

Tactic:
intro i
      fin_cases i
      all_goals simp [div_eq_mul_inv]

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

Goal state before:

Tactic:
‖A x‖ = √(re ⟪(A† ∘L A) x, x⟫) := by rw [apply_norm_eq_sqrt_inner_adjoint_left]
      _ ≤ √(‖A† ∘L A‖ * ‖x‖ * ‖x‖) := Real.sqrt_le_sqrt this
      _ = √‖A† ∘L A‖ * ‖x‖ := by
        simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖),
          Real.sqrt_mul_self (norm_nonneg x)]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).centroid = s.centroid

Tactic:
by
  rw [centroid, centroid]
  simp only [centroid_eq_affineCombination]
  simp only [reindex]
  have h_eq : m = n := by simpa using Fintype.card_eq.2 ⟨e⟩
  subst h_eq
  convert! Finset.univ.affineCombination_map e.toEmbedding _ _ <;> simp [Function.comp_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case e_a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ 1 = ↑n * (↑n + 1)⁻¹ + (↑n + 1)⁻¹

Tactic:
have : (↑n + (1 : k))⁻¹ = 1 * (↑n + (1 : k))⁻¹ := by simp

Goal state after:
case e_a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
this : (↑n + 1)⁻¹ = 1 * (↑n + 1)⁻¹
⊢ 1 = ↑n * (↑n + 1)⁻¹ + (↑n + 1)⁻¹
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i = (↑n)⁻¹ • ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid

Tactic:
eq_vadd_iff_vsub_eq,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i -ᵥ s.centroid = (↑n)⁻¹ • ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid)