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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : ¬(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2 = 0
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖

Tactic:
have : ‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 ≤
          ‖(Unitization.splitMul 𝕜 E (star x)).snd‖ * ‖(Unitization.splitMul 𝕜 E x).snd‖ :=
          (norm_splitMul_snd_sq 𝕜 x).trans <| by
            rw [map_mul, Prod.snd_mul]
            exact norm_mul_le _ _
        rw [sq] at this
        rw [← Ne, ← norm_pos_iff] at h
        simp only [Unitization.splitMul_apply, Unitization.snd_star,
          Unitization.fst_star] at this
        exact (mul_le_mul_iff_left₀ h).mp this

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_2
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 ↑s).NeBot
hxφ : φ x = 0
this : Tendsto (fun y ↦ y - φ y • 1) (𝓝 x ⊓ 𝓟 ↑s) (𝓝 x)
g : A
⊢ g ∈ ↑s → g - φ g • 1 ∈ ↑s ∩ ↑(RingHom.ker φ)

Tactic:
hg

Goal state after:
case refine_2
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 ↑s).NeBot
hxφ : φ x = 0
this : Tendsto (fun y ↦ y - φ y • 1) (𝓝 x ⊓ 𝓟 ↑s) (𝓝 x)
g : A
hg : g ∈ ↑s
⊢ g - φ g • 1 ∈ ↑s ∩ ↑(RingHom.ker φ)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id s) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
⊢ a * φ f = 0

Tactic:
induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simp [map_zero]
  | id => exact hmul_id
  | star_id => exact hmul_star_id
  | add _ _ h₁ h₂ => simp only [map_add, mul_add, h₁, h₂, zero_add]
  | mul _ _ h _ => simp only [map_mul, ← mul_assoc, h, zero_mul]
  | smul _ _ h => rw [map_smul, mul_smul_comm, h, smul_zero]
  | frequently f h => exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed[TopologicalSpace.vietoris α] {t | t ⊆ F}

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsOpen[TopologicalSpace.vietoris α] {t | t ⊆ F}ᶜ
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
F : Set α
hF : IsClosed[inst✝.toTopologicalSpace] F
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {t | t ⊆ F}

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
F : Set α
hF : IsClosed[inst✝.toTopologicalSpace] F
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {t | t ⊆ F}ᶜ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
⊢ IsClosed[t] (range fun x ↦ {x})

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
⊢ IsOpen[t] (range fun x ↦ {x})ᶜ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {K | ↑K ⊆ F}

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsOpen {K | ↑K ⊆ F}ᶜ
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ (↑‖x‖₊).toNNReal ∈ spectrum ℝ≥0 a

Tactic:
ENNReal.toNNReal_coe,

Goal state after:
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ ‖x‖₊ ∈ spectrum ℝ≥0 a
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: z w : ℂ
⊢ (convexHull ℝ) (⇑equivRealProd.symm '' {(z.re, z.im), (z.re, w.im), (w.re, z.im), (w.re, w.im)}) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}

Tactic:
image_insert_eq,

Goal state after:
z w : ℂ
⊢ (convexHull ℝ)
      (insert (equivRealProd.symm (z.re, z.im))
        (insert (equivRealProd.symm (z.re, w.im))
          (insert (equivRealProd.symm (w.re, z.im)) (⇑equivRealProd.symm '' {(w.re, w.im)})))) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ quasispectrum ℝ≥0 a
⊢ x ≤ ‖a‖₊

Tactic:
Unitization.quasispectrum_eq_spectrum_inr' ℝ≥0 ℂ

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 ↑a
⊢ x ≤ ‖a‖₊
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

Tactic:
have h₁ : ha₁.unit⁻¹ * star a * a = 1 := mul_assoc _ _ a ▸ ha₁.val_inv_mul

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
h₁ : ↑ha₁.unit⁻¹ * a⋆ * a = 1
⊢ IsUnit a
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected {K | (↑K).Nonempty ∧ ↑K ⊆ s}

Tactic:
refine (isPreconnected_nonempty_finite_subsets hs).subset_closure (by grind) ?_

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ {K | (↑K).Nonempty ∧ ↑K ⊆ s} ⊆ closure {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ s}
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist (g x) 0 < ε / 2
⊢ ε / 2 + ε / 2 ≤ ε

Tactic:
add_halves ε

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist (g x) 0 < ε / 2
⊢ ε ≤ ε
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := hu'.fintype
⊢ (univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {a | (∀ (i : ↑u), ↑(a i) ⊆ ⋃₀ u) ∧ (∀ U ∈ u, ((⋃ a_2, ↑(a a_2)) ∩ U).Nonempty) ∧ (⋃ a_1, ↑(a a_1)).Finite}

Tactic:
refine fun f hf => ⟨by grind, fun U hU => ?_, finite_iUnion (by grind)⟩

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f✝ : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := hu'.fintype
f : ↑u → Compacts α
hf : f ∈ univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}
U : Set α
hU : U ∈ u
⊢ ((⋃ a, ↑(f a)) ∩ U).Nonempty
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ZeroLEOneClass 𝕜
s : Set E
⊢ 0 ∈ s ∧ IsOpen[inst✝⁴] s ∧ AbsConvex 𝕜 s → ∃ i, (i ∈ 𝓝 0 ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s

Tactic:
⟨hs_zero, hs_open, hs_balanced, hs_convex⟩

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ZeroLEOneClass 𝕜
s : Set E
hs_zero : 0 ∈ s
hs_open : IsOpen[inst✝⁴] s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex 𝕜 s
⊢ ∃ i, (i ∈ 𝓝 0 ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected {K | ↑K ⊆ s}

Tactic:
rw [← isEmbedding_toCompacts.isPreconnected_image]
  convert Compacts.isPreconnected_nonempty_subsets hs
  exact subset_antisymm
    (image_subset_iff.mpr fun K hK => ⟨K.nonempty, hK⟩)
    (fun K hK => ⟨⟨K, hK.1⟩, hK.2, rfl⟩)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : Module ℝ E := restrictScalars ℝ 𝕜 E
this : IsScalarTower ℝ 𝕜 E := IsScalarTower.restrictScalars ℝ 𝕜 E
fr : Dual ℝ ↥S := reLm ∘ₗ ↑ℝ f
g : Dual ℝ E
hg : ∀ (x : ↥S), g ↑x = fr x
hgp : ∀ (x : E), |g x| ≤ (Seminorm.restrictScalars ℝ p) x
x : ↥S
⊢ ↑(fr x) - I * ↑(g ↑(I • x)) = f x

Tactic:
hg

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : Module ℝ E := restrictScalars ℝ 𝕜 E
this : IsScalarTower ℝ 𝕜 E := IsScalarTower.restrictScalars ℝ 𝕜 E
fr : Dual ℝ ↥S := reLm ∘ₗ ↑ℝ f
g : Dual ℝ E
hg : ∀ (x : ↥S), g ↑x = fr x
hgp : ∀ (x : E), |g x| ≤ (Seminorm.restrictScalars ℝ p) x
x : ↥S
⊢ ↑(fr x) - I * ↑(fr (I • x)) = f x
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup E
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝ : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded 𝕜₂ (range fun i ↦ (𝓕 i) x)
⊢ UniformEquicontinuous (DFunLike.coe ∘ 𝓕)

Tactic:
have hp := PolynormableSpace.withSeminorms 𝕜₂ F
  refine hp.banach_steinhaus ?_
  simp_rw [hp.isVonNBounded_iff_seminorm_bddAbove, ← range_comp] at H
  exact fun q x ↦ H x q

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
P : Type u_3
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
⊢ edist (k • x) (k • y) = ↑‖k‖₊ * edist x y

Tactic:
exact edist_smul₀ ..

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x)

Tactic:
by
  refine tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 ?_)
  simp only [approx]
  exact (c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (c.left.lim a✝) (c.right.lim a✝)) (midpoint ℝ (c.left.lim x) (c.right.lim x)) ≤ 3 / 4 * (3 / 4) ^ n

