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

Goal state before:
pp: case mp
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ f ≤ g → ∃ s, g = f + star s * s

pp: case mpr
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ (∃ s, g = f + star s * s) → f ≤ g

Tactic:
· rw [ContinuousMap.le_def]
    intro h
    use (mk _ ContinuousSqrt.continuousOn_sqrt.domRestrict).comp
      ⟨_, map_continuous (f.prodMk g) |>.codRestrict (s := {x | x.1 ≤ x.2}) (by exact h)⟩
    ext x
    simpa [IsSelfAdjoint.star_eq <| .of_nonneg (ContinuousSqrt.sqrt_nonneg (f x, g x) (h x))]
      using ContinuousSqrt.sqrt_mul_sqrt (f x, g x) (h x)

Goal state after:
case mpr
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ (∃ s, g = f + star s * s) → f ≤ g
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := ⋯
f : α → ℝ≥0∞ := ⋯
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
⊢ μ (s ∩ f ⁻¹' {∞}) = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
⊢ μ (s ∩ f ⁻¹' {∞}) ≤ 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)

Tactic:
apply le_antisymm _ (edist_le f (by simp) (by simp))

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
⊢ eVariationOn f {a, b} ≤ edist (f a) (f b)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
f : R → R
n : ℕ
a : A
hf : ContinuousOn f ((fun x ↦ x ^ n) '' spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f (x ^ n)) a = cfc f (a ^ n)

Tactic:
by
  rw [cfc_comp' .., cfc_pow_id ..]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
r : R
f : R → R
a : A
hf : ContinuousOn f ((fun x ↦ r * x) '' spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f (r * x)) a = cfc f (r • a)

Tactic:
rw [cfc_comp' .., cfc_const_mul_id ..]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Field S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalRing S
inst✝¹² : ContinuousStar S
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module S A
inst✝⁸ : IsScalarTower S A A
inst✝⁷ : SMulCommClass S A A
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : CompleteSpace R
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
hφ : IsClosedEmbedding ⇑φ
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
halg : IsUniformEmbedding ⇑(algebraMap R S)
⊢ IsClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)

Tactic:
have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _)

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Field S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalRing S
inst✝¹² : ContinuousStar S
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module S A
inst✝⁸ : IsScalarTower S A A
inst✝⁷ : SMulCommClass S A A
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : CompleteSpace R
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
hφ : IsClosedEmbedding ⇑φ
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
halg : IsUniformEmbedding ⇑(algebraMap R S)
this : h.homeomorph.symm 0 = 0
⊢ IsClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
⊢ cfc f 0 = (algebraMap R A) (f 0)

Tactic:
by
  simpa using cfc_algebraMap (A := A) 0 f

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Semiring A
inst✝¹² : StarRing A
inst✝¹¹ : IsSemitopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
⊢ φ = ψ

Tactic:
refine StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Semiring A
inst✝¹² : StarRing A
inst✝¹¹ : IsSemitopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
⊢ φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
a b : α
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
⊢ ENNReal.ofReal (f b - f a) ≤ ENNReal.ofReal (2 * C)

Tactic:
exact ofReal_mono (by grind)

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

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ ↑(NonUnitalAlgHomClass.toNonUnitalAlgHom (cfcₙHom ha)) f ∈ Set.range fun x ↦ cfcₙ x a

Tactic:
exact ⟨Subtype.val.extend f 0, cfcₙHom_eq_cfcₙ_extend _ ha _ |>.symm⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ X.toContinuousMap = ContinuousMap.id R

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
⊢ X.toContinuousMapOn s = restrict s (ContinuousMap.id R)

Tactic:
ext; simp

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

Goal state before:
pp: ⊢ ⊤ ≤ (polynomialFunctions I).topologicalClosure

Tactic:
rintro f -

Goal state after:
f : C(↑I, ℝ)
⊢ f ∈ (polynomialFunctions I).topologicalClosure
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
w : ∀ (k : ℕ), k • bernsteinPolynomial R n k = ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(n.choose k) * X
k : ℕ
x✝ : k ∈ Finset.range (n + 1)
⊢ ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(n.choose k) * X =
    (MvPolynomial.aeval e) ((pderiv true) (x ^ k * y ^ (n - k) * ↑(n.choose k))) * X

Tactic:
simp only [x, y, e, pderiv_true_x, pderiv_true_y, smul_eq_mul, nsmul_eq_mul,
      Bool.cond_true, Bool.cond_false, add_zero, mul_one, mul_zero, MvPolynomial.aeval_X,
      MvPolynomial.pderiv_mul, Derivation.leibniz_pow, Derivation.map_natCast, map_natCast, map_pow,
      map_mul]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
⊢ ⊤ ⊆ closure L

Tactic:
rintro f -

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
f : C(X, ℝ)
⊢ f ∈ closure L
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
⊢ (Polynomial.toContinuousMapOnAlgHom s) Polynomial.X = ContinuousMap.restrict s (ContinuousMap.id 𝕜)

Tactic:
ext; simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
⊢ ((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = (algebraMap ℝ≥0 C(X, ℝ≥0)) r

Tactic:
ext; simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
⊢ (-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = 0

Tactic:
ext; simp

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

Goal state before:
pp: case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
a✝ : A
hx : (mul 𝕜 A) a✝ = 0
⊢ ↑a✝ = 0

Tactic:
← map_zero (mul 𝕜 A)

Goal state after:
case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
a✝ : A
hx : (mul 𝕜 A) a✝ = (mul 𝕜 A) 0
⊢ ↑a✝ = 0
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 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝¹ x✝ : F
⊢ { toLinearMap := B.flip (x✝¹ + x✝), cont := ⋯ } =
    { toLinearMap := B.flip x✝¹, cont := ⋯ } + { toLinearMap := B.flip x✝, cont := ⋯ }

Tactic:
ext; simp

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✝⁶ : CommSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝¹ : 𝕜
x✝ : F
⊢ { toLinearMap := B.flip (x✝¹ • x✝), cont := ⋯ } = (RingHom.id 𝕜) x✝¹ • { toLinearMap := B.flip x✝, cont := ⋯ }

Tactic:
ext; simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ (∃ y ∈ 𝕜 ∙ 1, ∃ z ∈ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).toSubmodule, y + z = x) ↔
    x ∈ ↑(𝕜 ∙ 1) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
simp [Set.mem_add]

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

Goal state before:
pp: case inr
𝕜 : 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 - φ 1 = 0
⊢ φ 1 = 1

Tactic:
exact (sub_eq_zero.mp h₂).symm

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

Goal state before:
pp: case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
⊢ s₁ ⊆ s₁ ∧ s₃ ⊆ s₃

Tactic:
exact ⟨subset_rfl, subset_rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
⊢ IsClosed[t] (range fun x ↦ {x})

Tactic:
by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro s hs
  rcases Set.eq_empty_or_nonempty s with rfl | h
  · rwa [(isOpen_singleton_iff_nhds_eq_pure _).mp h₁, Filter.mem_pure]
  rcases h.exists_eq_singleton_or_nontrivial with ⟨x, rfl⟩ | ⟨x, hx, y, hy, hxy⟩
  · cases hs <| Set.mem_range_self x
  obtain ⟨U, V, hU, hV, hxU, hyV, hUV⟩ := t2_separation hxy
  filter_upwards [(h₂ hU).inter (h₂ hV) |>.mem_nhds ⟨⟨x, hx, hxU⟩, ⟨y, hy, hyV⟩⟩]
  rintro _ ⟨hzU, hzV⟩ ⟨z, rfl⟩
  rw [Set.mem_ofPred, Set.singleton_inter_nonempty] at hzU hzV
  exact hUV.notMem_of_mem_left hzU hzV

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      Prod.mk s ⁻¹' {x | x.1 ⊆ i'.preimage x.2 ∧ x.2 ⊆ i'.image x.1} ∈ 𝓝 s

Tactic:
Set.preimage_ofPred_eq,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a | s ⊆ i'.preimage a ∧ a ⊆ i'.image s} ∈ 𝓝 s
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✝ : CompactSpace α
⊢ ∀ (f : Ultrafilter (Set α)), ↑f ≤ 𝓟 Set.univ → ∃ x ∈ Set.univ, ↑f ≤ 𝓝 x

Tactic:
rintro f -

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompactSpace α
f : Ultrafilter (Set α)
⊢ ∃ x ∈ Set.univ, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : {x | x = ⊥} ⊆ {⊥} → ∃ u, {x | ↑x ⊆ ⋂ i ∈ u, F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅

Tactic:
Set.ofPred_eq_eq_singleton

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 = ∅
this : {⊥} ⊆ {⊥} → ∃ u, {x | ↑x ⊆ ⋂ i ∈ u, F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ ∀ i ∈ {s | t ∈ s ∧ s ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}},
    ⨅
        s_1 ∈
          {s_2 |
            s ∈ s_2 ∧
              s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
        Filter.principal s_1 ≤
      Filter.principal i

Tactic:
rintro _ ⟨hs, ⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩⟩

Goal state after:
case refine_2.inl
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
hs : t ∈ 𝒫 U
⊢ ⨅
      s_1 ∈
        {s_2 |
          s ∈ s_2 ∧
            s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
      Filter.principal s_1 ≤
    Filter.principal (𝒫 U)

case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
hs : t ∈ (fun V ↦ {s | (s ∩ V).Nonempty}) U
⊢ ⨅
      s_1 ∈
        {s_2 |
          s ∈ s_2 ∧
            s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
      Filter.principal s_1 ≤
    Filter.principal ((fun V ↦ {s | (s ∩ V).Nonempty}) U)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_1
𝕜 : 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⁻¹)
mem : ↑ha.unit⁻¹ ∈ S
⊢ a * ⟨↑ha.unit⁻¹, mem⟩ = 1

Tactic:
ext; simp

Goal state after:
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
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⁻¹)
mem : ↑ha.unit⁻¹ ∈ S
⊢ ⟨↑ha.unit⁻¹, mem⟩ * a = 1

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s t : Set α
inst✝ : T1Space α
⊢ s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure[inst✝¹] s

Tactic:
specializes_iff,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
s t : Set α
inst✝ : T1Space α
⊢ (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝¹] s ↔ s ⊆ t ∧ t ⊆ closure[inst✝¹] s
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 ↑a
⊢ x ≤ ‖a‖₊

Tactic:
simpa [Unitization.nnnorm_inr] using spectrum.le_nnnorm_of_mem hx

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ quasispectrum ℝ≥0 a
⊢ x ≤ ‖a‖₊

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' ℝ≥0 ℂ] at hx
  simpa [Unitization.nnnorm_inr] using spectrum.le_nnnorm_of_mem hx

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

Goal state before:
pp: case e_u
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ 1 / ↑‖a ^ n‖.toNNReal ^ (1 / ↑n) = 1 / ↑(‖a ^ n‖.toNNReal ^ (1 / ↑n))

Tactic:
rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]

Goal state after:
case e_u.hnc
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ ¬(‖a ^ n‖₊ = 0 ∧ 1 / ↑n < 0)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : 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)
⊢ Isometry ⇑(cfcₙHom ha)

Tactic:
rw [cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom]

Goal state after:
𝕜 : 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)
⊢ Isometry
    ⇑((↑(cfcHom ha)).comp
        ((↑(ContinuousMap.compStarAlgHom' 𝕜 𝕜 { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
          ContinuousMapZero.toContinuousMapHom))
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
⊢ IsUnit a

Tactic:
have ha₁ := ha.star.mul ha

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit ((↑a)⋆ * ↑a)
⊢ IsUnit a
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 : α → Compacts β
g : α → β → γ
hf : Continuous[inst✝², _] f
hg : Continuous[instTopologicalSpaceProd, inst✝] (Function.uncurry g)
x : α
⊢ Compacts.map (g x) ⋯ (f x) = Compacts.map (Function.uncurry g) hg ({x} ×ˢ f x)

Tactic:
ext; simp

Goal state after: