mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ ∃ x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
    s ∈ {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} ∧
      {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} ⊆ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
refine ⟨⟨⋃₀ u, f '' u⟩, ⟨isOpen_sUnion hu₂, hu₁.image _, by grind⟩, by grind,
      fun t ⟨ht₁, ht₂⟩ => ⟨ht₁, fun U hU => ?_⟩⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
x✝ : t ∈ {s | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty}
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ U ∈ (⋃₀ u, f '' u).2, (t ∩ U).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ U).Nonempty
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ⋃ K_1 ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}, ↑K_1 ⊆ U.preimage t

Tactic:
rw [Set.iUnion₂_subset_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ∀ i ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}, ↑i ⊆ U.preimage t
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : ClusterPt x l
⊢ ⋃ K_1 ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage U) x}, ↑K_1 ⊆ U.image ↑K

Tactic:
rw [Set.iUnion₂_subset_iff]

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : ClusterPt x l
⊢ ∀ i ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage U) x}, ↑i ⊆ U.image ↑K
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_2
𝕜 : 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
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ∀ᶠ (x : ↥S) in map (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ), IsUnit x

Tactic:
eventually_map

Goal state after:
case refine_2
𝕜 : 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
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ∀ᶠ (a : 𝕜) in 𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ, IsUnit ((algebraMap 𝕜 ↥S) a - x)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ ↑K
⊢ ∀ (i' : Set α), x ∈ i' ∧ IsOpen[inst✝.toTopologicalSpace] i' → i' ∈ f

Tactic:
intro U ⟨hxU, hU⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ ↑K
U : Set α
hxU : x ∈ U
hU : IsOpen[inst✝.toTopologicalSpace] U
⊢ U ∈ f
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_2.h.h
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, ‖↑t - x‖₊ ≤ t
x : ℝ
hx : x ∈ spectrum ℝ a
h_le : -↑t ≤ ↑t - x ∧ ↑t - x ≤ ↑t
⊢ 0 ≤ x

Tactic:
linarith [h_le.2]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝¹⁰ : Semifield R
inst✝⁹ : Field S
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Module R A
inst✝⁵ : Module S A
inst✝⁴ : IsScalarTower S A A
inst✝³ : SMulCommClass S A A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_cpct : IsCompact (σₙ S a)
⊢ IsCompact (σₙ R a)

Tactic:
exact h.image ▸ h_cpct.image (map_continuous f)

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsSemitopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σ ℝ a, 0 ≤ f x
ha : 0 ≤ a
x : ℝ
hx : x ∈ σ ℝ a
⊢ f x = ↑(f ↑x.toNNReal).toNNReal

Tactic:
rw [x.coe_toNNReal (spectrum_nonneg_of_nonneg ha hx), (f x).coe_toNNReal (hf_nonneg x hx)]

Goal state after:
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✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
rw [SetLike.not_le_iff_exists] at h'

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ∃ x ∈ K₁, x ∉ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := hu'.fintype
⊢ (univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {a |
      ⋃ a_1, ⋃ (_ : True), ↑(a a_1) ⊆ ⋃₀ u ∧
        (∀ U ∈ u, ((⋃ a_2, ⋃ (_ : True), ↑(a a_2)) ∩ U).Nonempty) ∧ (⋃ a_1, ⋃ (_ : True), ↑(a a_1)).Finite}

Tactic:
iUnion_true,

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := hu'.fintype
⊢ (univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {a | ⋃ a_1, ↑(a a_1) ⊆ ⋃₀ u ∧ (∀ U ∈ u, ((⋃ a_2, ↑(a a_2)) ∩ U).Nonempty) ∧ (⋃ a_1, ↑(a a_1)).Finite}
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous[⨅ i, induced (⇑(f i)) t𝕜, t𝕜] ⇑φ

Tactic:
let _ := ⨅ i, induced (f i) t𝕜
  constructor
  · exact Submodule.span_induction
      (Set.forall_mem_range.mpr fun i ↦ continuous_iInf_dom continuous_induced_dom) continuous_zero
      (fun _ _ _ _ ↦ .add) (fun c _ _ h ↦ h.const_smul c)
  · intro φ_cont
    refine mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_
    simp_rw [Submodule.mem_iInf, LinearMap.mem_ker] at hx ⊢
    have : Inseparable x 0 := by
      -- Maybe missing lemmas about `Inseparable`?
      simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
    simpa only [map_zero] using (this.map φ_cont).eq

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖
le : ∀ z ∈ s, ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
cancel : ‖c⁻¹‖ * ‖c‖ = 1
⊢ c⁻¹ • x' ∈ polar 𝕜 s

Tactic:
rwa [cancel] at le

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

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ ⨆ k ∈ spectrum ℂ ((gelfandTransform ℂ A) (star a * a)), ↑‖k‖₊ = ⨆ k ∈ spectrum ℂ (star a * a), ↑‖k‖₊

Tactic:
spectrum.gelfandTransform_eq

Goal state after:
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ ⨆ k ∈ spectrum ℂ (star a * a), ↑‖k‖₊ = ⨆ k ∈ spectrum ℂ (star a * a), ↑‖k‖₊
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] s)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
← compl_compl s

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
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
⊢ (cfcₙ f (a, b)).2 = (cfcₙ f a, cfcₙ f b).2

Tactic:
let φ := NonUnitalStarAlgHom.snd S A B
      exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb

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
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a c : A
hac : a = a⁺ - c
hc : 0 ≤ c
ha : IsSelfAdjoint a
⊢ a⁻ = c

Tactic:
nth_rw 1 [← posPart_sub_negPart a] at hac

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
a c : A
hac : a⁺ - a⁻ = a⁺ - c
hc : 0 ≤ c
ha : IsSelfAdjoint a
⊢ a⁻ = c
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 = -cfcₙ (fun x ↦ x⁻) a

Tactic:
← cfcₙ_neg

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ₙ (fun x ↦ -x⁻) a
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x : α
hx : x ∈ ⋃₀ 𝔖
⊢ LipschitzWith 1 fun f ↦ (toFun 𝔖) f x

Tactic:
intro f g
  simpa only [ENNReal.coe_one, one_mul] using edist_eval_le hx

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
⊢ Isometry ⇑(cfcHom ha)

Tactic:
by
    rw [cfcHom_eq_of_isStarNormal]
    exact isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
x : ℝ
ha : IsStrictlyPositive a
⊢ a ^ x * a ^ (-x) = 1

Tactic:
by
  rw [← rpow_add ha.isUnit, add_neg_cancel, rpow_zero a]

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

Goal state before:
pp: case snd
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ ((equiv A (E × F)) x).2 = ((equiv A (E × F)) 0).2

Tactic:
refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))
      exact le_add_of_nonneg_left CStarModule.inner_self_nonneg |>.trans_eq h

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

