mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

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

Tactic:
rintro ⟨hf₁, hf₂⟩
    rw [SetLike.mem_coe] at hf₂ ⊢
    simp_rw [adjoin_id_eq_span_one_add, Set.mem_add, SetLike.mem_coe, mem_span_singleton] at hf₁
    obtain ⟨-, ⟨r, rfl⟩, f, hf, rfl⟩ := hf₁
    have := nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf
    simp only [SetLike.mem_coe, RingHom.mem_ker, evalStarAlgHom_apply] at hf₂ this
    rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂
    rwa [hf₂, zero_smul, zero_add]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ (∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x

pp: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
case h₁ =>
    intro s t hst
    gcongr

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ (∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuous f
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ UpperHemicontinuous fun x ↦ i ⁻¹' f x

Tactic:
by
  rw [upperHemicontinuous_iff] at hf ⊢
  exact fun x ↦ (hf x).isInducing_comp hi h_cl

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

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ Metric.eball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y • a‖₊ < Real.toNNReal 1

Tactic:
Real.toNNReal_one,

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ Metric.eball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y • a‖₊ < 1
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
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
x : ↥S
hx : IsUnit x
⊢ Ring.inverse ((val S) x) = (val S) ↑hx.unit⁻¹

Tactic:
rw [← (hx.map (val S)).unit_spec, Ring.inverse_unit (hx.map (val S)).unit, val]

Goal state after:
𝕜 : 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
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
x : ↥S
hx : IsUnit x
⊢ ↑⋯.unit⁻¹ =
    { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } ↑hx.unit⁻¹
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
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ Function.Injective ⇑ψ

Tactic:
have h₁ : Function.Injective ⇑(codRestrict (cfcₙAux hp₁ a ha) _
          (cfcₙAux_mem_range_inr hp₁ a ha)) :=
        (Set.injective_codRestrict _).mpr (cfcₙAux_injective hp₁ a ha)

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
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
h₁ : Function.Injective ⇑(codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
⊢ Function.Injective ⇑ψ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
⊢ 0 ≤ a * b

Tactic:
by
  rw [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts]
  refine ⟨ha.isSelfAdjoint.commute_iff hb.isSelfAdjoint |>.mp h, ?_⟩
  rw [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at hb
  obtain ⟨x, hx₁, hx₂, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts hb.1 hb.2
  have hx := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts.mpr ⟨hx₁, hx₂⟩
  rw [← mul_assoc, quasispectrumRestricts_iff, quasispectrum.mul_comm,
    ← quasispectrumRestricts_iff, ← mul_assoc]
  exact QuasispectrumRestricts.nnreal_of_nonneg <| conjugate_nonneg_of_nonneg ha hx

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
⊢ ‖0‖₊ < c

pp: case refine_2
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : 0 ≤ a
⊢ ‖(cfcₙHom ha) { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }‖₊ < c

Tactic:
· simpa using (h 0 (quasispectrum.zero_mem ℝ≥0 _)).pos

Goal state after:
case refine_2
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : 0 ≤ a
⊢ ‖(cfcₙHom ha) { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }‖₊ < c
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ s = ∅ → (absConvexHull 𝕜) s = ∅

Tactic:
rintro rfl
    exact absConvexHull_empty

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommMonoid E
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : PartialOrder 𝕜
⊢ ∃ a, ∃ (_ : 0 ∈ a ∧ IsOpen[inst✝⁴] a ∧ AbsConvex 𝕜 a), True

Tactic:
exact ⟨Set.univ, ⟨mem_univ 0, isOpen_univ, balanced_univ, convex_univ⟩, trivial⟩

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

Goal state before:
pp: case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
S : Subspace ℝ E
f : Dual ℝ ↥S
p : Seminorm ℝ E
hp : ∀ (x : ↥S), f x ≤ p ↑x
x✝¹ : ℝ
hc : 0 < x✝¹
x✝ : E
⊢ p (x✝¹ • x✝) = x✝¹ * p x✝

pp: case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
S : Subspace ℝ E
f : Dual ℝ ↥S
p : Seminorm ℝ E
hp : ∀ (x : ↥S), f x ≤ p ↑x
⊢ ∀ (x y : E), p (x + y) ≤ p x + p y

Tactic:
· simp [map_smul_eq_mul, abs_of_nonneg hc.le]

Goal state after:
case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
S : Subspace ℝ E
f : Dual ℝ ↥S
p : Seminorm ℝ E
hp : ∀ (x : ↥S), f x ≤ p ↑x
⊢ ∀ (x y : E), p (x + y) ≤ p x + p y
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ AbsConvex 𝕜 (B.polar s)

Tactic:
by
  rw [polar_eq_biInter_preimage]
  exact AbsConvex.iInter₂ fun i hi =>
    ⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F →ₑ[(RingHom.id 𝕜)] 𝕜))),
      (convex_RCLike_iff_convex_real.mpr (convex_closedBall 0 1)).linear_preimage _⟩

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

Goal state before:
pp: α : Type u_1
ι : 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✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
h₁ : ∀ (n : ℕ), IsClosed[inst✝³] (p.closedBall 0 ↑n)
h₂ : ⋃ n, p.closedBall 0 ↑n = univ
n : ℕ
x : E
hxn : {y | p y ≤ ↑n} ∈ map (fun x_1 ↦ x + x_1) (𝓝 0)
hxn' : p x ≤ ↑n
y : E
hy : y ∈ (fun x_1 ↦ x + x_1) ⁻¹' {y | p y ≤ ↑n}
⊢ p y = p (x + y - x)

Tactic:
rw [add_sub_cancel_left]

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

Goal state before:
pp: α : Type u_1
ι : 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✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
⊢ ∀ (p : Seminorm 𝕜₁ E), LowerSemicontinuous ⇑p → Continuous[inst✝³, _] ⇑p

Tactic:
by
    -- Let `p` be a lower-semicontinuous seminorm on `E`.
    intro p hp
    -- Consider the family of all `p`-closed-balls with integer radius.
    -- By lower semicontinuity, each of these closed balls is indeed closed...
    have h₁ : ∀ n : ℕ, IsClosed (p.closedBall (0 : E) n) := fun n ↦ by
      simpa [p.closedBall_zero_eq] using! hp.isClosed_preimage n
    -- ... and clearly they cover the whole space.
    have h₂ : (⋃ n : ℕ, p.closedBall (0 : E) n) = univ :=
      eq_univ_of_forall fun x ↦ mem_iUnion.mpr (exists_nat_ge <| p (x - 0))
    -- Hence, one of them has nonempty interior. Let `n : ℕ` be its radius, and fix `x` an
    -- interior point.
    rcases nonempty_interior_of_iUnion_of_closed h₁ h₂ with ⟨n, ⟨x, hxn⟩⟩
    -- To show that `p` is continuous, we will show that the `p`-closed-ball of
    -- radius `2*n` is a neighborhood of zero.
    refine Seminorm.continuous' (r := n + n) ?_
    rw [p.closedBall_zero_eq] at hxn ⊢
    have hxn' : p x ≤ n := by convert! interior_subset hxn
    -- By definition, we have `p x' ≤ n` for `x'` sufficiently close to `x`.
    -- In other words, `p (x + y) ≤ n` for `y` sufficiently close to `0`.
    rw [mem_interior_iff_mem_nhds, ← map_add_left_nhds_zero] at hxn
    -- Hence, for `y` sufficiently close to `0`, we have
    -- `p y = p (x + y - x) ≤ p (x + y) + p x ≤ 2*n`
    filter_upwards [hxn] with y hy
    calc p y = p (x + y - x) := by rw [add_sub_cancel_left]
      _ ≤ p (x + y) + p x := map_sub_le_add _ _ _
      _ ≤ n + n := add_le_add hy hxn'

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:

Tactic:
approx n₂ c₂ x = 0 := approx_of_mem_C _ _ (h hx)
      _ ≤ approx n₁ c₁ x := approx_nonneg _ _ _

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
⊢ ∃ x, setOfIdeal I = {x}ᶜ

Tactic:
by
  have h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal :=
    (idealOfSet_ofIdeal_isClosed (inferInstance : IsClosed (I : Set C(X, 𝕜)))).symm ▸ hI
  obtain ⟨x, hx⟩ := Opens.isCoatom_iff.1 ((idealOfSet_isMaximal_iff 𝕜 (opensOfIdeal I)).1 h)
  exact ⟨x, congr_arg (fun (s : Opens X) => (s : Set X)) hx⟩

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:
let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
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
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
⊢ ∀ a_1 ∈ {a, b}, ∀ b_1 ∈ {a, b}, a_1 * star b_1 = star b_1 * a_1

Tactic:
by grind [commute_star_comm]

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ a ∈ S

Tactic:
apply le_topologicalClosure

Goal state after:
case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := ⋯
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S := ⋯
⊢ a ∈ adjoin ℂ {a, b}
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ b ∈ S

Tactic:
apply le_topologicalClosure

Goal state after:
case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := ⋯
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S := ⋯
⊢ b ∈ adjoin ℂ {a, b}
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ ∀ (x y : α →ᵤ β), edist x y = edist y x

Tactic:
simp [edist_def, edist_comm]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
⊢ ((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
      (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
    a

Tactic:
exact congr_arg Subtype.val <| continuousFunctionalCalculus_map_id a

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

Goal state before:
pp: 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
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont : ContinuousOn (fun x ↦ (ofFun {spectrum R a}) (f x)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
⊢ ContinuousOn (fun x ↦ cfc (f x) a) s

Tactic:
by
  rw [ContinuousOn] at h_cont ⊢
  simp only [ContinuousWithinAt, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Set.mem_singleton_iff,
    Function.comp_def, toFun_ofFun, forall_eq] at h_cont
  refine fun x hx ↦ continuousWithinAt_cfc_fun (h_cont x hx) ?_
  filter_upwards [self_mem_nhdsWithin] with x hx
  exact hf x hx

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

Goal state before:
pp: case add
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 : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f g : C(↑s, 𝕜)
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) f
hg : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) (f + g)

Tactic:
| add f g hf hg =>

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

Tactic:
sqrt_mul_sqrt_self a,

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
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
| ‖↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
⊢ b ∈ Set.Ici 0 → a ≤ b → cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b

Tactic:
(hb : 0 ≤ b)

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
⊢ a ≤ b → cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case add
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f g : C(↑s, 𝕜)₀
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) f
hg : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) (f + g)

Tactic:
| add f g hf hg =>

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
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y = y * ε ^ 2 * (y / (ε ^ 2 + y))

Tactic:
by simp [field]

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

Goal state before:
pp: F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst✝⁸ : NonUnitalCStarAlgebra A₁
inst✝⁷ : NonUnitalCStarAlgebra A₂
inst✝⁶ : PartialOrder A₁
inst✝⁵ : PartialOrder A₂
inst✝⁴ : StarOrderedRing A₁
inst✝³ : StarOrderedRing A₂
inst✝² : FunLike F A₁ A₂
inst✝¹ : NonUnitalAlgHomClass F ℂ A₁ A₂
inst✝ : StarHomClass F A₁ A₂
φ : F
k : ℕ
M : CStarMatrix (Fin k) (Fin k) A₁
hM : 0 ≤ M
⊢ 0 ≤ M.map ⇑φ

Tactic:
change 0 ≤ (mapₙₐ (φ : A₁ →⋆ₙₐ[ℂ] A₂)) M
    exact map_nonneg _ hM

Goal state after: