mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, ⟨u, ⋯⟩).1
⊢ edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x))) =
    edist (f (↑(n, ⟨fun i ↦ φ (u (n - i)), ⋯⟩).2 (x + 1))) (f (↑(n, ⟨fun i ↦ φ (u (n - i)), ⋯⟩).2 x))

Tactic:
dsimp only [Subtype.coe_mk, Function.comp_apply]

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, ⟨u, ⋯⟩).1
⊢ edist (f (φ (u (n - 1 - x + 1)))) (f (φ (u (n - 1 - x)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
⊢ eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))

Tactic:
rcases le_total x y with (h | h)

Goal state after:
case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
⊢ eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))

case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Ioi a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Ici a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Ioi a)) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Ici a))

Tactic:
exact eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt h h'

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

Goal state before:
pp: case mp.refine_2.convert_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ (b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹) ∈ I

Tactic:
rw [mul_comm (b - a)⁻¹, ← neg_mul, ← add_mul, ← sub_eq_add_neg]
        have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)
        have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1
        have w₃ : (x : ℝ) - a ≤ b - a := sub_le_sub_right x.2.2 a
        fconstructor
        · exact mul_nonneg w₂ (le_of_lt w₁)
        · rw [← div_eq_mul_inv, div_le_one (sub_pos.mpr h)]
          exact w₃

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

Goal state before:
pp: case mpr
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ polynomialFunctions (Set.Icc a b) →
    f ∈ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I)

Tactic:
rintro ⟨p, ⟨-, rfl⟩⟩

Goal state after:
case mpr
a b : ℝ
h : a < b
p : ℝ[X]
⊢ ↑(toContinuousMapOnAlgHom (Set.Icc a b)) p ∈
    Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
⊢ cfcₙ f a ≤ cfcₙ g a

Tactic:
by_cases ha : p a
  · rw [cfcₙ_apply f a, cfcₙ_apply g a]
    exact cfcₙHom_mono ha fun x ↦ h x.1 x.2
  · simp only [cfcₙ_apply_of_not_predicate _ ha, le_rfl]

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

Goal state before:
pp: 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
⊢ IsClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)

Tactic:
by
  let f : C(spectrum R a, σₙ R a) :=
    ⟨_, continuous_inclusion <| spectrum_subset_quasispectrum R a⟩
  refine (cfcHom_isClosedEmbedding ha).comp <|
    (IsUniformInducing.isUniformEmbedding ⟨?_⟩).isClosedEmbedding
  have := uniformSpace_eq_inf_precomp_of_cover (β := R) f (0 : C(Unit, σₙ R a))
    (map_continuous f).isProperMap (map_continuous 0).isProperMap <| by
      simp only [← Subtype.val_injective.image_injective.eq_iff, f, ContinuousMap.coe_mk,
        ContinuousMap.coe_zero, range_zero, image_union, image_singleton,
        quasispectrum.coe_zero, ← range_comp, val_comp_inclusion, image_univ, Subtype.range_coe,
        quasispectrum_eq_spectrum_union_zero]
  simp_rw +instances [← isUniformEmbedding_toContinuousMap.comap_uniformity, this,
    @inf_uniformity _ (.comap _ _) (.comap _ _), uniformity_comap, Filter.comap_inf,
    Filter.comap_comap]
  refine .symm <| inf_eq_left.mpr <| le_top.trans <| eq_top_iff.mp ?_
  have : ∀ U ∈ 𝓤 (C(Unit, R)), (0, 0) ∈ U := fun U hU ↦ refl_mem_uniformity hU
  convert! Filter.comap_const_of_mem this with ⟨u, v⟩ <;>
  ext ⟨x, rfl⟩ <;> [exact map_zero u; exact map_zero v]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : TopologicalSpace A
inst✝⁵ : T2Space A
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst✝⁶] ⇑φ
hψ : Continuous[_, inst✝⁶] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
f : ContinuousMapZero (↑s) 𝕜
hf : f ∈ ↑(adjoin 𝕜 {ContinuousMapZero.id s})
⊢ {ContinuousMapZero.id s} ⊆ ↑(NonUnitalStarAlgHom.equalizer φ ψ)

Tactic:
Set.singleton_subset_iff

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : TopologicalSpace A
inst✝⁵ : T2Space A
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst✝⁶] ⇑φ
hψ : Continuous[_, inst✝⁶] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
f : ContinuousMapZero (↑s) 𝕜
hf : f ∈ ↑(adjoin 𝕜 {ContinuousMapZero.id s})
⊢ ContinuousMapZero.id s ∈ ↑(NonUnitalStarAlgHom.equalizer φ ψ)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁹ : CommSemiring R
inst✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst✝¹⁹, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
⊢ φ (cfcₙ f a) = cfcₙ f (φ a)

Tactic:
let ψ : A →⋆ₙₐ[R] B := (φ : A →⋆ₙₐ[S] B).restrictScalars R

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁹ : CommSemiring R
inst✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst✝¹⁹, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
⊢ φ (cfcₙ f a) = cfcₙ f (φ a)
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
⊢ Continuous[inst✝, _] (↑(toWeakSpace 𝕜 E)).toFun

Tactic:
by
    apply WeakBilin.continuous_of_continuous_eval
    exact ContinuousLinearMap.continuous

