mathlib-initiative/mathlib-tactics huggingface dataset:
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
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
⊢ IsUnit (1 - z • a)

Tactic:
by_cases hz : z = 0
  · simp only [hz, isUnit_one, sub_zero, zero_smul]
  · let u := Units.mk0 z hz
    suffices hu : IsUnit (u⁻¹ • (1 : A) - a) by
      rwa [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv u] at hu
    rw [Units.smul_def, ← Algebra.algebraMap_eq_smul_one, ← mem_resolventSet_iff]
    refine mem_resolventSet_of_spectralRadius_lt ?_
    rwa [Units.val_inv_eq_inv_val, nnnorm_inv,
      coe_inv (nnnorm_ne_zero_iff.mpr (Units.val_mk0 hz ▸ hz : (u : 𝕜) ≠ 0)), lt_inv_iff_lt_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ CompactSpace (Closeds α) ↔ CompactSpace α

Tactic:
refine ⟨fun _ => compactSpace_of_finite_subfamily_closed fun {ι} F hF₁ hF₂ => ?_,
    fun _ => inferInstance⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
⊢ ∃ u, ⋂ i ∈ u, F i = ∅
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
n : ℕ
f : Fin n → α
ht₁ : (range f).Nonempty
ht₂ : (range f).Finite
hts : range f ⊆ s
⊢ range f ∈ ⋃ n, range '' univ.pi fun x ↦ s

Tactic:
rw [range_subset_iff] at hts

Goal state after:
case inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
n : ℕ
f : Fin n → α
ht₁ : (range f).Nonempty
ht₂ : (range f).Finite
hts : ∀ (y : Fin n), f y ∈ s
⊢ range f ∈ ⋃ n, range '' univ.pi fun x ↦ s
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
⊢ QuasispectrumRestricts (a * b) ⇑ContinuousMap.realToNNReal

Tactic:
rw [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at hb

Goal state after:
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 : IsSelfAdjoint b ∧ QuasispectrumRestricts b ⇑ContinuousMap.realToNNReal
h : Commute a b
⊢ QuasispectrumRestricts (a * b) ⇑ContinuousMap.realToNNReal
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
hw : w.Finite
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
wlog huw : u ⊆ w generalizing w

Goal state after:
case inr
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
hw : w.Finite
this :
  ∀ (w : Set (Set α)),
    ↑K ⊆ ⋃₀ w →
      w ⊆ B →
        ⋃₀ w ⊆ V →
          (∀ W ∈ w, (↑K ∩ W).Nonempty) →
            w.Finite →
              u ⊆ w →
                ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
                  K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
huw : ¬u ⊆ w
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
hw : w.Finite
huw : u ⊆ w
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
⊢ √(spectralRadius ℂ (a⋆ * a)).toReal = ‖a‖

Tactic:
simp [toReal_spectralRadius_star_mul_self_eq_norm_sq]

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

Goal state before:
pp: F : Type u_1
A : Type u_2
inst✝¹ : CStarAlgebra A
inst✝ : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
⊢ φ a⋆ = (φ a)⋆

Tactic:
suffices hsa : ∀ s : selfAdjoint A, (φ s)⋆ = φ s by
      rw [← realPart_add_I_smul_imaginaryPart a]
      simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq]

Goal state after:
F : Type u_1
A : Type u_2
inst✝¹ : CStarAlgebra A
inst✝ : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
⊢ ∀ (s : ↥(selfAdjoint A)), (φ ↑s)⋆ = φ ↑s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
⊢ RegularSpace (Compacts α)

Tactic:
regularSpace_generateFrom induced_generateFrom_eq,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
⊢ ∀
    t ∈
      preimage SetLike.coe ''
        (powerset '' {U | IsOpen[inst✝³] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝³] U}),
    ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case e'_5
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)) = ↑(expUnitary (2 • ℑ (z • star b)))

pp: case e'_6
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 (star z • a) * NormedSpace.exp (z • star (-a)) = ↑(expUnitary (2 • ℑ (star z • a)))

Tactic:
all_goals
    simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_smul I I, sub_eq_add_neg]
    grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed[WeakBilin.instTopologicalSpace B.flip] (⋂ x ∈ s, ⇑(B x) ⁻¹' Metric.closedBall 0 1)

Tactic:
exact isClosed_biInter
    fun _ _ ↦ Metric.isClosed_closedBall.preimage (WeakBilin.eval_continuous B.flip _)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f : α →ᵇ β
hf : ClusterPt f (𝓟 (range toBCF))
⊢ f ∈ range toBCF

Tactic:
rw [clusterPt_principal_iff] at hf

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range toBCF).Nonempty
⊢ f ∈ range toBCF
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ 0 ∈ B.polar Set.univ