Tactic:
c.right.lim_of_mem_C _ (c.left_U_subset_right_C hyl),

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (c.left.lim a✝) 0) (midpoint ℝ (c.left.lim x) (c.right.lim x)) ≤ 3 / 4 * (3 / 4) ^ n
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
⊢ 0 < slope f x₀ b ↔ f b < f x₀

Tactic:
by
  rw [slope_comm, slope_pos_iff hb]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ b ∈ ↑I, dist f b < ↑ε

Tactic:
simp_rw [dist_nndist]

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ b ∈ ↑I, ↑(nndist f b) < ↑ε
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t →
      (∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t, 0 < g' x) →
        ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ s, 0 < g' x

Tactic:
rintro s₁ s₂ hs ⟨g, hI, hgt⟩

Goal state after:
case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
hs : s₁ ⊆ s₂
g : C(X, ℝ≥0)
hI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hgt : ∀ x ∈ s₂, 0 < g x
⊢ ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ s₁, 0 < g' x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this✝ : Fact (0 ∈ s)
mul₁ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0
mul₂ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hc' hcs) f * (cfcₙHomSuperset hb' hbs) g = 0
ψ : C(↑s, ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src := ↑(cfcₙHomSuperset hb' hbs) + ↑(cfcₙHomSuperset hc' hcs);
  { toFun := ⇑(cfcₙHomSuperset hb' hbs) + ⇑(cfcₙHomSuperset hc' hcs), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
    map_mul' := ⋯, map_star' := ⋯ }
this : UniqueHom ℝ A
⊢ (cfcₙHomSuperset ha has) (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)

Tactic:
by simpa [ψ, -cfcₙHomSuperset_apply, cfcₙHomSuperset_id, sub_eq_add_neg] using habc

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖a‖ = max ‖a⁺‖ ‖a⁻‖

Tactic:
refine le_antisymm ?_ <| max_le (norm_posPart_le a) (norm_negPart_le a)

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖a‖ ≤ max ‖a⁺‖ ‖a⁻‖
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
this : cfcₙ (fun x ↦ √x * √x) a = cfcₙ (fun x ↦ x) a
⊢ sqrt a = cfcₙ Real.sqrt a

Tactic:
rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] at this

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
y : ℝ
f : ℝ → ℝ
hf₁ : ∀ x ∈ spectrum ℝ a, 0 < f x
hf₂ : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
hg : ContinuousOn (fun r ↦ r ^ y) (f '' spectrum ℝ a)
⊢ 0 ≤ cfc f a

Tactic:
grind [cfc_nonneg]

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

Goal state before:
pp: case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf : f ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
g : R →ᵤ[{spectrum R a}] R
⊢ g ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)} →
    edist ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) f) ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) g) ≤ ↑1 * edist f g

Tactic:
hg

Goal state after:
case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf : f ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
g : R →ᵤ[{spectrum R a}] R
hg : g ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
⊢ edist ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) f) ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) g) ≤ ↑1 * edist f g
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
h : IsUnit a
hx : x ≠ 0
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
by_cases hnonneg : 0 ≤ a
  case pos =>
    have : IsStrictlyPositive a := by grind
    simp [sqrt_eq_rpow, div_eq_mul_inv, one_mul, rpow_rpow _ _ _ hx]
  case neg =>
    simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a hnonneg]

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
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ a ≤ ↑b ↔ ‖sqrt a * ↑b ^ (-1 * (1 / 2))‖ ≤ 1

Tactic:
le_iff_norm_sqrt_mul_rpow a (hb := b.isUnit.isStrictlyPositive hb)

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * ↑b ^ (-1 * (1 / 2))‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
⊢ ↑a⁻¹ ≤ ↑b ↔ ↑b⁻¹ ≤ ↑a

Tactic:
by
  simpa using CStarAlgebra.inv_le_inv_iff ha (inv_nonneg_of_nonneg b hb)

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
z : A
hz : z ∈ {x | 0 ≤ x} ∩ ball 0 1 ∧ (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
⊢ 0 ≤ z ∧ ‖z‖ < 1

Tactic:
simpa using hz.1

Goal state after: