mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ (fun x ↦ -f x) a = -cfcₙ f a

Tactic:
simp only [not_and_or] at h

Goal state after:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
⊢ cfcₙ (fun x ↦ -f x) a = -cfcₙ f a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h0 : ¬f 0 = 0
⊢ cfcₙ (fun x ↦ -f x) a = -cfcₙ f a

Tactic:
· rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, neg_zero]
      exact (h0 <| neg_eq_zero.mp ·)

Goal state after:
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
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2

Tactic:
let e : Bool → R[X] := fun i => cond i X (1 - X)

Goal state after:
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
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: 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
⊢ ∃ δ > 0, ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2

Tactic:
have := CompactSpace.uniformContinuous_of_continuous (map_continuous f)

Goal state after:
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
this : UniformContinuous ⇑f
⊢ ∃ δ > 0, ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_2
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 + ε}
x : X
⊢ ↑(h x) x < f x + ε

Tactic:
h_eq

Goal state after:
case refine_2
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 + ε}
x : X
⊢ f x < f x + ε
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 : ∀ (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), ⋯⟩
z : X
⊢ ∀ (a b ε : ℝ), dist a b < ε ↔ a < b + ε ∧ b - ε < a

Tactic:
intros; simp only [← Metric.mem_ball, Real.ball_eq_Ioo, Set.mem_Ioo, and_comm]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous (_root_.toContinuousMap ∘ toNNReal)

Tactic:
convert_to! Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous (ContinuousMap.toNNReal ∘ _root_.toContinuousMap)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ 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:
by
    have := congr(φ $(f.toNNReal_add_add_neg_add_neg_eq g))
    simp only [map_add] at this ⊢
    rw [← sub_eq_zero] at this ⊢
    rw [← this]
    abel

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Fact (0 ∈ s)
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id s}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f : C(↑s, 𝕜)₀
⊢ p f

Tactic:
refine closure (fun f hf => ?_) f
  induction hf using NonUnitalAlgebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq] at hf
    obtain (rfl | rfl) := hf
    all_goals assumption
  | zero => exact zero
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg
  | smul _ _ _ hf => exact smul _ _ hf

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
⊢ IsOpen[generateFrom (powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V})]
    ({a | a ⊆ ⋃₀ u} ∩ {a | ∀ U ∈ u, (a ∩ U).Nonempty})

Tactic:
ofPred_forall

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
⊢ IsOpen[generateFrom (powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V})]
    ({a | a ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x | (x ∩ i).Nonempty})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
⊢ ∀ x ∈ ⋂₀ t,
    ∃ v ∈ (fun u ↦ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
      x ∈ v ∧ v ⊆ ⋂₀ t

Tactic:
s

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
s : Set α
⊢ s ∈ ⋂₀ t →
    ∃ v ∈ (fun u ↦ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
      s ∈ v ∧ v ⊆ ⋂₀ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] (V, u).1
hu : (V, u).2.Finite
huB : (V, u).2 ⊆ B
right✝ : ∀ U ∈ (V, u).2, U ⊆ (V, u).1
⊢ IsOpen[TopologicalSpace.vietoris α] ({a | a ⊆ V} ∩ {a | ∀ U ∈ u, (a ∩ U).Nonempty})

Tactic:
ofPred_forall

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] (V, u).1
hu : (V, u).2.Finite
huB : (V, u).2 ⊆ B
right✝ : ∀ U ∈ (V, u).2, U ⊆ (V, u).1
⊢ IsOpen[TopologicalSpace.vietoris α] ({a | a ⊆ V} ∩ ⋂ i ∈ u, {x | (x ∩ i).Nonempty})
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
⊢ ∀ x ∈ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty},
    ∃
      v ∈
        (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
      x ∈ v ∧ v ⊆ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
s

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 α
⊢ s ∈ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} →
    ∃
      v ∈
        (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
      s ∈ v ∧ v ⊆ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ (∀ (U : Set α), IsOpen[inst✝¹] U → IsOpen[Pi.topologicalSpace] {a | ∀ (y : ι), a y ∈ U}) ∧
    ∀ (F : Set α), IsClosed[inst✝¹] F → IsClosed[Pi.topologicalSpace] {a | ∀ (y : ι), a y ∈ F}

Tactic:
ofPred_forall

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ (∀ (U : Set α), IsOpen[inst✝¹] U → IsOpen[Pi.topologicalSpace] (⋂ i, {x | x i ∈ U})) ∧
    ∀ (F : Set α), IsClosed[inst✝¹] F → IsClosed[Pi.topologicalSpace] (⋂ i, {x | x i ∈ F})
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
⊢ IsPreconnected {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s}

Tactic:
suffices {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} =
      ⋃ n : ℕ+, range (ι := Fin n) '' Set.pi univ fun _ => s by
    rw [this]
    /- The family of nonempty subsets of `s` with at most `n` elements is connected, since it is the
    image of `sⁿ` under the continuous map `(x₁, …, xₙ) ↦ {x₁, …, xₙ}`. It follows that their union
    over `n ≥ 1` is also connected. -/
    exact isPreconnected_iUnion
      ⟨{x}, mem_iInter_of_mem fun n => ⟨fun _ => x, by simpa⟩⟩
      (fun n => .image (isPreconnected_univ_pi fun _ => hs) _ (by fun_prop))

Goal state after:
case inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
⊢ {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} = ⋃ n, range '' univ.pi fun x ↦ s
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
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ map (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ) ≤ 𝓝 ((algebraMap 𝕜 ↥S) μ - x)

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:
· calc
      _ ≤ map _ (𝓝 μ) := map_mono (by simp)
      _ ≤ _ := by rw [← Filter.Tendsto, ← ContinuousAt]; fun_prop

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)ᶜ
⊢ ∀ᶠ (x : ↥S) in map (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ), IsUnit x
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen ({a | ↑a ⊆ ⋃₀ u} ∩ {a | ∀ U ∈ u, (↑a ∩ U).Nonempty})

Tactic:
ofPred_forall

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen ({a | ↑a ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x | (↑x ∩ i).Nonempty})
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁶ : NormedRing A
inst✝⁵ : CompleteSpace A
inst✝⁴ : SetLike SA A
inst✝³ : SubringClass SA A
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
z : 𝕜
hz✝ : z ∈ σ 𝕜 x \ σ 𝕜 ↑x
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
⊢ Bornology.IsBounded univ

Tactic:
have := (spectrum.isBounded (x : A)).union <|
    h.connectedComponentIn hz' ▸ spectrum_isBounded_connectedComponentIn S x hz

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁶ : NormedRing A
inst✝⁵ : CompleteSpace A
inst✝⁴ : SetLike SA A
inst✝³ : SubringClass SA A
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
z : 𝕜
hz✝ : z ∈ σ 𝕜 x \ σ 𝕜 ↑x
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
this : Bornology.IsBounded (σ 𝕜 ↑x ∪ (σ 𝕜 ↑x)ᶜ)
⊢ Bornology.IsBounded univ
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_1
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, 0 ≤ x
x : ℝ
hx : x ∈ {↑t} - spectrum ℝ a
⊢ ↑‖x‖₊ ≤ ↑t

Tactic:
obtain ⟨y, hy, rfl⟩ : ∃ y ∈ spectrum ℝ a, ↑t - y = x := by simpa using hx

Goal state after:
case refine_1
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, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : ↑t - y ∈ {↑t} - spectrum ℝ a
⊢ ↑‖↑t - y‖₊ ≤ ↑t
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : IsStrictlyPositive a
hb : IsStrictlyPositive b
⊢ Commute a b ↔ IsStrictlyPositive (a * b)

Tactic:
rw [commute_iff_mul_nonneg ha.nonneg hb.nonneg]

Goal state after:
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : IsStrictlyPositive a
hb : IsStrictlyPositive b
⊢ 0 ≤ a * b ↔ IsStrictlyPositive (a * b)
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ ‖k‖ ≤ 1

pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ 1 ≤ ‖k‖

Tactic:
· simpa only [CStarRing.norm_coe_unitary u] using norm_le_norm_of_mem hk

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ 1 ≤ ‖k‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Nontrivial A
⊢ ‖cfc f a‖₊ < c

Tactic:
refine cfc_cases (‖·‖₊ < c) a f (by simpa) fun hf ha ↦ ?_

Goal state after:
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ ‖(cfcHom ha) { toFun := (σ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ }‖₊ < c
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
ha₁ : IsUnit (↑a⋆ * ↑a)
ha₂ : IsUnit (↑a * ↑a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

Tactic:
← MulMemClass.coe_mul,

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)
ha₂ : IsUnit ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
⊢ IsCompact (⋃ K ∈ S, ↑K)

Tactic:
by
  rw [isCompact_iff_finite_subcover]
  intro ι U hU h
  rw [iUnion₂_subset_iff] at h
  obtain ⟨s, hs⟩ := hS.elim_finite_subcover
    (fun s : Finset ι => {K | (K : Set α) ⊆ ⋃ i ∈ s, U i})
    (fun s => isOpen_subsets_of_isOpen <| isOpen_biUnion fun _ _ => hU _)
    (fun K hK => mem_iUnion.mpr <| K.isCompact.elim_finite_subcover U hU <| h K hK)
  classical
  refine ⟨s.biUnion id, (biUnion_subset_biUnion_left hs).trans ?_⟩
  simp_rw [biUnion_iUnion, iUnion_subset_iff, Finset.set_biUnion_biUnion]
  exact fun t ht K hK => subset_iUnion₂_of_subset t ht hK

Goal state after:
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 ∧ ∀ x ∈ B.polar Set.univ, x = 0

Tactic:
refine ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => ?_⟩

Goal state after:
𝕜 : 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
y : F
hy : y ∈ B.polar Set.univ
x : E
⊢ (B x) y = 0
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ balancedHull ℝ s ⊆ (convexHull ℝ) (s ∪ -s)

Tactic:
intro a ha
  obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 ha
  apply segment_subset_convexHull (mem_union_left (-s) hy) (mem_union_right _ (neg_mem_neg.mpr hy))
  have : 0 ≤ 1 + r := neg_le_iff_add_nonneg'.mp (neg_le_of_abs_le hr)
  have : 0 ≤ 1 - r := sub_nonneg.2 (le_of_abs_le hr)
  refine ⟨(1 + r)/2, (1 - r)/2, by positivity, by positivity, by ring, ?_⟩
  rw [smul_neg, ← sub_eq_add_neg, ← sub_smul]
  ring_nf

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

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hgx : g x = g ↑⟨x, ⋯⟩
⊢ g x = ↑‖x‖

Tactic:
have hcx : coord ⟨x, _⟩ = 1 := LinearEquiv.coord_self 𝕜 E x (ne_zero_of_norm_ne_zero h)

Goal state after:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hgx : g x = g ↑⟨x, ⋯⟩
hcx : coord ⟨x, ⋯⟩ = 1
⊢ g x = ↑‖x‖