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

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

Tactic:
congr 1; simp only [← natCast_mul, push_cast]
    cases k <;> · simp; ring

Goal state after:
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
a✝ : Nontrivial A
⊢ ‖((addEquiv 𝕜 A) x).2‖ ≤ 2 * max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖

Tactic:
rw [two_mul]

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
a✝ : Nontrivial A
⊢ ‖((addEquiv 𝕜 A) x).2‖ ≤
    max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖ +
      max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
⊢ f ∈ A.topologicalClosure

Tactic:
let f_re : C(X, ℝ) := (⟨RCLike.re, RCLike.reCLM.continuous⟩ : C(𝕜, ℝ)).comp f

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
⊢ f ∈ A.topologicalClosure
Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1

Goal state before:
pp: case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)

Tactic:
apply (norm_add_le _ _).trans

Goal state after:
case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 • y.ofLp.toProd.2‖ + ‖y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1

Goal state before:
pp: case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖

Tactic:
apply (norm_add_le _ _).trans

Goal state after:
case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ + ‖x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
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✝ f : C(↑s, 𝕜)₀
hf : f ∈ adjoin 𝕜 {ContinuousMapZero.id s}
⊢ p f

Tactic:
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: α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed[TopologicalSpace.vietoris α] (𝒫 F)

Tactic:
simp_rw [powerset, ← isOpen_compl_iff, compl_ofPred, ← inter_compl_nonempty_iff]
  exact isOpen_inter_nonempty_of_isOpen h.isOpen_compl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst✝ : U.IsSymm
⊢ (hausdorffEntourage U).inv = hausdorffEntourage U

Tactic:
inv_hausdorffEntourage,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst✝ : U.IsSymm
⊢ hausdorffEntourage U.inv = hausdorffEntourage U
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:
· rw [isTopologicalBasis.mem_closure_iff, forall_mem_image]
    rintro u ⟨hu₁, hu₂⟩ ⟨ht₁, ht₂⟩
    choose x hxU hxs using fun U : u => show (↑U ∩ s).Nonempty by
      obtain ⟨x, hxK, hxV⟩ := ht₂ U U.prop
      exact mem_closure_iff.mp (hKs hxK) _ (hu₂ _ U.prop) hxV
    have := hu₁.to_subtype
    exact ⟨range x, ⟨range_subset_iff.mpr fun V => mem_sUnion_of_mem (hxU V) V.prop,
      fun U hU => ⟨x ⟨U, hU⟩, mem_range_self _, hxU ⟨U, hU⟩⟩⟩,
      finite_range _, range_subset_iff.mpr hxs⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ Continuous[Pi.topologicalSpace, TopologicalSpace.vietoris α] range

Tactic:
simp_rw [continuous_iff, powerset, preimage_ofPred_eq, range_subset_iff, 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.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
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
⊢ f ≤ 𝓝 L

Tactic:
nhds_eq_comap_uniformity'

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
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
⊢ f ≤ Filter.comap (fun y ↦ (y, L)) (𝓤 (Compacts α))
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : 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
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : x ∈ ↑K
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
⊢ x ∈ U.preimage ↑L

Tactic:
have hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U)) := .of_inf_right hy

Goal state after:
case left
α : 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
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : x ∈ ↑K
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U))
⊢ x ∈ U.preimage ↑L
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
obtain ⟨x, hx⟩ := K.nonempty

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ ↑K
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKV : ↑K ⊆ V
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hwB : w ⊆ B
hwV : V = ⋃₀ w
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
hwV

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : V = ⋃₀ w
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ ↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊

Tactic:
refine congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (this x) |>.symm.trans_le <| le_iSup₂ (α := ℝ≥0∞) _ ?_

Goal state after:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ (algebraMap 𝕜₁ 𝕜₂) x ∈ spectrum 𝕜₂ a
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ (absConvexHull 𝕜) s ≠ ∅ ↔ s ≠ ∅

Tactic:
Ne,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ ¬(absConvexHull 𝕜) s = ∅ ↔ s ≠ ∅
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
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
⊢ (𝓝 0).HasAntitoneBasis v

Tactic:
refine ⟨hu_basis.to_hasBasis ?_ ?_,
      fun _ _ hij ↦ absConvexHull_mono (interior_mono (hu_basis.antitone hij))⟩

