mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹² : Semifield S
inst✝¹¹ : StarRing S
inst✝¹⁰ : MetricSpace S
inst✝⁹ : IsTopologicalSemiring S
inst✝⁸ : ContinuousStar S
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(spectrum S a), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts a ⇑f
h_id : φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
⊢ (starAlgHom φ h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a

Tactic:
by
  simp only [SpectrumRestricts.starAlgHom_apply]
  convert! h_id
  ext x
  exact h.rightInvOn x.2

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : CompleteSpace E
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
ha : IsBot a
A : Iic a = {a}
⊢ Iio a = ∅

Tactic:
simp [ha.isMin]

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
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ (spectrum R a).domRestrict f x ∈
    spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })

Tactic:
sp_eq

Goal state after:
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
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ (spectrum R a).domRestrict f x ∈ f '' spectrum R a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: 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
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
x : ↑(σₙ R a)
⊢ (σₙ R a).domRestrict f x ∈
    σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ })

Tactic:
sp_eq

Goal state after:
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
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
x : ↑(σₙ R a)
⊢ (σₙ R a).domRestrict f x ∈ f '' σₙ R a
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: case calc_1
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
hn₀ : n ≠ 0
x : ↑I
S : Finset (Fin (n + 1)) := {k | dist k/ₙ x < δ}
⊢ ∑ k ∈ S, (bernstein n ↑k) x * gauge U (f k/ₙ - f x) ≤ 1 / 2

pp: case calc_2
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
hn₀ : n ≠ 0
x : ↑I
S : Finset (Fin (n + 1)) := {k | dist k/ₙ x < δ}
⊢ ∑ k ∈ Sᶜ, (bernstein n ↑k) x * gauge U (f k/ₙ - f x) < 1 / 2

Tactic:
· -- We now work on the terms in `S`: uniform continuity and `bernstein.probability`
    -- quickly give us a bound.
    calc
      ∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ S, bernstein n k x * (1 / 2) := by
        gcongr with k hk
        refine (hδ _ _ ?_).le
        simpa [S] using hk
      _ = 1 / 2 * ∑ k ∈ S, bernstein n k x := by rw [mul_comm, Finset.sum_mul]
      -- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
      -- so that we can use `bernstein.probability`.
      _ ≤ 1 / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
      _ = 1 / 2 := by rw [bernstein.probability, mul_one]

Goal state after:
case calc_2
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
hn₀ : n ≠ 0
x : ↑I
S : Finset (Fin (n + 1)) := {k | dist k/ₙ x < δ}
⊢ ∑ k ∈ Sᶜ, (bernstein n ↑k) x * gauge U (f k/ₙ - f x) < 1 / 2
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f g : C(X, ℝ)
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)

Tactic:
have := congr(φ $(f.toNNReal_add_add_neg_add_neg_eq g))
    simp only [map_add] at this ⊢
    rw [← sub_eq_zero] at this ⊢
    convert! this using 1
    abel

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

Goal state before:
pp: case pos
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 : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose
xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhds)
xs_nonempty : xs.Nonempty
k : ↑L := ⟨xs.inf' xs_nonempty fun x ↦ ↑(h x), ⋯⟩
⊢ dist (↑k) f < ε

Tactic:
dist_lt_iff pos

Goal state after:
case pos
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 : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose
xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhds)
xs_nonempty : xs.Nonempty
k : ↑L := ⟨xs.inf' xs_nonempty fun x ↦ ↑(h x), ⋯⟩
⊢ ∀ (x : X), dist (↑k x) (f x) < ε
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖ ≤
    ↑2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖

Tactic:
NNReal.coe_two

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖ ≤
    2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ : ∀ (x : Unitization 𝕜 E), ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖
h₂ : ‖((splitMul 𝕜 E) (x⋆ * x)).2‖ = ‖((splitMul 𝕜 E) x).2‖ ^ 2
h₃ : ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ = ‖((splitMul 𝕜 E) x).1‖ ^ 2
⊢ max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ * max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ ≤
    max ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ (‖((splitMul 𝕜 E) x).2‖ ^ 2)