Tactic:
by simp only [zero_mem_polar]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : Module ℝ E := restrictScalars ℝ 𝕜 E
this : IsScalarTower ℝ 𝕜 E := IsScalarTower.restrictScalars ℝ 𝕜 E
fr : Dual ℝ ↥S := reLm ∘ₗ ↑ℝ f
g : Dual ℝ E
hg : ∀ (x : ↥S), g ↑x = fr x
hgp : ∀ (x : E), |g x| ≤ (Seminorm.restrictScalars ℝ p) x
x : ↥S
⊢ g.extendRCLike ↑x = f x

Tactic:
g.extendRCLike_apply,

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : Module ℝ E := restrictScalars ℝ 𝕜 E
this : IsScalarTower ℝ 𝕜 E := IsScalarTower.restrictScalars ℝ 𝕜 E
fr : Dual ℝ ↥S := reLm ∘ₗ ↑ℝ f
g : Dual ℝ E
hg : ∀ (x : ↥S), g ↑x = fr x
hgp : ∀ (x : E), |g x| ≤ (Seminorm.restrictScalars ℝ p) x
x : ↥S
⊢ ↑(g ↑x) - I * ↑(g (I • ↑x)) = f x
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
⊢ polar 𝕜 (ball 0 r) = polar 𝕜 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 r))

Tactic:
polar_closure

Goal state after:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
⊢ polar 𝕜 (ball 0 r) = polar 𝕜 (ball 0 r)
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)
⊢ Continuous[inst✝³, _] ⇑p

Tactic:
have h₂ : (⋃ n : ℕ, p.closedBall (0 : E) n) = univ :=
      eq_univ_of_forall fun x ↦ mem_iUnion.mpr (exists_nat_ge <| p (x - 0))

Goal state after:
α : 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
⊢ Continuous[inst✝³, _] ⇑p
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx n c x
c : CU P
⊢ 0 ≤ approx (n + 1) c x

