mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case zero
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
⊢ 0 • bernsteinPolynomial R n 0 = ↑0 * X ^ (0 - 1) * (1 - X) ^ (n - 0) * ↑(n.choose 0) * X

pp: case succ
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
k : ℕ
⊢ (k + 1) • bernsteinPolynomial R n (k + 1) =
    ↑(k + 1) * X ^ (k + 1 - 1) * (1 - X) ^ (n - (k + 1)) * ↑(n.choose (k + 1)) * X

Tactic:
· simp

Goal state after:
case succ
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
k : ℕ
⊢ (k + 1) • bernsteinPolynomial R n (k + 1) =
    ↑(k + 1) * X ^ (k + 1 - 1) * (1 - X) ^ (n - (k + 1)) * ↑(n.choose (k + 1)) * X
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case zero
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
⊢ (0 * (0 - 1)) • bernsteinPolynomial R n 0 =
    ↑(n.choose 0) * ((1 - X) ^ (n - 0) * (↑0 * (↑(0 - 1) * X ^ (0 - 1 - 1)))) * X ^ 2

pp: case succ.zero
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
⊢ ((0 + 1) * (0 + 1 - 1)) • bernsteinPolynomial R n (0 + 1) =
    ↑(n.choose (0 + 1)) * ((1 - X) ^ (n - (0 + 1)) * (↑(0 + 1) * (↑(0 + 1 - 1) * X ^ (0 + 1 - 1 - 1)))) * X ^ 2

pp: case succ.succ
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
k : ℕ
⊢ ((k + 1 + 1) * (k + 1 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2

Tactic:
· simp

Goal state after:
case succ.zero
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
⊢ ((0 + 1) * (0 + 1 - 1)) • bernsteinPolynomial R n (0 + 1) =
    ↑(n.choose (0 + 1)) * ((1 - X) ^ (n - (0 + 1)) * (↑(0 + 1) * (↑(0 + 1 - 1) * X ^ (0 + 1 - 1 - 1)))) * X ^ 2

case succ.succ
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
k : ℕ
⊢ ((k + 1 + 1) * (k + 1 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ.zero
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
⊢ ((0 + 1) * (0 + 1 - 1)) • bernsteinPolynomial R n (0 + 1) =
    ↑(n.choose (0 + 1)) * ((1 - X) ^ (n - (0 + 1)) * (↑(0 + 1) * (↑(0 + 1 - 1) * X ^ (0 + 1 - 1 - 1)))) * X ^ 2

pp: case succ.succ
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
k : ℕ
⊢ ((k + 1 + 1) * (k + 1 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2

Tactic:
· simp

Goal state after:
case succ.succ
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
k : ℕ
⊢ ((k + 1 + 1) * (k + 1 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C(↑(σₙ R a), R)₀
h :
  ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
            toContinuousMapHom).toNonUnitalAlgHom
      f =
    ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
            toContinuousMapHom).toNonUnitalAlgHom
      g
⊢ f 0 = g 0

pp: case inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C(↑(σₙ R a), R)₀
h :
  ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
            toContinuousMapHom).toNonUnitalAlgHom
      f =
    ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
            toContinuousMapHom).toNonUnitalAlgHom
      g
x : ↑(σₙ R a)
hx : x ≠ 0
⊢ f x = g x

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C(↑(σₙ R a), R)₀
h :
  ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
            toContinuousMapHom).toNonUnitalAlgHom
      f =
    ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
            toContinuousMapHom).toNonUnitalAlgHom
      g
x : ↑(σₙ R a)
hx : x ≠ 0
⊢ f x = g x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousMapZero.UniqueHom R A
inst✝ : CompleteSpace R
a : A
ha : p a
⊢ IsClosedEmbedding ⇑(cfcₙHom ha)

Tactic:
rw [cfcₙHom_eq_cfcₙHom_of_cfcHom (R := R) ha]
    exact isClosedEmbedding_cfcₙHom_of_cfcHom ha

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_2.zero
R : Type u_1
inst✝ : CommRing R
p :
  ∑ x ∈ Finset.range (0 + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * 0) * X) * ↑x + ↑(0 ^ 2) * X ^ 2) * bernsteinPolynomial R 0 x =
    ↑(0 * (0 - 1)) * X ^ 2 + (1 - (2 * 0) • X) * 0 • X + 0 ^ 2 • X ^ 2 * 1
⊢ ↑0 * ↑(0 - 1) * X ^ 2 + (1 - 2 * ↑0 * X) * (↑0 * X) + ↑0 ^ 2 * X ^ 2 * 1 = ↑0 * X * (1 - X)

pp: case calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
p :
  ∑ x ∈ Finset.range (n✝ + 1 + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * (n✝ + 1)) * X) * ↑x + ↑((n✝ + 1) ^ 2) * X ^ 2) * bernsteinPolynomial R (n✝ + 1) x =
    ↑((n✝ + 1) * (n✝ + 1 - 1)) * X ^ 2 + (1 - (2 * (n✝ + 1)) • X) * (n✝ + 1) • X + (n✝ + 1) ^ 2 • X ^ 2 * 1