Goal state after:
case refine_1
𝕜 : 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
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
⊢ ∀ (i : ℕ), True → ∃ i', True ∧ v i' ⊆ u i

case refine_2
𝕜 : 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
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ u i ⊆ v i'
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case refine_2
𝕜 : 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
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ u i ⊆ v i'

Tactic:
· intro n _
      obtain ⟨m, hm⟩ := hu_basis.mem_iff.mp (isOpen_interior.mem_nhds (hu_zero n))
      exact ⟨m, trivial, hm.trans subset_absConvexHull⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := finBasis 𝕜 ↥(↑f).range
e : ↥(↑f).range ≃L[𝕜] Fin (finrank 𝕜 ↥(↑f).range) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(↑f).range) → ↥S →L[𝕜] 𝕜 :=
  fun i ↦ LinearMap.toContinuousLinearMap (b.coord i) ∘SL f.codRestrict (↑f).range ⋯
⊢ ∃ g, f = g ∘SL S.subtypeL

Tactic:
choose gi hgf using fun i ↦ StrongDual.exists_extension S (fi i)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := finBasis 𝕜 ↥(↑f).range
e : ↥(↑f).range ≃L[𝕜] Fin (finrank 𝕜 ↥(↑f).range) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(↑f).range) → ↥S →L[𝕜] 𝕜 :=
  fun i ↦ LinearMap.toContinuousLinearMap (b.coord i) ∘SL f.codRestrict (↑f).range ⋯
gi : Fin (finrank 𝕜 ↥(↑f).range) → StrongDual 𝕜 E
hgf : ∀ (i : Fin (finrank 𝕜 ↥(↑f).range)) (x : ↥S), (gi i) ↑x = (fi i) x
⊢ ∃ g, f = g ∘SL S.subtypeL
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r r' : k
h : a < b
⊢ (lineMap a b) r ≤ (lineMap a b) r' ↔ r ≤ r'

Tactic:
by
  simp only [lineMap_apply_module']
  rw [add_le_add_iff_right, smul_le_smul_iff_of_pos_right (sub_pos.mpr h)]

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

Goal state before:
pp: case refine_3
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, 0 < g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, 0 < g₂ x
⊢ ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ s₁ ∪ s₂, 0 < g' x

Tactic:
refine ⟨g₁ + g₂, ?_, fun x hx => ?_⟩

Goal state after:
case refine_3.refine_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, 0 < g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, 0 < g₂ x
⊢ (↑(algebraMapCLM ℝ≥0 𝕜)).comp (g₁ + g₂) ∈ I

case refine_3.refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, 0 < g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, 0 < g₂ x
x : X
hx : x ∈ s₁ ∪ s₂
⊢ 0 < (g₁ + g₂) x
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : ∃ f ∈ I, f x ≠ 0
⊢ ∃ t_1 ∈ nhdsWithin x t, ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t_1, 0 < g' x

Tactic:
obtain ⟨g, hI, hgx⟩ := hx

Goal state after:
case refine_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : g x ≠ 0
⊢ ∃ t_1 ∈ nhdsWithin x t, ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t_1, 0 < g' x
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (⇑f) 0 {x}
fy : Set.EqOn (⇑f) 1 {y}
⊢ (continuousMapEval X 𝕜) x ≠ (continuousMapEval X 𝕜) y

Tactic:
DFunLike.ne_iff

Goal state after:
case refine_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (⇑f) 0 {x}
fy : Set.EqOn (⇑f) 1 {y}
⊢ ∃ a, ((continuousMapEval X 𝕜) x) a ≠ ((continuousMapEval X 𝕜) y) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
x✝ : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this✝ : StarOrderedRing (Unitization ℂ A)
this :
  (Unitization.inrNonUnitalStarAlgHom ℂ A) a ∈
    AddSubmonoid.map (Unitization.inrNonUnitalStarAlgHom ℂ A) (AddSubmonoid.closure (Set.range fun s ↦ star s * s))
⊢ ↑a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)

Tactic:
AddMonoidHom.map_mclosure,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
x✝ : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this✝ : StarOrderedRing (Unitization ℂ A)
this :
  (Unitization.inrNonUnitalStarAlgHom ℂ A) a ∈
    AddSubmonoid.closure (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) '' Set.range fun s ↦ star s * s)
⊢ ↑a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)