Tactic:
simp only [approx, midpoint_eq_smul_add]

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx n c x
c : CU P
⊢ 0 ≤ ⅟2 • (approx n c.left x + approx n c.right x)
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a ≤ a'
hr : r ≤ 1
⊢ (lineMap a b) r ≤ (lineMap a' b) r

Tactic:
simp only [lineMap_apply_module]

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a ≤ a'
hr : r ≤ 1
⊢ (1 - r) • a + r • b ≤ (1 - r) • a' + r • b
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a < a'
hr : r < 1
⊢ (lineMap a b) r < (lineMap a' b) r

Tactic:
simp only [lineMap_apply_module]

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a < a'
hr : r < 1
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b b' : E
r : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ (lineMap a b) r ≤ (lineMap a b') r

Tactic:
simp only [lineMap_apply_module]

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b b' : E
r : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ (1 - r) • a + r • b ≤ (1 - r) • a + r • b'
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b b' : E
r : k
hb : b < b'
hr : 0 < r
⊢ (lineMap a b) r < (lineMap a b') r

Tactic:
simp only [lineMap_apply_module]

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b b' : E
r : k
hb : b < b'
hr : 0 < r
⊢ (1 - r) • a + r • b < (1 - r) • a + r • b'
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Ring k
inst✝⁷ : PartialOrder k
inst✝⁶ : IsOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
a b : E
r r' : k
inst✝ : PosSMulReflectLT k E
h : r < r'
⊢ (lineMap a b) r < (lineMap a b) r' ↔ a < b

Tactic:
simp only [lineMap_apply_module]

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁸ : Ring k
inst✝⁷ : PartialOrder k
inst✝⁶ : IsOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
a b : E
r r' : k
inst✝ : PosSMulReflectLT k E
h : r < r'
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Ring k
inst✝⁷ : PartialOrder k
inst✝⁶ : IsOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
a b : E
r r' : k
inst✝ : PosSMulReflectLT k E
h : r < r'
⊢ (1 - r - (1 - r')) • a < (r' - r) • b ↔ a < b

Tactic:
sub_sub_sub_cancel_left,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁸ : Ring k
inst✝⁷ : PartialOrder k
inst✝⁶ : IsOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
a b : E
r r' : k
inst✝ : PosSMulReflectLT k E
h : r < r'
⊢ (r' - r) • a < (r' - r) • b ↔ a < b
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
a b : E
r r' : k
h : r < r'
⊢ (lineMap a b) r ≤ (lineMap a b) r' ↔ a ≤ b

Tactic:
simp only [lineMap_apply_module]

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b ≤ (1 - r') • a + r' • b ↔ a ≤ b
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r - (1 - r')) • a ≤ (r' - r) • b ↔ a ≤ b

Tactic:
sub_sub_sub_cancel_left,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
a b : E
r r' : k
h : r < r'
⊢ (r' - r) • a ≤ (r' - r) • b ↔ a ≤ b
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_2
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
⊢ x ∈ s

Tactic:
· obtain ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
    by_contra hx'
    exact notMem_idealOfSet.mpr ⟨x, hx', hfx⟩ (h hf)

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

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  let __Subalgebra := (gelfandTransform ℂ A).range;
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ x✝¹ ≠ x✝ → ∃ f ∈ (fun f ↦ ⇑f) '' ↑rng.toSubalgebra, f x✝¹ ≠ f x✝

Tactic:
contrapose!

Goal state after:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  let __Subalgebra := (gelfandTransform ℂ A).range;
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ (∀ f ∈ (fun f ↦ ⇑f) '' ↑rng.toSubalgebra, f x✝¹ = f x✝) → x✝¹ = x✝
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✝ : T2Space A
a : A
⊢ a⁺ = (-a)⁻

Tactic:
← sub_eq_zero,

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✝ : T2Space A
a : A
⊢ a⁺ - (-a)⁻ = 0
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
f g : α →ᵤ[𝔖] β
C : ℝ≥0∞
⊢ edist f g ≤ C ↔ ∀ x ∈ ⋃₀ 𝔖, edist ((toFun 𝔖) f x) ((toFun 𝔖) g x) ≤ C

Tactic:
by
  simp_rw [edist_def, iSup₂_le_iff]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ CFC.sqrt ↑a = ↑(CFC.sqrt a)

Tactic:
by
  by_cases ha : 0 ≤ a <;> have ha' := by rwa [← Unitization.inr_nonneg_iff] at ha
  · rw [CFC.sqrt_eq_iff .., ← inr_mul, CFC.sqrt_mul_sqrt_self a]
  · rw [CFC.sqrt, CFC.sqrt, cfcₙ_apply_of_not_predicate _ ha,
      cfcₙ_apply_of_not_predicate _ ha', inr_zero]

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

Goal state before:
pp: 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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
replace hf : ContinuousOn (fun x ↦ f x.toNNReal : ℝ → ℝ) (NNReal.toReal '' s) := by
    apply hf.ofReal_map_toNNReal
    rw [Set.mapsTo_image_iff]
    intro x hx
    simpa

Goal state after:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
⊢ ContinuousOn (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 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✝ : CompleteSpace A
s : Set ℝ≥0
⊢ ContinuousOn (fun fa ↦ cfc ((toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)})

Tactic:
by
  refine continuousOn_of_locally_continuousOn fun (f, a) ⟨hf, ha, has⟩ ↦ ?_
  have hs := ContinuousFunctionalCalculus.isCompact_spectrum (R := ℝ≥0) a
  obtain ⟨k, ⟨hka, hk⟩, hks⟩ := hs.nhdsSet_basis_isCompact.mem_iff.mp has
  have := (upperHemicontinuous_spectrum_nnreal A).isOpen k
  refine ⟨Set.univ ×ˢ {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)}, isOpen_univ.prod this, by simpa, ?_⟩
  conv in cfc _ => equals cfc (toFun {k} (ofFun {k} (toFun {t | IsCompact t ∧ t ⊆ s} fa.1))) => rfl
  refine continuousOn_cfc_nnreal_setProd hk |>.comp'
    (uniformContinuous_ofFun_toFun_of_mem _ {t | IsCompact t ∧ t ⊆ s} _ ⟨hk, hks⟩ |>.prodMap
      uniformContinuous_id).continuous.continuousOn ?_
  intro (f, a) ⟨⟨hf, ha⟩, ⟨_, ha'⟩⟩
  exact ⟨hf.mono hks, ha.1, subset_of_mem_nhdsSet ha'⟩

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ ‖x‖ = √‖x * star x‖

Tactic:
by
    rw [← sq_eq_sq₀ (norm_nonneg _) (by positivity)]
    simpa [sq] using Eq.symm <| CStarRing.norm_self_mul_star

Goal state after: