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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
a✝ : Nontrivial A
⊢ ‖((addEquiv 𝕜 A) x).2‖ ≤
    max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖ +
      max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖

Tactic:
calc
      ‖x.snd‖ = ‖mul 𝕜 A x.snd‖ :=
        .symm <| (isometry_mul 𝕜 A).norm_map_of_map_zero (map_zero _) _
      _ ≤ ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ + ‖x.fst‖ := by
        simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
          norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
      _ ≤ _ := add_le_add le_sup_right le_sup_left

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
hx₂ : x ∈ U
⊢ {s | (s ∩ U).Nonempty} ∈ 𝓝 s

Tactic:
rw [← hU.mem_nhds_iff, mem_nhds_iff] at hx₂

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
hx₂ : ∃ V ∈ 𝓤 α, ball x V ⊆ U
⊢ {s | (s ∩ U).Nonempty} ∈ 𝓝 s
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
r : ℝ≥0
hr : ∀ k ∈ σ a, ‖k‖₊ < r
⊢ ∀ x ∈ σ a, ‖x‖ₑ < ↑r

Tactic:
simpa using hr

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z ↦ resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ 1
⊢ resolvent a =ᶠ[cobounded 𝕜] fun z ↦ z⁻¹ • resolvent (z⁻¹ • a) 1

Tactic:
by
      filter_upwards [isBounded_singleton (x := 0)] with z hz
      lift z to 𝕜ˣ using Ne.isUnit hz
      simpa [Units.smul_def] using congr(z⁻¹ • $(units_smul_resolvent_self (r := z) (a := a)))

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
simp_rw [nhds_eq_comap_uniformity,
    uniformity_hasBasis_open.uniformity_hausdorff |>.comap _ |>.ge_iff, Function.comp_id,
    hausdorffEntourage, Set.preimage_ofPred_eq, Set.ofPred_and]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a | s ⊆ i'.preimage a} ∩ {a | a ⊆ i'.image s} ∈ 𝓝 s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
⊢ s ⤳ t ↔ (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s

Tactic:
by
  refine ⟨fun h => ⟨fun x hx => ?_, subset_closure_of_specializes h⟩, fun ⟨hst, hts⟩ => ?_⟩
  · obtain ⟨y, hyt, hxy⟩ := h.mem_closed (s := {u | (u ∩ closure {x}).Nonempty})
      (isClosed_inter_nonempty_of_isClosed isClosed_closure) ⟨x, hx, subset_closure rfl⟩
    exact ⟨y, hyt, specializes_iff_mem_closure.mpr hxy⟩
  · simp_rw [Specializes, nhds_generateFrom, le_iInf₂_iff]
    rintro _ ⟨hs, ⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩⟩
    · refine iInf₂_le U.powerset ⟨fun x hx => ?_, .inl <| mem_image_of_mem _ hU⟩
      obtain ⟨y, hyt, hxy⟩ := hst x hx
      exact hxy.mem_open hU <| hs hyt
    · obtain ⟨x, hxt, hxU⟩ := hs
      obtain ⟨y, hyU, hys⟩ := mem_closure_iff.mp (hts hxt) U hU hxU
      exact iInf₂_le {t | (t ∩ U).Nonempty} ⟨⟨y, hys, hyU⟩, .inr <| mem_image_of_mem _ hU⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ map (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ) ≤ 𝓝 ((algebraMap 𝕜 ↥S) μ - x)

Tactic:
rw [← Filter.Tendsto, ← ContinuousAt]; fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_2
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ∀ᶠ (a : 𝕜) in 𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ, IsUnit ((algebraMap 𝕜 ↥S) a - x)

Tactic:
apply Eventually.filter_mono inf_le_right

Goal state after:
case refine_2
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓟 (σ 𝕜 x)ᶜ, IsUnit ((algebraMap 𝕜 ↥S) x_1 - x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ‖(cfcHom ha) { toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ }‖ < c

Tactic:
simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)]

Goal state after:
case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ∀ x ∈ (fun x ↦ ‖f x‖) '' σ 𝕜 a, x < c
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ (algebraMap 𝕜₁ 𝕜₂) x ∈ spectrum 𝕜₂ a

