mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
u : ℕ → α
hu : Monotone u
⊢ eVariationOn f (u '' Iic 0) = ∑ i ∈ Finset.range 0, edist (f (u i)) (f (u (i + 1)))

Tactic:
simp [Iic]

Goal state after:
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 μ
s : Set α
⊢ ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a ↦ μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)

Tactic:
by
  let t := toMeasurable μ s
  have A :
    ∀ᵐ x ∂μ.restrict s,
      Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x)) := by
    apply ae_mono restrict_le_self
    apply ae_tendsto_measure_inter_div_of_measurableSet
    exact measurableSet_toMeasurable _ _
  have B : ∀ᵐ x ∂μ.restrict s, t.indicator 1 x = (1 : ℝ≥0∞) := by
    refine ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) ?_
    filter_upwards [ae_restrict_mem (measurableSet_toMeasurable μ s)] with _ hx
    simp only [t, hx, Pi.one_apply, indicator_of_mem]
  filter_upwards [A, B] with x hx h'x
  rw [h'x] at hx
  apply hx.congr' _
  filter_upwards [v.eventually_filterAt_measurableSet x] with _ ha
  congr 1
  exact measure_toMeasurable_inter_of_sFinite ha _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, δ ∈ Ioo 0 ε := exists_between εpos

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
⊢ ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)

Tactic:
by
  rcases eq_empty_or_nonempty s with rfl | ⟨x₀, hx₀⟩
  · simpa using tendsto_const_nhds
  /- The variation is monotone, therefore it converges. If the limit were positive, say `ε`,
  then one would get variation `ε` between two points `x₀` and `x₁`. But also between two points
  `x₁` and `x₂`, and so on. Adding up these variations would be arbitrarily large, contradicting
  the finite variation of the function. -/
  apply tendsto_order.2 ⟨by simp, fun ε εpos ↦ ?_⟩
  obtain ⟨δ, δpos, hδ⟩ : ∃ δ, δ ∈ Ioo 0 ε := exists_between εpos
  by_contra! H
  have B (y) (hy : y ∈ s) : ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y') := by
    obtain ⟨y', hy', y'_mem⟩ : ∃ y', ε ≤ eVariationOn f (s ∩ Ici y') ∧ y' ∈ s ∩ Ici y :=
      (H.and_eventually (hL y hy)).exists
    obtain ⟨a, ha, b, hb, hab, h⟩ : ∃ a ∈ s ∩ Ici y', ∃ b ∈ s ∩ Ici y', a < b ∧
      δ < eVariationOn f ((s ∩ Ici y') ∩ Icc a b) :=
        exists_lt_eVariationOn_inter_Icc (hδ.trans_le hy')
    refine ⟨b, ⟨hb.1, le_trans y'_mem.2 hb.2⟩, ?_⟩
    have : Ici y' ∩ Icc a b = Icc a b := by grind
    rw [inter_assoc, this] at h
    exact h.le.trans (mono _ (by grind))
  choose! y y_mem le_y using B
  let v (n : ℕ) := y^[n] x₀
  have I n : v n ∈ s := by
    induction n with
    | zero => simpa [v] using hx₀
    | succ n ih =>
      simp only [Function.iterate_succ', Function.comp_apply, v]
      exact (y_mem _ ih).1
  have J (n : ℕ) : n * δ ≤ eVariationOn f s := calc
    n * δ
    _ = ∑ i ∈ Finset.range n, δ := by simp
    _ ≤ ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (v i) (v (i + 1))) := by
      gcongr with i hi
      simp only [Function.iterate_succ', Function.comp_apply, v]
      grind
    _ = eVariationOn f (s ∩ Icc (v 0) (v n)) := by
      apply eVariationOn.sum
      · apply monotone_nat_of_le_succ (fun n ↦ ?_)
        simp only [Function.iterate_succ', Function.comp_apply, v]
        exact (y_mem _ (I n)).2
      · grind
    _ ≤ eVariationOn f s := mono _ inter_subset_left
  have : Tendsto (fun (n : ℕ) ↦ n * δ) atTop (𝓝 (∞ * δ)) :=
    ENNReal.Tendsto.mul_const ENNReal.tendsto_nat_nhds_top (by simp)
  rw [ENNReal.top_mul δpos.ne'] at this
  have : ∞ ≤ eVariationOn f s := le_of_tendsto this (Eventually.of_forall J)
  simp only [BoundedVariationOn] at hf
  order

Goal state after:
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
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0) =
    0

Tactic:
dif_neg (not_and_of_not_right _ (not_and_of_not_left _ hf))

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
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 = 0
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : StarRing A
inst✝² : StarModule R A
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : ContinuousStar A
s : Subalgebra R A
⊢ (star s).topologicalClosure = star s.topologicalClosure

Tactic:
by
  suffices ∀ t : Subalgebra R A, (star t).topologicalClosure ≤ star t.topologicalClosure from
    le_antisymm (this s) (by simpa only [star_star] using Subalgebra.star_mono (this (star s)))
  exact fun t => (star t).topologicalClosure_minimal (Subalgebra.star_mono subset_closure)
    (isClosed_closure.preimage continuous_star)

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ k < 0 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n 0)) = 0

pp: case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
· rintro ⟨⟩

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
⊢ ↑(polynomialFunctions X) = Set.range ⇑(toContinuousMapOnAlgHom X)

Tactic:
by
  ext
  simp [polynomialFunctions]

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
⊢ ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X

Tactic:
have pderiv_true_y : pderiv true y = 0 := by rw [pderiv_X]; rfl

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
⊢ ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a

Tactic:
by_cases ha : p a
  · rw [cfcₙ_apply f a, cfcₙ_apply g a, ← map_sub, cfcₙ_apply ..]
    congr
  · simp [cfcₙ_apply_of_not_predicate a ha]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := ⋯
y : MvPolynomial Bool R := ⋯
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := ⋯
⊢ (MvPolynomial.aeval e) ((pderiv true) ((x + y) ^ n)) * X = n • X

Tactic:
rw [(pderiv true).leibniz_pow, (pderiv true).map_add, pderiv_true_x, pderiv_true_y]

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
⊢ (MvPolynomial.aeval e) (n • (x + y) ^ (n - 1) • (1 + 0)) * X = n • X
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
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2

Tactic:
have pderiv_true_y : pderiv true y = 0 := by rw [pderiv_X]; rfl

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
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f : C(↑s, 𝕜)
⊢ p f

Tactic:
refine closure (fun f hf => ?_) f
  rw [polynomialFunctions.starClosure_eq_adjoin_X] at hf
  induction hf using Algebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
    obtain (rfl | rfl) := hf
    all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
  | algebraMap r => exact const r
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x : E
⊢ (toWeakSpaceCLM 𝕜 E) x = (toWeakSpace 𝕜 E) x

Tactic:
by rfl

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 φ

Goal state after:
𝕜 : 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 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ characterSpace 𝕜 A ↔ φ ∈ {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ UpperHemicontinuous fun x ↦ {x}

Tactic:
simp [upperHemicontinuous_iff, upperHemicontinuousAt_iff]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
x : α
hf : UpperHemicontinuousAt f x
hg : UpperHemicontinuousAt g x
⊢ UpperHemicontinuousAt (fun x ↦ f x ∪ g x) x

Tactic:
rw [← upperHemicontinuousWithinAt_univ_iff] at hf hg ⊢
  exact hf.union hg

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

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

Tactic:
intro u ⟨hu₁, hu₂⟩

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})]
    {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
⊢ K ∈ closure[TopologicalSpace.vietoris α] {t | t.Finite ∧ t ⊆ s}

Tactic:
isTopologicalBasis.mem_closure_iff,

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
⊢ ∀ o ∈ (fun u ↦ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    K ∈ o → (o ∩ {t | t.Finite ∧ t ⊆ s}).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖k‖₊ = (↑‖k‖₊ ^ (n + 1)) ^ (1 / ↑(n + 1))

pp: case e'_4
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1)) = (↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊) ^ (1 / ↑(n + 1))

Tactic:
· rw [one_div, pow_rpow_inv_natCast]
    positivity

Goal state after:
case e'_4
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1)) = (↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊) ^ (1 / ↑(n + 1))
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x✝ :
  (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
⊢ Continuous[inst✝¹, TopologicalSpace.vietoris β] f

Tactic:
continuous_generateFrom_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x✝ :
  (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
⊢ ∀ s ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V},
    IsOpen[inst✝¹] (f ⁻¹' s)
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)

pp: case neg
𝕜 : 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:
case neg
𝕜 : 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)
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 ∈ spectrum ℝ ((algebraMap ℝ A) ↑t - a)
⊢ ↑‖x‖₊ ≤ ↑t

Tactic:
← spectrum.singleton_sub_eq

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
x : ℝ
hx : x ∈ {↑t} - spectrum ℝ a
⊢ ↑‖x‖₊ ≤ ↑t
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ (spectralRadius ℂ a).toReal = ‖a‖

Tactic:
simp [ha.spectralRadius_eq_nnnorm]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
heq : (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x ↦ x ^ 2) ∘ fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ ↑‖a‖₊ ^ 2 = spectralRadius ℂ (a⋆ * a)

Tactic:
rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Continuous[_, TopologicalSpace.vietoris (α × β)] (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2)

Tactic:
continuous_generateFrom_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ ∀
    s ∈
      powerset '' {U | IsOpen[instTopologicalSpaceProd] U} ∪
        (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[instTopologicalSpaceProd] V},
    IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' s)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
V : Set α
W : Set β
hV : IsOpen[inst✝¹] V
hW : IsOpen[inst✝] W
hxV : x ∈ V
hyW : y ∈ W
hVW : V ×ˢ W ⊆ U
⊢ ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U, IsOpen t ∧ (K, L) ∈ t

Tactic:
grw [preimage_ofPred_eq, ← hVW]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
V : Set α
W : Set β
hV : IsOpen[inst✝¹] V
hW : IsOpen[inst✝] W
hxV : x ∈ V
hyW : y ∈ W
hVW : V ×ˢ W ⊆ U
⊢ ∃ t ⊆ {a | ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) a ∩ V ×ˢ W).Nonempty}, IsOpen t ∧ (K, L) ∈ t
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
⊢ ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C

Tactic:
obtain ⟨K : Set α, hK₁, hK₂⟩ := mem_cocompact.mp
    (tendsto_def.mp (zero_at_infty (f : F)) _ (closedBall_mem_nhds (0 : β) zero_lt_one))
  obtain ⟨C, hC⟩ := (hK₁.image (map_continuous f)).isBounded.subset_closedBall (0 : β)
  refine ⟨max C 1 + max C 1, fun x y => ?_⟩
  have : ∀ x, f x ∈ closedBall (0 : β) (max C 1) := by
    intro x
    by_cases hx : x ∈ K
    · exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)
    · exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)
  exact (dist_triangle (f x) 0 (f y)).trans
    (add_le_add (mem_closedBall.mp <| this x) (mem_closedBall'.mp <| this y))

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ 𝓝 0 ∧ AbsConvex 𝕜 s) id

Tactic:
by
  refine
    (LocallyConvexSpace.convex_basis_zero 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs =>
      ⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩
  refine ⟨convexHull 𝕜 (balancedCore 𝕜 s), ?_, convexHull_min (balancedCore_subset s) hs.2⟩
  refine ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull 𝕜 _), ?_⟩
  refine ⟨(balancedCore_balanced s).convexHull, ?_⟩
  exact convex_convexHull 𝕜 (balancedCore 𝕜 s)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual 𝕜 ↥p
⊢ ?m.28

Tactic:
refine Module.Dual.exists_continuous_extension_of_le_seminorm p f
      (show Continuous (‖f‖₊ • (normSeminorm 𝕜 E)) from ?_) fun x => f.le_opNorm x

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual 𝕜 ↥p
⊢ Continuous ⇑(‖f‖₊ • normSeminorm 𝕜 E)
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ slope f a ((lineMap a b) r) ≤ slope f a b ↔ slope f a ((lineMap a b) r) ≤ slope f ((lineMap a b) r) b

Tactic:
←
    lineMap_slope_lineMap_slope_lineMap f a b r,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ slope f a ((lineMap a b) r) ≤ (lineMap (slope f ((lineMap a b) r) b) (slope f a ((lineMap a b) r))) r ↔
    slope f a ((lineMap a b) r) ≤ slope f ((lineMap a b) r) b