Goal state after:
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
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : IsCompact (quasispectrum ℝ a)
⊢ IsCompact (quasispectrum ℝ≥0 a)

Tactic:
← quasispectrum.preimage_algebraMap ℝ

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedRing A
inst✝¹¹ : NormedAlgebra 𝕜 A
inst✝¹⁰ : CompleteSpace A
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : IsCompact (quasispectrum ℝ a)
⊢ IsCompact (⇑(algebraMap ℝ≥0 ℝ) ⁻¹' quasispectrum ℝ a)
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
⊢ ∀ᶠ (z : 𝕜) in cobounded 𝕜, IsUnit (resolvent a z)

Tactic:
rw [atTop_basis_Ioi.cobounded_of_norm.eventually_iff]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ ∃ i, True ∧ ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Set.Ioi i → IsUnit (resolvent a x)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case inl
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : U ∈ {U | IsOpen[inst✝.toTopologicalSpace] U}
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
⊢ 𝒫 U ∈ 𝓝 s

Tactic:
filter_upwards [UniformSpace.ball_mem_nhds _ (Filter.mem_lift' hV₁)]
      with t ⟨_, ht⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : U ∈ {U | IsOpen[inst✝.toTopologicalSpace] U}
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
t : Set α
left✝ : (s, t).1 ⊆ V.preimage (s, t).2
ht : (s, t).2 ⊆ V.image (s, t).1
⊢ t ∈ 𝒫 U
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
a : A
ha : p a
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ (cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

Tactic:
← SetLike.mem_coe

Goal state after:
𝕜 : 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
a : A
ha : p a
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ (cfcₙAux ⋯ a ha) f ∈ ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
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)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
⊢ liminf (fun i ↦ 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop = p.radius

Tactic:
simp only [p, p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]

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)
h : ↑r ≤ p.radius
⊢ liminf (fun i ↦ 1 / ↑‖a ^ i‖.toNNReal ^ (1 / ↑i)) atTop = liminf (fun n ↦ 1 / ↑(‖a ^ n‖.toNNReal ^ (1 / ↑n))) atTop
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * (NormedSpace.exp (-(star z • b)) * x * NormedSpace.exp (star z • a)) *
      NormedSpace.exp (z • star (-a)) =
    ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))

Tactic:
simp_rw [← mul_assoc, mul_assoc (_ * _ * x)]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * NormedSpace.exp (-(star z • b)) * x *
      (NormedSpace.exp (star z • a) * NormedSpace.exp (z • star (-a))) =
    ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
a b : A
| deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 = a ^ 2 + 2 • (a * b) + b ^ 2

Tactic:
enter [1, 1, y, 1, x, 1]; rw [← mul_one (exp (x • a))]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
a b : A
y x : ℝ
| NormedSpace.exp (x • a) * 1
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace (NonemptyCompacts α) ↔ PreconnectedSpace α

Tactic:
refine ⟨fun h => ?_, fun h => inferInstance⟩
  rw [preconnectedSpace_iff_clopen] at h ⊢
  intro s hs
  apply h _ ⟨isClosed_subsets_of_isClosed hs.isClosed, isOpen_subsets_of_isOpen hs.isOpen⟩ |>.imp
  · simp only [Set.eq_empty_iff_forall_notMem]
    exact fun h x hx => h {x} (Set.singleton_subset_iff.mpr hx)
  · simp only [Set.eq_univ_iff_forall]
    exact fun h x => Set.singleton_subset_iff.mp (h {x})

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
⊢ ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simp_all [nnnorm_add_eq_max this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

Goal state after:
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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺ - x⁻) a = a

Tactic:
conv_rhs => rw [← cfcₙ_id ℝ a]

Goal state after:
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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺ - x⁻) a = cfcₙ id a
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
a : A
ha : 0 ≤ a
⊢ a⁺ = a

Tactic:
conv_rhs => rw [← cfcₙ_id ℝ a]

Goal state after:
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
a : A
ha : 0 ≤ a
⊢ a⁺ = cfcₙ id a
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
f g : α →ᵤ β
C : ℝ
hC : 0 ≤ C
⊢ dist f g ≤ C ↔ ∀ (x : α), dist (toFun f x) (toFun g x) ≤ C

Tactic:
simp_rw [dist_edist, ← ENNReal.le_ofReal_iff_toReal_le (edist_ne_top _ _) hC, edist_le]

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

Goal state before:
pp: case e'_5
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' := ⋯ }
f : C(↑s, ℝ)₀ := { toFun := fun x ↦ (↑x)⁺, continuous_toFun := ⋯, map_zero' := ⋯ }
key :
  cfcₙ
      (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id has, continuous_toFun := ⋯, map_zero' := ⋯ })
        fun x ↦ x⁺)
      a =
    cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hbs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        b +
      cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hcs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        (-c)
x : { x // x ∈ σₙ ℝ b }
⊢ 0 ≤ ↑x

Tactic:
exact quasispectrum_nonneg_of_nonneg b hb x.val x.property

Goal state after:
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✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
x : A
⊢ ↑(ℜ x) + I • ((↑(ℑ x))⁺ - (↑(ℑ x))⁻) = x

Tactic:
CFC.posPart_sub_negPart _ (ℑ x).2,

Goal state after:
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✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
x : A
⊢ ↑(ℜ x) + I • ↑(ℑ x) = x