Tactic:
exact (spectrum.algebraMap_mem_iff _).mpr hx

Goal state after:
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
⊢ (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a

Tactic:
by
  obtain ⟨x, hx₁, hx₂⟩ := spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty ha
  rw [← hx₂, ENNReal.toNNReal_coe, ← spectrum.algebraMap_mem_iff ℝ, NNReal.algebraMap_eq_coe]
  have : 0 ≤ x := ha'.rightInvOn hx₁ ▸ NNReal.zero_le_coe
  convert! hx₁
  simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_2
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : CompleteSpace A
⊢ UpperHemicontinuous (quasispectrum ℝ≥0)

Tactic:
by
  obtain ⟨⟨h₁, -⟩, h₂⟩ := NNReal.isClosedEmbedding_coe
  simpa [← NNReal.algebraMap_eq_coe] using
    upperHemicontinuous_quasispectrum ℝ A |>.isInducing_comp h₁ h₂

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ x = 0 ∨ x ∈ σ 𝕜 a

Tactic:
by
        simpa [quasispectrum_eq_spectrum_union_zero] using hx

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
x : α
hx₁ : x ∈ ↑K
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {K | ↑K ⊆ W} ∈ 𝓝ˢ ((fun a ↦ {a_1 | (↑a_1 ∩ a).Nonempty}) U)ᶜ

Tactic:
simp_rw [(isOpen_subsets_of_isOpen hW).mem_nhdsSet, compl_ofPred, not_nonempty_iff_eq_empty,
        ← disjoint_iff_inter_eq_empty, ← subset_compl_iff_disjoint_right]
      gcongr

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ t
hr' : r = ‖↑r‖ * 1
hr'' : ↑r ≠ 0
⊢ IsOpen[inst✝⁷] ((gaugeSeminormFamily 𝕜 E S).ball 0 (‖↑r‖ * 1))

Tactic:
← Seminorm.smul_ball_zero hr'',

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ t
hr' : r = ‖↑r‖ * 1
hr'' : ↑r ≠ 0
⊢ IsOpen[inst✝⁷] (↑r • (gaugeSeminormFamily 𝕜 E S).ball 0 1)
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: 𝕜✝ : Type u_1
E : Type u_2
F✝ : Type u_3
inst✝⁷ : RCLike 𝕜✝
𝕜 : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
smulI : F →L[ℝ] F := ContinuousLinearMap.restrictScalars ℝ (I • ContinuousLinearMap.id 𝕜 F)
mulI : 𝕜 →L[ℝ] 𝕜 := (mul ℝ 𝕜) I
⊢ Continuous (ContinuousLinearMap.restrictScalars ℝ ∘ (↑extendRCLikeₗ).toFun)

Tactic:
exact ofRealCLM.postcomp F - mulI.postcomp F ∘L smulI.precomp 𝕜 ∘L ofRealCLM.postcomp F
      |>.continuous

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
𝕜₁ : 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
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i ↦ (q k) ((𝓕 i) x))
k : κ
⊢ BddAbove (range fun k_1 ↦ (q k).comp ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous[inst✝⁵.toTopologicalSpace, _] (⨆ k_1, ⇑((q k).comp ((toLinearMap ∘ 𝓕) k_1)))

Tactic:
have : BddAbove (range fun i ↦ (q k).comp (𝓕 i).toLinearMap) := by
    rw [Seminorm.bddAbove_range_iff]
    exact H k

Goal state after:
ι : Type u_2
κ : Type u_3
𝕜₁ : 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
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i ↦ (q k) ((𝓕 i) x))
k : κ
this : BddAbove (range fun i ↦ (q k).comp ↑(𝓕 i))
⊢ BddAbove (range fun k_1 ↦ (q k).comp ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous[inst✝⁵.toTopologicalSpace, _] (⨆ k_1, ⇑((q k).comp ((toLinearMap ∘ 𝓕) k_1)))
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
⊢ a✝ ∈ c.left.U → dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n → dist (c.lim a✝) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
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
⊢ dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n → dist (c.lim a✝) (c.lim x) ≤ (3 / 4) ^ (n + 1)
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.right.Cᶜ
y : X
⊢ y ∈ c.left.right.Cᶜ →
    dist (c.left.right.lim y) (c.left.right.lim x) ≤ (3 / 4) ^ n →
      dist (c.right.lim y) (c.right.lim x) ≤ (3 / 4) ^ n → dist (c.lim y) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
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.right.Cᶜ
y : X
hyl : y ∈ c.left.right.Cᶜ
⊢ dist (c.left.right.lim y) (c.left.right.lim x) ≤ (3 / 4) ^ n →
    dist (c.right.lim y) (c.right.lim x) ≤ (3 / 4) ^ n → dist (c.lim y) (c.lim x) ≤ (3 / 4) ^ (n + 1)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: case snd
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²⁸ : CommSemiring R
inst✝²⁷ : CommRing S
inst✝²⁶ : Nontrivial R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Algebra R S
inst✝²⁰ : NonUnitalRing A
inst✝¹⁹ : NonUnitalRing B
inst✝¹⁸ : Module S A
inst✝¹⁷ : Module R A
inst✝¹⁶ : Module R B
inst✝¹⁵ : Module S B
inst✝¹⁴ : SMulCommClass R A A
inst✝¹³ : SMulCommClass R B B
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : StarRing A
inst✝⁹ : StarRing B
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst✝³ : NonUnitalContinuousFunctionalCalculus R A pa
inst✝² : NonUnitalContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMapZero.UniqueHom R A
inst✝ : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
hf₀ : f 0 = 0
⊢ (cfcₙ f (a, b)).2 = (cfcₙ f a, cfcₙ f b).2

Tactic:
case snd =>
      let φ := NonUnitalStarAlgHom.snd S A B
      exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb

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

Goal state before:
pp: case pos
X : Type u_1
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✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ Tendsto (fun x ↦ cfc (F x) a) l (𝓝 (cfc f a))

Tactic:
let s : Set X := {x | ContinuousOn (F x) (spectrum R a)}

Goal state after:
case pos
X : Type u_1
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✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
⊢ Tendsto (fun x ↦ cfc (F x) a) l (𝓝 (cfc f a))
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
a : A
n : ℕ
ha : 0 ≤ a
⊢ a ^ ↑n = a ^ n

Tactic:
by
  rw [← cfc_pow_id (R := ℝ≥0) a n, rpow_def]
  congr
  simp

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
r : ℝ
hr : r > 0
hr_le : ∀ x ∈ spectrum ℝ a, r ≤ x
⊢ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
exact (hr.trans_le <| hr_le · ·)

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
n : ℕ
ha : 0 ≤ a
⊢ ‖a‖ ≤ ↑n ↔ a ≤ ↑n

Tactic:
simpa using norm_le_iff_le_algebraMap a n.cast_nonneg

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

Tactic:
lift b to Aˣ using hb.isUnit

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
⊢ a ≤ ↑b ↔ ‖sqrt a * ↑b ^ (-(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
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
le_iff_norm_sqrt_mul_sqrt_inv hb_inv ha_inv,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a⁻¹⁻¹‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive ↑a
hab : ↑a ≤ ↑b
⊢ ↑b ^ (-1) ≤ ↑a ^ (-1)

Tactic:
rpow_neg_one_eq_inv a,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive ↑a
hab : ↑a ≤ ↑b
⊢ ↑b ^ (-1) ≤ ↑a⁻¹
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ cfcₙ f (cfcₙ g a) ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)

Tactic:
have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
      exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
        (cfcₙ_nonneg_of_predicate.trans hab') hab'

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i ↦ ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊) = Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊

Tactic:
by
      simp_rw [@Finset.sum_comm m, Finset.mul_sum]

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

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : PartialOrder A₂
inst✝¹ : StarOrderedRing A₁
inst✝ : StarOrderedRing A₂
f g : A₁ →CP A₂
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    cases f
    cases g
    congr
    apply DFunLike.coe_injective
    exact h

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
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
⊢ star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m

Tactic:
rw [cfc_mul _ _ m (continuousOn_id' _ |>.fun_mul hg') (continuousOn_id' _),
    cfc_mul _ _ m (continuousOn_id' _) hg', cfc_id' .., hm₁.star_eq]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
⊢ m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = m * cfc (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) m * m