mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg
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
f_cont : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ f a = (cfcₙHom ha) (mkD ((σₙ R a).domRestrict f) 0)

Tactic:
cfcₙ_apply_of_not_continuousOn a f_cont,

Goal state after:
case neg
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
f_cont : ¬ContinuousOn f (σₙ R a)
⊢ 0 = (cfcₙHom ha) (mkD ((σₙ R a).domRestrict f) 0)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
⊢ 0 ≤ cfc f a

Tactic:
by
  by_cases hf : ContinuousOn f (spectrum R a)
  · simpa using cfc_mono h
  · simp only [cfc_apply_of_not_continuousOn _ hf, le_rfl]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
⊢ cfc f a ≤ 0

Tactic:
by
  by_cases hf : ContinuousOn f (spectrum R a)
  · simpa using cfc_mono h
  · simp only [cfc_apply_of_not_continuousOn _ hf, le_rfl]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 1
⊢ 0 ≤ 1

Tactic:
by simp

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 g : R → R
a : A
⊢ Commute 0 (cfcₙ g a)

Tactic:
by simp

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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ Commute ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }) 0

Tactic:
by simp

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 α
inst✝¹ : CompleteSpace E
inst✝ : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim (Function.leftLim f) x))
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x

Tactic:
leftLim_leftLim (hf.tendsto_leftLim x)

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
E : Type u_2
inst✝⁴ : PseudoEMetricSpace E
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : CompleteSpace E
inst✝ : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim f x))
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : p a
⊢ (algebraMap R A) r ≤ a ↔ ∀ x ∈ spectrum R a, r ≤ x

Tactic:
by
  nth_rw 1 [← cfc_id R a]
  exact algebraMap_le_cfc_iff id r a

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

Goal state before:
pp: a b : ℝ
⊢ a ∈ Set.univ

Tactic:
by simp

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

Goal state before:
pp: a b : ℝ
⊢ b ∈ Set.univ

Tactic:
by simp

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 ν : ℕ
⊢ k + 1 ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k + 1] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν ↦ bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ LinearIndependent ℚ fun ν ↦ bernsteinPolynomial ℚ n ↑ν

Tactic:
| succ k ih =>

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (X + (1 - X)) ^ n = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n ν : ℕ
x : ↑I
⊢ (bernstein n ν) x = ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
by
  dsimp [bernstein, Polynomial.toContinuousMapOn, Polynomial.toContinuousMap, bernsteinPolynomial]
  simp

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✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
⊢ Filter.comap ((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (𝓤 C(Unit, R)) = ⊤

Tactic:
convert! Filter.comap_const_of_mem this with ⟨u, v⟩

Goal state after:
case e'_2.e'_3
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).1 = 0

case e'_2.e'_4
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).2 = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

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

Tactic:
simpa only [cfcₙHom_id ha] using! cfcHom_id ha

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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ f a = cfc f a

pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : ¬p a
⊢ cfcₙ f a = cfc f a

Tactic:
· have hf' := hf.mono <| spectrum_subset_quasispectrum R a
    rw [cfc_apply f a ha hf', cfcₙ_apply f a hf, cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom]
    dsimp only [NonUnitalStarAlgHom.comp_apply,
      NonUnitalStarAlgHom.coe_coe, compStarAlgHom'_apply]
    congr

Goal state after:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : ¬p a
⊢ cfcₙ f a = cfc f a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
⊢ φ (ContinuousMap.toNNReal 1) - φ (-1).toNNReal = 1

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
⊢ φ (ContinuousMap.toNNReal 0) - φ (-0).toNNReal = 0

Tactic:
by simp

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

Goal state before:
pp: case refine_2
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
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
x : X
⊢ x ∈ W x

Tactic:
· dsimp only [W, Set.mem_ofPred_eq]
      rw [h_eq]
      exact lt_add_of_pos_right _ pos

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 : A
⊢ ‖1 x‖ ≤ 1 * ‖x‖

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
f : C(X, ℝ)₀
⊢ (ContinuousMap.realToNNReal.comp ↑f) 0 = 0

Tactic:
by simp

Goal state after:
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
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
⊢ φ (toNNReal 0) - φ (-0).toNNReal = 0

Tactic:
by simp

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ 0 < ENNReal.toReal 1

Tactic:
by simp

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ (‖x.ofLp.toProd.1‖ ^ ENNReal.toReal 1 + ‖x.ofLp.toProd.2‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) =
    ‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖

Tactic:
by simp

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

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

Tactic:
snd_smul,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r • x.ofLp.toProd.1‖ + ‖r • x.ofLp.toProd.2‖ ≤ ‖r‖ * (‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖)
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 : Set β
⊢ ∀ ⦃t : Set β⦄, s ⊆ t → f ⁻¹' Iic s ∈ 𝓝[s✝] x → f ⁻¹' Iic t ∈ 𝓝[s✝] x

Tactic:
t

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s✝ : Set α
x : α
inst✝ : TopologicalSpace β
s t : Set β
⊢ s ⊆ t → f ⁻¹' Iic s ∈ 𝓝[s✝] x → f ⁻¹' Iic t ∈ 𝓝[s✝] x
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 : Set β
⊢ ∀ ⦃t : Set β⦄, s ⊆ t → (∀ᶠ (x' : α) in 𝓝[s✝] x, s ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s✝] x, t ∈ 𝓝ˢ (f x')

Tactic:
t

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] (f ⁻¹' Iic u)

Tactic:
simp_rw [upperHemicontinuous_iff_preimage_Iic, isOpen_iff_mem_nhds (s := f ⁻¹' Iic _)]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔ ∀ (u : Set β), IsOpen[inst✝] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
x : α
| ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x

Tactic:
rw [hasBasis_nhdsSet (f x) |>.forall_iff fun s t hst ↦ by gcongr]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
x : α
| ∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝 x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

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

Tactic:
t

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ∀ t ∈ 𝓝 (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝 (f x')
t : Set β
⊢ t ∈ 𝓝 (f x) → ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ t
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
⊢ SemicontinuousAt (fun x t ↦ IsOpen[inst✝] t ∧ ((fun x ↦ {x}) x ∩ t).Nonempty) x

Tactic:
t

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
t : Set α
⊢ (fun x t ↦ IsOpen[inst✝] t ∧ ((fun x ↦ {x}) x ∩ t).Nonempty) x t →
    ∀ᶠ (x' : α) in 𝓝 x, (fun x t ↦ IsOpen[inst✝] t ∧ ((fun x ↦ {x}) x ∩ t).Nonempty) x' t
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

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

Tactic:
t

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ∀ (u : Set β), IsOpen[inst✝] u → f x ∈ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∈ u
t : Set β
⊢ t ∈ 𝓝 (f x) → ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ t
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
n✝ : ℕ
⊢ n✝ + 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: 𝕜 : Type u_1
A✝ : Type u_2
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing A✝
inst✝⁴ : NormedAlgebra 𝕜 A✝
inst✝³ : CompleteSpace A✝
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : CompactSpace ↑(spectrum ℝ a)
⊢ CompactSpace ↑(spectrum ℝ≥0 a)

Tactic:
← isCompact_iff_compactSpace

Goal state after:
𝕜 : Type u_1
A✝ : Type u_2
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing A✝
inst✝⁴ : NormedAlgebra 𝕜 A✝
inst✝³ : CompleteSpace A✝
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : IsCompact (spectrum ℝ a)
⊢ IsCompact (spectrum ℝ≥0 a)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedRing A
inst✝¹¹ : NormedAlgebra 𝕜 A
inst✝¹⁰ : CompleteSpace A
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : CompactSpace ↑(quasispectrum ℝ a)
⊢ CompactSpace ↑(quasispectrum ℝ≥0 a)

Tactic:
← isCompact_iff_compactSpace

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedRing A
inst✝¹¹ : NormedAlgebra 𝕜 A
inst✝¹⁰ : CompleteSpace A
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : IsCompact (quasispectrum ℝ a)
⊢ IsCompact (quasispectrum ℝ≥0 a)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ V.preimage (closure[inst✝.toTopologicalSpace] t) ⊆ SetRel.preimage U t

Tactic:
closure_subset_preimage hV t,

Goal state after:
case left
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ V.preimage (V.preimage t) ⊆ SetRel.preimage U t
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
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ Metric.eball 0 (↑‖a‖₊)⁻¹
h : ‖a‖₊ = 0
⊢ ‖y • a‖ < 1

pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ Metric.eball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
⊢ ‖y • a‖ < 1

Tactic:
· simp only [nnnorm_eq_zero.mp h, norm_zero, zero_lt_one, smul_zero]

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ Metric.eball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
⊢ ‖y • a‖ < 1