Tactic:
h₃

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ : ∀ (x : Unitization 𝕜 E), ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖
h₂ : ‖((splitMul 𝕜 E) (x⋆ * x)).2‖ = ‖((splitMul 𝕜 E) x).2‖ ^ 2
h₃ : ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ = ‖((splitMul 𝕜 E) x).1‖ ^ 2
⊢ max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ * max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ ≤
    max (‖((splitMul 𝕜 E) x).1‖ ^ 2) (‖((splitMul 𝕜 E) x).2‖ ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ : ∀ (x : Unitization 𝕜 E), ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖
h₂ : ‖((splitMul 𝕜 E) (x⋆ * x)).2‖ = ‖((splitMul 𝕜 E) x).2‖ ^ 2
h₃ : ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ = ‖((splitMul 𝕜 E) x).1‖ ^ 2
h : ‖((splitMul 𝕜 E) x).2‖ < ‖((splitMul 𝕜 E) x).1‖
⊢ max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ * max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ ≤
    max (‖((splitMul 𝕜 E) x).1‖ ^ 2) (‖((splitMul 𝕜 E) x).2‖ ^ 2)

Tactic:
replace h := h.le
      rw [sq, sq, sup_eq_left.mpr h, sup_eq_left.mpr (mul_self_le_mul_self (norm_nonneg _) h)]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
⊢ characterSpace 𝕜 A = {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}

Tactic:
ext φ
  refine ⟨?_, ?_⟩
  · rintro hφ
    lift φ to characterSpace 𝕜 A using hφ
    exact ⟨map_one φ, map_mul φ⟩
  · rintro ⟨hφ₁, hφ₂⟩
    refine ⟨?_, hφ₂⟩
    rintro rfl
    exact zero_ne_one hφ₁

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
x✝¹ : Set (α × α) × Set (β × β)
U : Set (α × α)
V : Set (β × β)
x✝ : (U, V).1 ∈ 𝓤 α ∧ (U, V).2 ∈ 𝓤 β
hU : (U, V).1 ∈ 𝓤 α
hV : (U, V).2 ∈ 𝓤 β
⊢ ∀ᶠ (x : (Set α × Set β) × Set α × Set β) in 𝓤 (Set α × Set β),
    ((fun x ↦ x.1 ×ˢ x.2) x.1, (fun x ↦ x.1 ×ˢ x.2) x.2) ∈
      (hausdorffEntourage ∘ fun i ↦ entourageProd (id i.1) (id i.2)) (U, V)

Tactic:
filter_upwards [entourageProd_mem_uniformity (Filter.mem_lift' hU) (Filter.mem_lift' hV)]
    with ⟨⟨s₁, s₂⟩, ⟨t₁, t₂⟩⟩ ⟨h₁, h₂⟩ using prod_mem_hausdorffEntourage_entourageProd U V h₁ h₂

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

Goal state before:
pp: case inl
α : 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}
hs : ∅ ∈ (range fun x ↦ {x})ᶜ
⊢ (range fun x ↦ {x})ᶜ ∈ 𝓝 ∅

Tactic:
rwa [(isOpen_singleton_iff_nhds_eq_pure _).mp h₁, Filter.mem_pure]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : z = 0
⊢ IsUnit (1 - z • a)

Tactic:
simp only [hz, isUnit_one, sub_zero, zero_smul]

Goal state after:
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 ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
⊢ ∃ t, t.Finite ∧ U.preimage t ∈ l

Tactic:
rw [← SetRel.preimage_eq_biUnion] at ht₂

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
⊢ ∃ t, t.Finite ∧ U.preimage t ∈ l
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case pos.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
this :
  ∀ (U V : Set α),
    IsOpen[inst✝] U →
      IsOpen[inst✝] V →
        ⋃₀ s ⊆ U ∪ V → t ⊆ U ∨ t ⊆ V → t ⊆ U → (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty
htU : ¬t ⊆ U
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty

pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
htU : t ⊆ U
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty

Tactic:
· grind

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
htU : t ⊆ U
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: case lower
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ {z | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0}

pp: case upper
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ {z | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}

Tactic:
all_goals
    refine Set.subset_inter (fun z hz hz' ↦ ?_) (fun _ ↦ by simpa using le_of_lt)
    rw [Set.mem_ofPred_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz
    simp_all

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x s : Unitization ℂ A
hs : IsSelfAdjoint s
this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s
⊢ ‖ψ s‖₊ ≤ ‖s‖₊

Tactic:
by
      rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this

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✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
⊢ ∃ M, IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ (↑K ∩ interior M).Nonempty

Tactic:
obtain ⟨x, hxK, hxU⟩ := hKu₂ U hU

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ ↑K
hxU : x ∈ U
⊢ ∃ M, IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ (↑K ∩ interior M).Nonempty
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 = a ^ 2 + 2 • (a * b) + b ^ 2
h₄ :
  deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    star a ^ 2 + 2 • (star a * -a) + a ^ 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    a ^ 2 + 2 • (-a * star a) + star a ^ 2
⊢ IsStarNormal a

Tactic:
h₃

Goal state after:
case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 = a ^ 2 + 2 • (a * b) + b ^ 2
h₄ : a ^ 2 + 2 • (-a * star a) + star a ^ 2 = star a ^ 2 + 2 • (star a * -a) + a ^ 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    a ^ 2 + 2 • (-a * star a) + star a ^ 2
⊢ IsStarNormal a
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
⊢ dist c₁ c₂ ≤ ↑(nndist p₁ p₂)⁻¹ * dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂)

Tactic:
rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]

Goal state after:
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 b' : E
r : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ r
h₁ : r ≤ 1
⊢ (lineMap a b) r < (lineMap a' b') r

Tactic:
by
  rcases h₀.eq_or_lt with (rfl | h₀); · simpa
  exact (lineMap_mono_left ha.le h₁).trans_lt (lineMap_strict_mono_right hb h₀)

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
K V : Set X
hK : IsCompact K
hV : IsOpen[inst✝²] V
hKV : K ⊆ V
U : Set X
hU1 : IsOpen[inst✝²] U
hU2 : K ⊆ U
hU3 : closure[inst✝²] U ⊆ V
hU4 : IsCompact (closure[inst✝²] U)
f : C(X, ℝ)
hf1 : tsupport ⇑f ⊆ U
hf2 : EqOn (⇑f) 1 (closure[inst✝²] K)
hf3 : ∀ (x : X), f x ∈ Icc 0 1
hfU : tsupport ⇑f ⊆ closure[inst✝²] U
⊢ ∃ f, EqOn (⇑f) 1 K ∧ IsCompact (tsupport ⇑f) ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
exact ⟨f, hf2.mono subset_closure,
    .of_isClosed_subset hU4 isClosed_closure hfU, hfU.trans hU3, hf3⟩

Goal state after: