mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r) ∈ R[(toContinuousMapOnAlgHom s) X]

pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf : (toContinuousMapOnAlgHom s) f ∈ R[(toContinuousMapOnAlgHom s) X]
hg : (toContinuousMapOnAlgHom s) g ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (f + g) ∈ R[(toContinuousMapOnAlgHom s) X]

pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ (n + 1)) ∈ R[(toContinuousMapOnAlgHom s) X]

Tactic:
· rw [Polynomial.C_eq_algebraMap, AlgHomClass.commutes]
    exact Subalgebra.algebraMap_mem _ r

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf : (toContinuousMapOnAlgHom s) f ∈ R[(toContinuousMapOnAlgHom s) X]
hg : (toContinuousMapOnAlgHom s) g ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (f + g) ∈ R[(toContinuousMapOnAlgHom s) X]

case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ (n + 1)) ∈ R[(toContinuousMapOnAlgHom s) 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
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 + (pderiv true) y)) * X = n • X

Tactic:
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.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L

Tactic:
dsimp only [Set.SeparatesPointsStrongly] at sep

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: case refine_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ 0 ≤ x

Tactic:
obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx
    exact coe_nonneg x

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
x✝¹ : 𝕜 × WeakBilin B
x✝ : F
⊢ (x✝¹.1 • ((fun x y ↦ (B x) y) ∘ Prod.snd) x✝¹) x✝ = ((fun x y ↦ (B x) y) ∘ fun p ↦ p.1 • p.2) x✝¹ x✝

Tactic:
simp only [Function.comp_apply, Pi.smul_apply, map_smulₛₗ, RingHom.id_apply, LinearMap.smul_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 β
⊢ UpperHemicontinuousWithinAt f s x ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x

Tactic:
simp_rw [upperHemicontinuousWithinAt_iff]
  rw [hasBasis_nhdsSet (f x) |>.forall_iff ?h₁, hasBasis_nhdsSet (f x) |>.forall_iff ?h₂]
  case h₂ =>
    intro s t hst
    gcongr
  case h₁ =>
    intro s t hst
    gcongr
  refine forall₂_congr fun u ⟨hu, hfu⟩ ↦ ?_
  simp [hu.mem_nhdsSet, eventually_iff, Iic]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
t : Set α
ht : IsOpen[inst✝] t
hne : ((fun x ↦ {x}) x ∩ t).Nonempty
x' : α
hx' : x' ∈ t
⊢ IsOpen[inst✝] t ∧ ({x'} ∩ t).Nonempty

Tactic:
exact ⟨ht, Set.singleton_inter_nonempty.mpr hx'⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClopen (𝒫 ∅)

Tactic:
exact ⟨isClosed_empty.powerset_vietoris, isOpen_empty.powerset_vietoris⟩

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
⊢ ∃ y, (∀ᶠ (n : ℕ) in atTop, y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)

Tactic:
classical
  obtain ⟨U, hU, hUbasis⟩ := (nhds_basis_opens y₀).exists_antitone_subbasis
  have hev (k) : ∀ᶠ n in atTop, (f (x n) ∩ U k).Nonempty :=
    hx.eventually <| (lowerHemicontinuousAt_iff.mp hf) (U k) (hU k).2 ⟨y₀, hy₀, (hU k).1⟩
  -- For each `n`, find the largest `k ≤ n` where `U k` intersects `f (x n)`.
  let g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
  have key (n k) (hkn : k ≤ n) (hk : (f (x n) ∩ U k).Nonempty) : (f (x n) ∩ U (g n)).Nonempty :=
    Nat.findGreatest_spec (P := fun k ↦ (f (x n) ∩ U k).Nonempty) hkn hk
  -- Define `y n` to be some element of `f (x n) ∩ U (g n)` (or be arbitrary)
  let y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀
  have hy (n) (h : (f (x n) ∩ U (g n)).Nonempty) : y n ∈ f (x n) ∩ U (g n) := by
    simpa only [y, dif_pos h] using h.some_mem
  refine ⟨y, (hev 0).mono (by grind), ?_⟩
  -- Have to show for all `k`, eventually, all `y n ∈ U k`.
  rw [hUbasis.tendsto_right_iff]
  intro k _
  filter_upwards [hev k, eventually_ge_atTop k] with n hk hkn
  exact hUbasis.antitone (Nat.le_findGreatest hkn hk) (hy n (key n k hkn hk)).2

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : ⋂ i, {C | ↑C ⊆ F i} ⊆ {⊥} → ∃ u, ⋂ i ∈ u, {C | ↑C ⊆ F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅

Tactic:
← Set.ofPred_forall,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : {x | ∀ (i : ι), ↑x ⊆ F i} ⊆ {⊥} → ∃ u, {x | ∀ i ∈ u, ↑x ⊆ F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case neg.inl
α : 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, (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
⊢ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ 𝒫 U ∪ ⋃₀ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' T)

Tactic:
← sdiff_subset_iff,

Goal state after:
case neg.inl
α : 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, (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
⊢ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} \ 𝒫 U ⊆ ⋃₀ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' T)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σ 𝕜 a
ha : p a
⊢ ‖x‖ ≤ ‖a‖

Tactic:
simpa only [cfc_id 𝕜 a] using! norm_apply_le_norm_cfc (id : 𝕜 → 𝕜) a hx

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    ((algebraMap 𝕜 A) k - a)
H₂ : HasDerivAt (fun k ↦ (algebraMap 𝕜 A) k - a) 1 k
⊢ HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

Tactic:
simpa [resolvent, sq, hk.unit_spec, ← Ring.inverse_unit hk.unit] using! H₁.comp_hasDerivAt k H₂

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

Goal state before:
pp: A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
x✝ : ℕ
⊢ ENNReal.ofReal (‖a ^ x✝‖ ^ (1 / ↑x✝)) = ↑‖a ^ x✝‖₊ ^ (1 / ↑x✝)

Tactic:
rw [← ofReal_rpow_of_nonneg (norm_nonneg _) _, ← coe_nnnorm, coe_nnreal_eq]

Goal state after:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
x✝ : ℕ
⊢ 0 ≤ 1 / ↑x✝
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 (Set α)⦄,
    x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} →
      ∀ x_1 ∈ SetLike.coe ⁻¹' {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty},
        ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
          x_1 ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}

Tactic:
· intro ⟨V, u⟩ ⟨hV, hu, huB, huV⟩ K ⟨hKV, hKu⟩
    dsimp only at *
    obtain ⟨w, hwB, hwV⟩ := hB.open_eq_sUnion hV
    rw [hwV] at hKV
    replace hwV := hwV.symm.subset
    wlog hwK : ∀ W ∈ w, ((K : Set α) ∩ W).Nonempty generalizing w
    · refine this {W ∈ w | (↑K ∩ W).Nonempty} (fun x hx => ?_) (by grind) (by grind) (by grind)
      obtain ⟨W, hWw, hxW⟩ := mem_sUnion.mp (hKV hx)
      exact mem_sUnion_of_mem hxW ⟨hWw, x, hx, hxW⟩
    wlog hw : w.Finite generalizing w
    · rw [sUnion_eq_biUnion] at hKV
      obtain ⟨w', _⟩ := K.isCompact.elim_finite_subcover_image (fun W hW => hB.isOpen (hwB hW)) hKV
      apply this w' <;> grind [sUnion_eq_biUnion]
    wlog huw : u ⊆ w generalizing w
    · apply this (u ∪ w) <;> grind [sUnion_union, Finite.union]
    rw [exists_mem_image]
    exists w
    #adaptation_note /-- Before leanprover/lean4#13166, this was just `grind`.
    The new canonicalizer using `isDefEq` less,
    and so does not unify as many of the conditions that `grind` wants to case split on.
    Alternatively `simp; grind` also works here. -/
    grind (splits := 12)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus

Goal state before:
pp: E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C
⊢ ∃ C', ∀ (i : ι), ‖g i‖ ≤ C'

Tactic:
show (∃ C, ∀ i, ‖g i‖ ≤ C) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 5 2

Goal state after:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C
⊢ UniformEquicontinuous (DFunLike.coe ∘ g)
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) = 0

Tactic:
rw [ihn, ihn, midpoint_self]

Goal state after:
case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.right.C

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.left.C
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) = 1

Tactic:
rw [ihn, ihn, midpoint_self]

Goal state after:
case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.right.U

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.left.U
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
W : Type u_3
Q : Type u_4
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : P := Classical.arbitrary P
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑(AddMonoidHom.ofMapMidpoint ℝ ℝ (⇑(AffineEquiv.vaddConst ℝ (f c)).symm ∘ f ∘ ⇑(AffineEquiv.vaddConst ℝ c)) ⋯ ⋯)

Tactic:
apply_rules [Continuous.vadd, Continuous.vsub, continuous_const, hfc.comp, continuous_id]

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

Goal state before:
pp: 𝕜 : Type u_5
F : Type u_7
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
f : WeakDual ℝ F
x : F
⊢ re ((extendRCLikeL f) x) = f x

Tactic:
by
  simp [extendRCLikeL_apply_apply]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
let P : Set X → Set X → Prop := fun C _ => IsCompact C

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Set X → Prop := fun C x ↦ IsCompact C
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Set X → Prop := fun C x ↦ IsCompact C
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
set c : Urysohns.CU P :=
  { C := k
    U := tᶜ
    P_C_U := k_comp
    closed_C := k_closed
    open_U := ht.isOpen_compl
    subset := kt
    hP := by
      rintro c u - c_comp u_open cu
      rcases exists_compact_closed_between c_comp u_open cu with ⟨k, k_comp, k_closed, ck, ku⟩
      have A : closure (interior k) ⊆ k :=
        (IsClosed.closure_subset_iff k_closed).2 interior_subset
      refine ⟨interior k, isOpen_interior, ck, A.trans ku, c_comp,
        k_comp.of_isClosed_subset isClosed_closure A⟩ }

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Set X → Prop := fun C x ↦ IsCompact C
c : Urysohns.CU P := { C := k, U := tᶜ, P_C_U := k_comp, closed_C := k_closed, open_U := ⋯, subset := kt, hP := ⋯ }
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
have S x : Summable (fun n ↦ u n * f n x) := Summable.of_nonneg_of_le
      (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1) (fun n ↦ I n x) u_sum

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n
S : ∀ (x : X), Summable fun n ↦ u n * (f n) x
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
f g : α →ᵤ[𝔖] β
C : ℝ≥0∞
⊢ edist f g ≤ C ↔ ∀ x ∈ ⋃₀ 𝔖, edist ((toFun 𝔖) f x) ((toFun 𝔖) g x) ≤ C

Tactic:
simp_rw [edist_def, iSup₂_le_iff]

Goal state after:
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 : 0 ≤ a
⊢ ∀ x ∈ spectrum ℝ ↑a, 0 ≤ x

Tactic:
let _ := CStarAlgebra.spectralOrder A⁺¹

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x✝ : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
⊢ ∀ x ∈ spectrum ℝ ↑a, 0 ≤ x
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : SeparatelyContinuousMul α
l : Filter α
hl : l.IsApproximateUnit
⊢ l ≤ 𝓝 1

Tactic:
by simpa using! hl.tendsto_mul_left 1

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

Goal state before:
pp: case frequently
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(cfcHom ⋯) ((f - g).comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ })‖ ≤ ε

Tactic:
isometry_cfcHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcHom (ha' x)))

Goal state after:
case frequently
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(f - g).comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ }‖ ≤ ε
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ ↑⋯.unit⁻¹ ≤ ↑⋯.unit⁻¹

Tactic:
exact CStarAlgebra.inv_le_inv (Units.isStrictlyPositive_iff.mp apos) hab

Goal state after: