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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
⊢ eVariationOn f (s ∩ Set.Icc a b) = ENNReal.ofReal (f b - f a)

Tactic:
have hle : eVariationOn f (s ∩ Icc a b) ≤ .ofReal (f b - f a) := by
      apply iSup_le _
      rintro ⟨n, ⟨u, hu, us⟩⟩
      calc
        _ = ∑ i ∈ range n, .ofReal (f (u (i + 1)) - f (u i)) := by
          refine sum_congr rfl fun i hi => ?_
          simp only [Finset.mem_range] at hi
          rw [edist_dist, Real.dist_eq, abs_of_nonneg]
          exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
        _ = .ofReal (∑ i ∈ range n, (f (u (i + 1)) - f (u i))) := by
          rw [ofReal_sum_of_nonneg]
          exact fun i _ ↦ sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
        _ = .ofReal (f (u n) - f (u 0)) := by rw [sum_range_sub (f <| u ·)]
        _ ≤ _ :=
          ofReal_le_ofReal (sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1))
    have h : BoundedVariationOn f (s ∩ Icc a b) := (hle.trans_lt ofReal_lt_top).ne
    apply eq_of_le_of_ge hle (ofReal_le_of_le_toReal _)
    grw [← h.dist_le (x := a) (y := b)] <;> grind [Real.dist_eq]

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ (n + 1)) ∈ R[(toContinuousMapOnAlgHom s) X]

Tactic:
· rw [pow_succ, ← mul_assoc, map_mul]
    exact mul_mem hn (Algebra.subset_adjoin <| Set.mem_singleton _)

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

Goal state before:
pp: case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (Subalgebra.comap W (polynomialFunctions I)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
polynomialFunctions.comap_compRightAlgHom_iccHomeoI

Goal state after:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure

Tactic:
by
  rw [polynomialFunctions_closure_eq_top _ _]
  simp

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
⊢ AK.SeparatesPoints

Tactic:
intro x y hxy

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑AK, f x ≠ f y
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_1
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f ↦ ⇑f) f x₁ ≠ (fun f ↦ ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x ↦ ‖F x‖ ^ 2, continuous_toFun := ⋯ } ∈
    restrictScalars ℝ A.toSubalgebra

Tactic:
convert! (A.restrictScalars ℝ).mul_mem hFA (star_mem hFA : star F ∈ A)

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f ↦ ⇑f) f x₁ ≠ (fun f ↦ ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x ↦ ‖F x‖ ^ 2, continuous_toFun := ⋯ } = F * star F
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst✝⁴] ⇑ξ
ξ' : C(↑s', ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })
⊢ Continuous[_, inst✝⁴] ⇑ξ' ∧ ξ' (ContinuousMapZero.id s') = ξ (ContinuousMapZero.id s)

Tactic:
refine ⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩

Goal state after:
case refine_1
X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst✝⁴] ⇑ξ
ξ' : C(↑s', ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })
⊢ Continuous ⇑↑(nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }).toNonUnitalAlgHom

case refine_2
X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst✝⁴] ⇑ξ
ξ' : C(↑s', ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })
⊢ ξ' (ContinuousMapZero.id s') = ξ (ContinuousMapZero.id s)
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ ContinuousAdd (WeakBilin B)

Tactic:
by
  refine ⟨continuous_induced_rng.2 ?_⟩
  refine
    cast (congr_arg _ ?_)
      (((coeFn_continuous B).comp continuous_fst).add ((coeFn_continuous B).comp continuous_snd))
  ext
  simp only [Function.comp_apply, Pi.add_apply, map_add, LinearMap.add_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpace B, instTopologicalSpace B] fun a ↦ -a

Tactic:
by
    refine continuous_induced_rng.2 (continuous_pi_iff.mpr fun y => ?_)
    refine cast (congr_arg _ ?_) (eval_continuous B (-y))
    ext x
    simp only [map_neg, Function.comp_apply, LinearMap.neg_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : φ 1 * (1 - φ 1) = 0
h₂ : φ 1 = 0
this : ∀ (a : A), φ (a * 1) = 0
⊢ ∀ (x : A), ↑φ x = 0 x

Tactic:
by simpa only [mul_one] using! this

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf₁ : f ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
hf₂ : f ∈ RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)
⊢ f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
adjoin_id_eq_span_one_add,

Goal state after:
case mp
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf₂ : f ∈ RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)
hf₁ : f ∈ ↑(𝕜 ∙ 1) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
⊢ f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ ↑t, {x | (x, y) ∈ Prod.swap ⁻¹' U}
⊢ ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s) ∈ hausdorffEntourage U

Tactic:
refine ⟨fun _ h => h.2, fun x hx => ?_⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ ↑t, {x | (x, y) ∈ Prod.swap ⁻¹' U}
x : α
hx : x ∈ ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2
⊢ x ∈ U.image ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformly F f l
hF : ∀ (n : ι), LowerHemicontinuous (F n)
⊢ LowerHemicontinuousOn f univ

Tactic:
exact htendsto.tendstoUniformlyOn.lowerHemicontinuousOn (fun n ↦ (hF n).lowerHemicontinuousOn _)

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
⊢ Tendsto (fun x ↦ x⁻¹ • a) (cobounded 𝕜) (𝓝 0)

Tactic:
by simpa using (tendsto_inv₀_cobounded (α := 𝕜)).smul_const a

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : ProperSpace 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a₀ : A
⊢ ∀ᶠ (x : A) in 𝓝 a₀, spectrum 𝕜 x ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * ‖1‖)

Tactic:
filter_upwards [Metric.closedBall_mem_nhds a₀ zero_lt_one] with a ha

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : ProperSpace 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
⊢ spectrum 𝕜 a ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * ‖1‖)
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ DifferentiableAt 𝕜 (fun z ↦ (1 - z • a)⁻¹ʳ) z

Tactic:
have hu : IsUnit (1 - z • a) := by
    refine isUnit_one_sub_smul_of_lt_inv_radius (lt_of_le_of_lt (coe_mono ?_) hr)
    simpa only [norm_toNNReal, Real.toNNReal_coe] using
      Real.toNNReal_mono (mem_closedBall_zero_iff.mp z_mem)

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
hu : IsUnit (1 - z • a)
⊢ DifferentiableAt 𝕜 (fun z ↦ (1 - z • a)⁻¹ʳ) z
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
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
hx' : x ∈ σ 𝕜 a
⊢ ‖↑f ⟨x, hx⟩‖ ≤ ‖(↑f).comp ι‖

Tactic:
· exact (f : C(σₙ 𝕜 a, 𝕜)).comp ι |>.norm_coe_le_norm ⟨x, hx'⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace (NonemptyCompacts α)
x : α
U : Set α
x✝ : x ∈ U ∧ IsOpen[inst✝] U
hx : x ∈ U
hU : IsOpen[inst✝] U
⊢ ∃ i', (i' ∈ 𝓝 x ∧ IsPreconnected i') ∧ id i' ⊆ U

Tactic:
obtain ⟨V, ⟨hV₁, hV₂⟩, hxV, hKV⟩ :=
    IsTopologicalBasis.isOpen_isPreconnected.exists_subset_of_mem_open
      (show {x} ∈ {K : NonemptyCompacts α | ↑K ⊆ U} by simpa)
      (isOpen_subsets_of_isOpen hU)

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace (NonemptyCompacts α)
x : α
U : Set α
x✝ : x ∈ U ∧ IsOpen[inst✝] U
hx : x ∈ U
hU : IsOpen[inst✝] U
V : Set (NonemptyCompacts α)
hV₁ : IsOpen V
hV₂ : IsPreconnected V
hxV : {x} ∈ V
hKV : V ⊆ {K | ↑K ⊆ U}
⊢ ∃ i', (i' ∈ 𝓝 x ∧ IsPreconnected i') ∧ id i' ⊆ U
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
p q : P
⊢ dist ((Equiv.pointReflection p) q) q = ‖2‖ * dist p q

Tactic:
simp [dist_eq_norm_vsub V, Equiv.pointReflection_vsub_right (G := V), ← Nat.cast_smul_eq_nsmul 𝕜,
    norm_smul]

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
⊢ ‖a + b‖ = max ‖a‖ ‖b‖

Tactic:
by
  /- Since `a` and `b` are normal, commute, and commute with the `star` of the other,
  the C⋆-subalgebra generated by `a` and `b` is commutative, and the conclusion follows from the
  corresponding result for commutative C⋆-algebras. -/
  -- TODO: once #36418 is merged, it should be possible to remove the `let _`s below entirely.
  let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
  have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure
  have hcomm₁ := ha.commute_star_left hcomm
  have hcomm₂ := hb.commute_star_right hcomm
  have : IsMulCommutative (adjoin ℂ {a, b}) :=
    isMulCommutative_adjoin ℂ (by grind) (by grind [commute_star_comm])
  let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm
  let _ : NonUnitalCommCStarAlgebra S := { }
  refine CommCStarAlgebra.norm_add_eq_max (A := S) (a := ⟨a, ?_⟩) (b := ⟨b, ?_⟩) (by ext; simpa)
  all_goals apply le_topologicalClosure; aesop

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
⊢ 0⁻ = 0

Tactic:
by simp [negPart_def]

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

Goal state before:
pp: 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
φ : A × B →⋆ₙₐ[S] A := NonUnitalStarAlgHom.fst S A B
⊢ ContinuousOn f (quasispectrum R (a, b))

Tactic:
Prod.quasispectrum_eq

Goal state after:
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
φ : A × B →⋆ₙₐ[S] A := NonUnitalStarAlgHom.fst S A B
⊢ ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: 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
φ : A × B →⋆ₙₐ[S] B := NonUnitalStarAlgHom.snd S A B
⊢ ContinuousOn f (quasispectrum R (a, b))

Tactic:
Prod.quasispectrum_eq

Goal state after:
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
φ : A × B →⋆ₙₐ[S] B := NonUnitalStarAlgHom.snd S A B
⊢ ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
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' := ⋯ }
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)
⊢ b = cfcₙ id b + cfcₙ 0 (-c)

Tactic:
by simp [cfcₙ_id ℝ b]

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

Goal state before:
pp: case neg.inr
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)
ha : ¬p a
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
rw [cfcₙ_apply_of_not_predicate a ha, inr_zero,
        cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)]

Goal state after: