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

Goal state before:
pp: case neg.inr.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ (fun x ↦ -f x) a = -cfcₙ f a

Tactic:
cfcₙ_apply_of_not_continuousOn a hf,

Goal state after:
case neg.inr.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ (fun x ↦ -f x) a = -0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case e'_2.e'_4
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield 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✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).2 PUnit.unit = 0 PUnit.unit

Tactic:
exact map_zero v

Goal state after:
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
h : Function.Injective ⇑(mul 𝕜 A)
⊢ Function.Injective ⇑(splitMul 𝕜 A)

Tactic:
rw [injective_iff_map_eq_zero]
  intro x hx
  induction x
  rw [map_add] at hx
  simp only [splitMul_apply, fst_inl, snd_inl, map_zero, add_zero, fst_inr, snd_inr,
    zero_add, Prod.mk_add_mk, Prod.mk_eq_zero] at hx
  obtain ⟨rfl, hx⟩ := hx
  simp only [map_zero, zero_add, inl_zero] at hx ⊢
  rw [← map_zero (mul 𝕜 A)] at hx
  rw [h hx, inr_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ _root_.toContinuousMap ⁻¹' _root_.toContinuousMap '' closure ↑(adjoin 𝕜 {ContinuousMapZero.id s}) = Set.univ

Tactic:
← isClosedEmbedding_toContinuousMap.closure_image_eq,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ _root_.toContinuousMap ⁻¹' closure (_root_.toContinuousMap '' ↑(adjoin 𝕜 {ContinuousMapZero.id s})) = Set.univ
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (((𝓤 α).lift' hausdorffEntourage).lift' fun s ↦ SetRel.comp s s) ≤ (𝓤 α).lift' hausdorffEntourage

Tactic:
rw [Filter.le_lift']

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ s ∈ 𝓤 α, hausdorffEntourage s ∈ ((𝓤 α).lift' hausdorffEntourage).lift' fun s ↦ SetRel.comp s s
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
⊢ (fun z ↦ z⁻¹ • resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ ‖x⁻¹‖

Tactic:
simpa using (isBigO_refl (· ⁻¹) (cobounded 𝕜)).norm_right.smul 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
⊢ ‖cfc f a‖ < c

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A
  · simpa [Subsingleton.elim (cfc f a) 0]
  · refine cfc_cases (‖·‖ < c) a f (by simpa) fun hf ha ↦ ?_
    simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
x✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p := ⋯
⊢ IsScalarTower 𝕜 (Unitization 𝕜 A) (Unitization 𝕜 A)

pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
x✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p := ⋯
⊢ SMulCommClass 𝕜 (Unitization 𝕜 A) (Unitization 𝕜 A)

Tactic:
all_goals infer_instance

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : IsStrictlyPositive a
hb : IsStrictlyPositive b
⊢ Commute a b ↔ IsStrictlyPositive (a * b)

Tactic:
by
  rw [commute_iff_mul_nonneg ha.nonneg hb.nonneg]
  exact ⟨fun h => ha.isUnit.mul hb.isUnit |>.isStrictlyPositive h, fun h => h.nonneg⟩

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

Goal state before:
pp: A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ liminf (fun i ↦ 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop

Tactic:
let p : FormalMultilinearSeries ℂ ℂ A := fun n =>
    ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)

Goal state after:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
⊢ ↑r ≤ liminf (fun i ↦ 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop
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
    have h₂ : a * (star a * ha₂.unit⁻¹) = 1 := (mul_assoc a _ _).symm ▸ ha₂.mul_val_inv
    exact ⟨⟨a, ha₁.unit⁻¹ * star a, left_inv_eq_right_inv h₁ h₂ ▸ h₂, h₁⟩, rfl⟩

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ x‖₊ * ‖ψ x‖₊ ≤ ‖x‖₊ * ‖x‖₊

Tactic:
simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ (x⋆ * x)‖₊ ≤ ‖x⋆ * x‖₊
Module: Mathlib.Analysis.CStarAlgebra.Exponential

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
⊢ Continuous expUnitary

Tactic:
simp only [continuous_induced_rng, Function.comp_def, selfAdjoint.expUnitary_coe]
  let +nondep : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
  fun_prop

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
h : ∀ i ∈ S, ↑i ⊆ ⋃ i, U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ⋃ x ∈ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}, ↑x ⊆ ⋃ i ∈ s.biUnion id, U i

Tactic:
biUnion_iUnion,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
h : ∀ i ∈ S, ↑i ⊆ ⋃ i, U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ⋃ i ∈ s, ⋃ x ∈ {K | ↑K ⊆ ⋃ i_2 ∈ i, U i_2}, ↑x ⊆ ⋃ i ∈ s.biUnion id, U i
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
⊢ IsCompact (⋃ K ∈ S, ↑K)

Tactic:
rw [isCompact_iff_finite_subcover]
  intro ι U hU h
  rw [iUnion₂_subset_iff] at h
  obtain ⟨s, hs⟩ := hS.elim_finite_subcover
    (fun s : Finset ι => {K | (K : Set α) ⊆ ⋃ i ∈ s, U i})
    (fun s => isOpen_subsets_of_isOpen <| isOpen_biUnion fun _ _ => hU _)
    (fun K hK => mem_iUnion.mpr <| K.isCompact.elim_finite_subcover U hU <| h K hK)
  classical
  refine ⟨s.biUnion id, (biUnion_subset_biUnion_left hs).trans ?_⟩
  simp_rw [biUnion_iUnion, iUnion_subset_iff, Finset.set_biUnion_biUnion]
  exact fun t ht K hK => subset_iUnion₂_of_subset t ht hK

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

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ⇑f
⊢ Continuous[inst✝⁴, inst✝³] f'

Tactic:
rw [h]
    exact f.continuous_toFun

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
ι : Type u_2
F : ι → α →C₀ β
f : α →C₀ β
l : Filter ι
⊢ Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i ↦ ⇑(F i)) (⇑f) l

Tactic:
simpa only [Metric.tendsto_nhds] using!
    @BoundedContinuousFunction.tendsto_iff_tendstoUniformly _ _ _ _ _ (fun i => (F i).toBCF)
      f.toBCF l

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

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C₀ β
⊢ Tendsto (fun x ↦ star (f x)) (cocompact α) (𝓝 0)

Tactic:
simpa only [star_zero] using! (continuous_star.tendsto (0 : β)).comp (zero_at_infty f)

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

Goal state before:
pp: 𝕜 : 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 𝕜
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ 𝓝 0 ∧ IsClosed[inst✝⁴] s ∧ AbsConvex 𝕜 s) id

Tactic:
refine (nhds_basis_opens 0).to_hasBasis ?_
    fun s ⟨hs_nhds, _, _⟩ ↦ ⟨interior s,
      by simp [interior_subset, mem_interior_iff_mem_nhds.mpr hs_nhds]⟩

Goal state after:
𝕜 : 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 𝕜
⊢ ∀ (i : Set E), 0 ∈ i ∧ IsOpen[inst✝⁴] i → ∃ i', (i' ∈ 𝓝 0 ∧ IsClosed[inst✝⁴] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ i
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : NonemptyCompacts α
hL : IsPreconnected ↑L
⊢ IsPreconnected (Ioc (toCompactsOrderEmbedding K) (toCompactsOrderEmbedding L))

Tactic:
exact Compacts.isPreconnected_Ioc hL

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : NonemptyCompacts α
hL : IsPreconnected ↑L
⊢ IsPreconnected (Ioc K L)

Tactic:
rw [← isEmbedding_toCompacts.isPreconnected_image, ← coe_toCompactsOrderEmbedding,
    OrderEmbedding.image_Ioc _ (by simpa [← Set.Ioi_bot] using ordConnected_Ioi)]
  exact Compacts.isPreconnected_Ioc hL

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
by
  rw [dist_comm, dist_left_midpoint]

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

Goal state before:
pp: case neg.inl
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
cfcₙ_apply_of_not_continuousOn a hf,

Goal state after:
case neg.inl
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
⊢ ↑0 = 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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
h : IsUnit a
ha : 0 ≤ a
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
by
  have : IsStrictlyPositive a := by grind
  rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_mul_eq_div]

Goal state after:
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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : spectrum 𝕜 (a x) ⊆ s x✝
⊢ x ∈ t → spectrum 𝕜 (a x) ⊆ s x✝

Tactic:
hxt

Goal state after:
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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : spectrum 𝕜 (a x) ⊆ s x✝
hxt : x ∈ t
⊢ spectrum 𝕜 (a x) ⊆ s x✝
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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : spectrum 𝕜 (a x) ⊆ s x✝
⊢ x ∈ t → p (a x)

Tactic:
hxt

Goal state after:
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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : spectrum 𝕜 (a x) ⊆ s x✝
hxt : x ∈ t
⊢ p (a x)
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 > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) → ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
rintro ⟨r, hr, hr_le⟩

Goal state after:
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
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
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
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : spectrum ℝ≥0 (a x) ⊆ s x✝
⊢ x ∈ t → spectrum ℝ≥0 (a x) ⊆ s x✝

Tactic:
hxt

Goal state after:
X : Type u_1
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
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : spectrum ℝ≥0 (a x) ⊆ s x✝
hxt : x ∈ t
⊢ spectrum ℝ≥0 (a x) ⊆ s x✝
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
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
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : spectrum ℝ≥0 (a x) ⊆ s x✝
⊢ x ∈ t → 0 ≤ a x

Tactic:
hxt

Goal state after:
X : Type u_1
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
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : spectrum ℝ≥0 (a x) ⊆ s x✝
hxt : x ∈ t
⊢ 0 ≤ a x
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (∑ i, ∑ j, ‖replicateRow ι v i j‖ ^ 2) ^ (1 / 2) = ‖toLp 2 v‖

Tactic:
Fintype.sum_unique,

Goal state after:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (∑ j, ‖replicateRow ι v default j‖ ^ 2) ^ (1 / 2) = ‖toLp 2 v‖
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
this : ∀ (n : ℕ), ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖
⊢ False

Tactic:
choose x hx using this

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
x : ℕ → A₁
hx : ∀ (n : ℕ), 0 ≤ x n ∧ ‖x n‖ = 1 ∧ 2 ^ (2 * n) < ‖f (x n)‖
⊢ False