⊢ ↑(n✝ + 1) * ↑(n✝ + 1 - 1) * X ^ 2 + (1 - 2 * ↑(n✝ + 1) * X) * (↑(n✝ + 1) * X) + ↑(n✝ + 1) ^ 2 * X ^ 2 * 1 =
    ↑(n✝ + 1) * X * (1 - X)

Tactic:
· simp

Goal state after:
case calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
p :
  ∑ x ∈ Finset.range (n✝ + 1 + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * (n✝ + 1)) * X) * ↑x + ↑((n✝ + 1) ^ 2) * X ^ 2) * bernsteinPolynomial R (n✝ + 1) x =
    ↑((n✝ + 1) * (n✝ + 1 - 1)) * X ^ 2 + (1 - (2 * (n✝ + 1)) • X) * (n✝ + 1) • X + (n✝ + 1) ^ 2 • X ^ 2 * 1
⊢ ↑(n✝ + 1) * ↑(n✝ + 1 - 1) * X ^ 2 + (1 - 2 * ↑(n✝ + 1) * X) * (↑(n✝ + 1) * X) + ↑(n✝ + 1) ^ 2 * X ^ 2 * 1 =
    ↑(n✝ + 1) * X * (1 - X)
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
hφ : Continuous[_, inst✝¹] ⇑φ
⊢ Continuous[_, inst✝¹] ⇑φ.realContinuousMapOfNNReal

Tactic:
dsimp [realContinuousMapOfNNReal]

Goal state after:
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
hφ : Continuous[_, inst✝¹] ⇑φ
⊢ Continuous[_, inst✝¹] fun f ↦ φ f.toNNReal - φ (-f).toNNReal
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε

Tactic:
obtain ⟨⟨gK, hgKAK⟩, hgapprox⟩ :=
    @ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints _ _
    (isCompact_iff_compactSpace.mp hK) AK hsep (K.domRestrict f)
    (ContinuousOn.domRestrict (Continuous.continuousOn f.continuous)) ε pos

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK⟩ x - K.domRestrict (⇑f) x‖ < ε
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε
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
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖((x.toProd.1 • b)⋆ + b⋆ * x.toProd.2⋆) * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖

Tactic:
star_smul,

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
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖(x.toProd.1⋆ • b⋆ + b⋆ * x.toProd.2⋆) * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖
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✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
a✝ : ↑(characterSpace 𝕜 A)
⊢ { toFun := fun φ ↦ φ (a + b), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun φ ↦ φ a, continuous_toFun := ⋯ } + { toFun := fun φ ↦ φ b, continuous_toFun := ⋯ }) a✝

Tactic:
simp only [map_add, coe_mk, coe_add, Pi.add_apply]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ (∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')) ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x

Tactic:
hasBasis_nhdsSet (f x) |>.forall_iff ?h₁,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ (∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x

case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst✝] u
t : Set β
ht_open : IsOpen[inst✝] t
ht : f x ∩ u ⊆ t
⊢ f x ⊆ t ∪ uᶜ

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
hf : LowerHemicontinuousAt f x₀
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y₀ : β
hy₀ : y₀ ∈ f x₀
inst✝ : (𝓝 y₀).IsCountablyGenerated
U : ℕ → Set β
hU : ∀ (i : ℕ), y₀ ∈ U i ∧ IsOpen[inst✝¹] (U i)
hUbasis : (𝓝 y₀).HasAntitoneBasis fun i ↦ U i
hev : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, (f (x n) ∩ U k).Nonempty
g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
key : ∀ (n k : ℕ), k ≤ n → (f (x n) ∩ U k).Nonempty → (f (x n) ∩ U (g n)).Nonempty
y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀
hy : ∀ (n : ℕ), (f (x n) ∩ U (g n)).Nonempty → y n ∈ f (x n) ∩ U (g n)
⊢ ∀ (x_1 : ℕ), (f (x x_1) ∩ U 0).Nonempty → y x_1 ∈ f (x x_1)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ⊆ U ∧ ∀ i ∈ v, s ∈ {s | (s ∩ i).Nonempty}
⊢ s ⊆ U ∧ s.Nonempty ∧ ∀ ⦃x : Set α⦄, x ∈ v → (s ∩ x).Nonempty

Tactic:
by grind

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set α × Set (Set α)⦄,
    x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} →
      IsOpen[TopologicalSpace.vietoris α] {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}

Tactic:
intro ⟨V, u⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
⊢ (V, u) ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} →
    IsOpen[TopologicalSpace.vietoris α] {s | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀V : y₀ ∈ V
W : Set (β × β)
hW : W ∈ uniformity β
hWsub : ball y₀ W ⊆ V
U₁ : Set (β × β)
hU₁ : U₁ ∈ uniformity β
hU₁sym : SetRel.IsSymm U₁
hU₁comp : SetRel.comp U₁ U₁ ⊆ W
U : Set (β × β)
hU : U ∈ uniformity β
hUsym : SetRel.IsSymm U
hUcomp : SetRel.comp U U ⊆ U₁
hU_le_U₁ : U ⊆ U₁
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
z₀ : β
hz₀FN : z₀ ∈ F N x₀
hz₀y₀ : (y₀, z₀) ∈ U
U' : SetRel β β
hU'sub : id U' ⊆ U
hU'mem : U' ∈ uniformity β
hU'open : IsOpen[instTopologicalSpaceProd] U'
hmeet₀ : (F N x₀ ∩ ball z₀ U').Nonempty
hSmeet : ∀ᶠ (x : α) in 𝓝[s] x₀, (F N x ∩ ball z₀ U').Nonempty
x : α
⊢ (F N x ∩ ball z₀ U').Nonempty → x ∈ s → (f x ∩ V).Nonempty

Tactic:
⟨w, hwFN, hwball⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀V : y₀ ∈ V
W : Set (β × β)
hW : W ∈ uniformity β
hWsub : ball y₀ W ⊆ V
U₁ : Set (β × β)
hU₁ : U₁ ∈ uniformity β
hU₁sym : SetRel.IsSymm U₁
hU₁comp : SetRel.comp U₁ U₁ ⊆ W
U : Set (β × β)
hU : U ∈ uniformity β
hUsym : SetRel.IsSymm U
hUcomp : SetRel.comp U U ⊆ U₁
hU_le_U₁ : U ⊆ U₁
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
z₀ : β
hz₀FN : z₀ ∈ F N x₀
hz₀y₀ : (y₀, z₀) ∈ U
U' : SetRel β β
hU'sub : id U' ⊆ U
hU'mem : U' ∈ uniformity β
hU'open : IsOpen[instTopologicalSpaceProd] U'
hmeet₀ : (F N x₀ ∩ ball z₀ U').Nonempty
hSmeet : ∀ᶠ (x : α) in 𝓝[s] x₀, (F N x ∩ ball z₀ U').Nonempty
x : α
w : β
hwFN : w ∈ F N x
hwball : w ∈ ball z₀ U'
⊢ x ∈ s → (f x ∩ V).Nonempty
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : 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
⊢ (⋃₀ u, f '' u).2 ⊆ B ∧ ∀ U ∈ (⋃₀ u, f '' u).2, U ⊆ (⋃₀ u, f '' u).1

Tactic:
by grind

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

Goal state before:
pp: α : 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
⊢ s ∈ {s | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty}

Tactic:
by grind

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

Goal state before:
pp: case zero
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
⊢ spectralRadius 𝕜 a ^ 0 ≤ spectralRadius 𝕜 (a ^ 0)

pp: case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
n✝ : ℕ
⊢ spectralRadius 𝕜 a ^ (n✝ + 1) ≤ spectralRadius 𝕜 (a ^ (n✝ + 1))

Tactic:
· simp

Goal state after:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
n✝ : ℕ
⊢ spectralRadius 𝕜 a ^ (n✝ + 1) ≤ spectralRadius 𝕜 (a ^ (n✝ + 1))
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
k : 𝕜
h : ‖a‖ < ‖k‖
⊢ ‖a‖ * ‖1‖ < ‖k‖

Tactic:
norm_one,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
k : 𝕜
h : ‖a‖ < ‖k‖
⊢ ‖a‖ * 1 < ‖k‖
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      ∀ x_1 ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (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_1 ∈ v ∧ v ⊆ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}

Tactic:
intro u ⟨hu₁, hu₂⟩ s ⟨hs₁, hs₂⟩
    choose! f hfB hfU hfs using show ∀ U ∈ u, ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty by
      intro U hU
      obtain ⟨x, hxs, hxU⟩ := hs₂ U hU
      obtain ⟨W, hWB, hxW, hW⟩ := hB.exists_subset_of_mem_open hxU <| hu₂ U hU
      exact ⟨W, hWB, hW, x, hxs, hxW⟩
    rw [exists_mem_image]
    refine ⟨⟨⋃₀ u, f '' u⟩, ⟨isOpen_sUnion hu₂, hu₁.image _, by grind⟩, by grind,
      fun t ⟨ht₁, ht₂⟩ => ⟨ht₁, fun U hU => ?_⟩⟩
    rw [forall_mem_image] at ht₂
    grw [← hfU U hU]
    exact ht₂ hU

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

Goal state before:
pp: case zero
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
⊢ ‖a ^ 0‖₊ * r ^ 0 ≤ max 1 ‖1‖₊

pp: case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ max 1 ‖1‖₊

Tactic:
· simp

Goal state after:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ max 1 ‖1‖₊
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht✝ : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
u : Set α
hu : u.Finite
ht : t ⊆ ⋃ y ∈ u, {x | (x, y) ∈ U}
s : Set α
hs : s ⊆ t
⊢ u ∩ U.image s ∈ 𝒫 u

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ L ∈ s, (L \ ⋃₀ u).Nonempty
L : Set α
h : L ∈ s
⊢ L \ ⋃₀ u ⊆ K \ ⋃₀ u ∩ L

Tactic:
by grind

Goal state after: