mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})
B : ν (s ∩ f ⁻¹' {∞}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ t ^ n * t ^ (-1) < t ^ n

Tactic:
conv_rhs => rw [← mul_one (t ^ n)]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})
B : ν (s ∩ f ⁻¹' {∞}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ t ^ n * t ^ (-1) < t ^ n * 1
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (0 + edist (f x) l))
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))

Tactic:
simp only [zero_add] at H

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
⊢ Tendsto (fun x_1 ↦ eVariationOn f (s ∩ Ico x_1 x)) (𝓝[s ∩ Iio x] x) (𝓝 0)

Tactic:
exact (hf.tendsto_eVariationOn_Ico_zero x).mono_left (nhdsWithin_mono _ inter_subset_left)

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

Goal state before:
pp: case refine_1
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
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x ↦ x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ Continuous[_, inst✝⁴] ⇑φ

pp: case refine_2
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
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x ↦ x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ φ (ContinuousMapZero.id (σₙ R ((cfcₙHom ha) f))) = (cfcₙHom ha) f

Tactic:
· refine (cfcₙHom_continuous ha).comp <| continuous_induced_rng.mpr ?_
    exact f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom

Goal state after:
case refine_2
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
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x ↦ x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ φ (ContinuousMapZero.id (σₙ R ((cfcₙHom ha) f))) = (cfcₙHom ha) f
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
ha : p a
⊢ cfcₙ f a = (cfcₙHom ha) (mkD ((σₙ R a).domRestrict f) 0)

Tactic:
by_cases f_cont : ContinuousOn f (quasispectrum R a)
  · by_cases f_zero : f 0 = 0
    · rw [cfcₙ_apply f a, mkD_of_continuousOn f_cont f_zero]
    · rw [cfcₙ_apply_of_not_map_zero a f_zero, mkD_of_not_zero, map_zero]
      exact f_zero
  · rw [cfcₙ_apply_of_not_continuousOn a f_cont, mkD_of_not_continuousOn f_cont, map_zero]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hs : IsOpen[inst✝¹] s
⊢ eVariationOn (Function.leftLim f) s ≤ eVariationOn f s

Tactic:
by
  apply eVariationOn_le_of_mapClusterPt (fun x hx ↦ ?_)
  rw [IsOpen.nhdsWithin_eq hs hx]
  exact (mapClusterPt_leftLim f x).mono nhdsWithin_le_nhds

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) -
      Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) (ν + 1))) =
    0

Tactic:
rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]

Goal state after:
case succ.succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) = 0
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ Tendsto (fun n ↦ bernsteinApproximation n f) atTop (𝓝 f)

Tactic:
suffices ∀ U ∈ 𝓝 (0 : E), Convex ℝ U →
      ∀ᶠ n in atTop, ∀ x : I, gauge U (bernsteinApproximation n f x - f x) < 1 by
    rw [(LocallyConvexSpace.convex_basis_zero ℝ E).uniformity_of_nhds_zero_swapped
      |>.compactConvergenceUniformity_of_compact |> nhds_basis_uniformity |>.tendsto_right_iff]
    rintro U ⟨hU₀, hcU⟩
    filter_upwards [this U hU₀ hcU] with n hn x
    exact setOfPred_gauge_lt_one_subset_self hcU (mem_of_mem_nhds hU₀) (absorbent_nhds_zero hU₀)
      (hn x)

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ ∀ U ∈ 𝓝 0, Convex ℝ U → ∀ᶠ (n : ℕ) in atTop, ∀ (x : ↑I), gauge U ((bernsteinApproximation n f) x - f x) < 1
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
hn₀ : n ≠ 0
x : ↑I
S : Finset (Fin (n + 1)) := {k | dist k/ₙ x < δ}
⊢ ∑ k, gauge U ((bernstein n ↑k) x • (f k/ₙ - f x)) = ∑ k, (bernstein n ↑k) x * gauge U (f k/ₙ - f x)

Tactic:
simp only [gauge_smul_of_nonneg, bernstein_nonneg, smul_eq_mul]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
⊢ φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)

Tactic:
convert! h using 1

Goal state after:
case e'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
⊢ φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))

case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
⊢ ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
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
⊢ Function.Injective realContinuousMapOfNNReal

Tactic:
intro φ ψ h

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
⊢ φ = ψ
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_2
𝕜 : 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
a : E
⊢ ∀ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, a_1 ≤ ‖a‖₊

Tactic:
rintro - ⟨x, hx, rfl⟩

Goal state after:
case refine_2
𝕜 : 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
a x : E
hx : x ∈ Metric.closedBall 0 1
⊢ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) x ≤ ‖a‖₊
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_3
𝕜 : 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
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, r < a_1

Tactic:
have ha : 0 < ‖a‖₊ := hr.pos

Goal state after:
case refine_3
𝕜 : 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
a : E
r : NNReal
hr : r < ‖a‖₊
ha : 0 < ‖a‖₊
⊢ ∃ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, r < a_1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
⊢ Function.Injective realContinuousMapZeroOfNNReal

Tactic:
intro φ ψ h

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
⊢ φ = ψ
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case neg
𝕜 : 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
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : 0 < ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖
this : ‖((splitMul 𝕜 E) x).2‖ * ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖ * ‖((splitMul 𝕜 E) x).2‖
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖

Tactic:
simp only [Unitization.splitMul_apply, Unitization.snd_star,
          Unitization.fst_star] at this

Goal state after:
case neg
𝕜 : 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
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : 0 < ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖
this :
  ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ *
      ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖ *
      ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this✝² : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
this✝¹ :
  ∀ (ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A),
    Continuous[_, inst✝⁴] ⇑ξ →
      let ξ' :=
        ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 });
      Continuous[_, inst✝⁴] ⇑ξ' ∧ ξ' (ContinuousMapZero.id s') = ξ (ContinuousMapZero.id s)
hφ' :
  Continuous[_, inst✝⁴]
    ⇑(φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hφ_id :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    φ (ContinuousMapZero.id s)
hψ' :
  Continuous[_, inst✝⁴]
    ⇑(ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hψ_id :
  (ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    ψ (ContinuousMapZero.id s)
hs' : CompactSpace ↑s'
this✝ : ContinuousMapZero.UniqueHom ℝ A
h' :
  φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }) =
    ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })
this :
  (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' }) =
    NonUnitalStarAlgHom.id ℝ C(↑s, ℝ)₀
h'' : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
⊢ φ = ψ

Tactic:
exact NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective h''

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✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ { toFun := fun φ ↦ φ (a * b), continuous_toFun := ⋯ } =
    { toFun := fun φ ↦ φ a, continuous_toFun := ⋯ } * { toFun := fun φ ↦ φ b, continuous_toFun := ⋯ }

Tactic:
ext; simp only [map_mul, coe_mk, coe_mul, Pi.mul_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 β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x

Tactic:
intro s t hst
    gcongr

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 β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
intro s t hst
    gcongr

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
⊢ s ∈ {s | (s ∩ U).Nonempty} → {s | (s ∩ U).Nonempty} ∈ 𝓝 s

Tactic:
⟨x, hx₁, hx₂⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
hx₂ : x ∈ U
⊢ {s | (s ∩ U).Nonempty} ∈ 𝓝 s
Module: Mathlib.Topology.Sets.VietorisTopology

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

Tactic:
refine subset_antisymm ?_ (fun K hKs => ?_)
  · rw [isClosed_closure.powerset_vietoris.closure_subset_iff]
    exact fun K ⟨_, h⟩ => h.trans subset_closure
  · 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.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 : {⊥} ⊆ {⊥} → ∃ u, {x | ↑x ⊆ ⋂ i ∈ u, F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅

Tactic:
obtain ⟨s, hs⟩ := this .rfl

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 : {⊥} ⊆ {⊥} → ∃ u, {x | ↑x ⊆ ⋂ i ∈ u, F i} ⊆ {⊥}
s : Finset ι
hs : {x | ↑x ⊆ ⋂ i ∈ s, F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case e'_4
𝕜 : 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
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x ↦ ‖f x‖) '' σ 𝕜 a) ((fun x ↦ ‖f x‖) x)
⊢ ‖(cfcHom ha) { toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ }‖ = (fun x ↦ ‖f x‖) x

Tactic:
norm_cfcHom a _

Goal state after:
case e'_4
𝕜 : 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
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x ↦ ‖f x‖) '' σ 𝕜 a) ((fun x ↦ ‖f x‖) x)
⊢ ‖{ toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ }‖ = (fun x ↦ ‖f x‖) x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
𝕜 : 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ c ∈ upperBounds ((fun x ↦ ‖f x‖) '' σ 𝕜 a)

Tactic:
rintro - ⟨x, hx, rfl⟩

Goal state after:
case inr
𝕜 : 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun x ↦ ‖f x‖) x ≤ c