Goal state before:
pp: case h₁
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.1‖ ≤ ‖(equiv A (E × F)) x‖

Tactic:
exact norm_fst_le x

Goal state after:
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊) ≤
    Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊

Tactic:
refine Finset.sup_mono_fun fun i _hi => ?_
      gcongr with j hj
      exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj

Goal state after:
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
h : i.1 = i.2
⊢ False

Tactic:
exact Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩

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

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

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖f (∑' (n : ℕ), (2 : ℝ) ^ (-(n : ℤ)) • x n)‖ < (2 : ℝ) ^ n :=
    tendsto_pow_atTop_atTop_of_one_lt one_lt_two |>.eventually_gt_atTop _
      |>.exists

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
x : ℕ → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), 2 ^ (2 * x_1) < ‖f (x x_1)‖
x_summable : Summable fun n ↦ 2 ^ (-↑n) • x n
n : ℕ
hn : ‖f (∑' (n : ℕ), 2 ^ (-↑n) • x n)‖ < 2 ^ n
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℜ a))
ha : IsStarNormal a
⊢ cfc (fun x ↦ ↑(f x.re)) a = cfc f ↑(ℜ a)

Tactic:
have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((re · : ℂ → ℂ) '' spectrum ℂ a) := by
    rw [spectrum_realPart' a] at hf
    refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_
    simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..
  conv_rhs =>
    rw [cfc_real_eq_complex, ← cfc_re_id a, ← cfc_comp' ..]
    simp

Goal state after:
Module: Mathlib.Topology.Algebra.LinearMapCompletion

Goal state before:
pp: α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝¹¹ : UniformSpace α
inst✝¹⁰ : AddCommGroup α
inst✝⁹ : IsUniformAddGroup α
inst✝⁸ : Semiring R₁
inst✝⁷ : Module R₁ α
inst✝⁶ : UniformContinuousConstSMul R₁ α
inst✝⁵ : Semiring R₂
inst✝⁴ : UniformSpace β
inst✝³ : AddCommGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : Module R₂ β
inst✝ : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
r : R₁
x : Completion α
⊢ (↑((↑f).toAddMonoidHom.completion ⋯)).toFun (r • x) = σ r • (↑((↑f).toAddMonoidHom.completion ⋯)).toFun x

Tactic:
induction x using induction_on with
    | hp =>
      exact isClosed_eq (continuous_map.comp <| continuous_const_smul r)
        (continuous_map.fun_const_smul _)
    | ih x => simp [← Completion.coe_smul]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
⊢ ∀ (x y : f.PreGNS), (starRingEnd ℂ) (f (star (f.ofPreGNS y) * f.ofPreGNS x)) = f (star (f.ofPreGNS x) * f.ofPreGNS y)

Tactic:
by simp [← Complex.star_def, ← map_star f]

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

Goal state before:
pp: case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
k : ℕ
hk : ∀ (x y : A), (a.toProd.2 ^ k) x * y = x * (a.toProd.1 ^ k) y
x y : A
⊢ (a.toProd.2 * a.toProd.2 ^ k) x * y = x * (a.toProd.1 ^ (k + 1)) y

Tactic:
mul_apply_eq_comp,

Goal state after:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
k : ℕ
hk : ∀ (x y : A), (a.toProd.2 ^ k) x * y = x * (a.toProd.1 ^ k) y
x y : A
⊢ a.toProd.2 ((a.toProd.2 ^ k) x) * y = x * (a.toProd.1 ^ (k + 1)) y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ (↑x).arg < x.angleDiff y + (↑x).arg

Tactic:
by simp [angleDiff_pos h]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ ↑u)
y : ℂ
hy : y ∈ spectrum ℂ ↑u
hy₁ : ‖y‖ = 1
⊢ NormedSpace.exp (I • ↑y.arg) = y

Tactic:
have : I * y.arg = log y :=
    Complex.ext (by simp [log_re, spectrum.norm_eq_one_of_unitary u.2 hy]) (by simp [log_im])

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this✝ : ContinuousOn arg (spectrum ℂ ↑u)
y : ℂ
hy : y ∈ spectrum ℂ ↑u
hy₁ : ‖y‖ = 1
this : I * ↑y.arg = log y
⊢ NormedSpace.exp (I • ↑y.arg) = y
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
this : re ⟪(adjoint A ∘SL A) x, x⟫_𝕜 ≤ ‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖
⊢ ‖A x‖ = √(re ⟪(adjoint A ∘SL A) x, x⟫_𝕜)

Tactic:
rw [apply_norm_eq_sqrt_inner_adjoint_left]

Goal state after: