mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ cfc f a ≤ 1

Tactic:
by
  apply cfc_cases (· ≤ 1) _ _ (by simp) fun hf ha ↦ ?_
  rw [← map_one (cfcHom ha (R := R))]
  apply cfcHom_mono ha
  simpa [ContinuousMap.le_def] using h

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✝¹¹ : 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun z ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i, f ↑i) (σₙ R a)
⊢ cfcₙ (∑ i, f ↑i) a = ∑ i, cfcₙ (f ↑i) a

Tactic:
rw [cfcₙ_apply_pi _ a ha (fun ⟨i, hi⟩ => hf i hi), ← map_sum, cfcₙ_apply _ a hf']

Goal state after:
case pos
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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun z ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i, f ↑i) (σₙ R a)
⊢ (cfcₙHom ha) { toFun := (σₙ R a).domRestrict (∑ i, f ↑i), continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) (∑ x, { toFun := (σₙ R a).domRestrict (f ↑x), continuous_toFun := ⋯, map_zero' := ⋯ })
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 ≤ cfcₙ f a

pp: case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a

Tactic:
· simp only [cfcₙ_apply_of_not_continuousOn _ hf, le_rfl]

Goal state after:
case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ f a ≤ 0

pp: case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬f 0 = 0
⊢ cfcₙ f a ≤ 0

Tactic:
· simp only [cfcₙ_apply_of_not_continuousOn _ hf, le_rfl]

Goal state after:
case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬f 0 = 0
⊢ cfcₙ f a ≤ 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case e'_5
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
f : C(X, ℝ≥0)
⊢ φ ({ toFun := toReal, continuous_toFun := continuous_coe }.comp f).toNNReal = φ f

pp: case e'_6
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
f : C(X, ℝ≥0)
⊢ φ (-{ toFun := toReal, continuous_toFun := continuous_coe }.comp f).toNNReal = φ 0

Tactic:
all_goals
    congr
    ext x
    simp

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

Goal state before:
pp: case e'_5
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
f : C(X, ℝ≥0)₀
⊢ φ ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = φ f

pp: case e'_6
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
f : C(X, ℝ≥0)₀
⊢ φ (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = φ 0

Tactic:
all_goals
    congr
    ext x
    simp

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : Ring A
inst✝¹ : TopologicalSpace A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
z : 𝕜
⊢ φ ((algebraMap 𝕜 A) z) = z

Tactic:
simp [AlgHomClass.commutes]

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
k : 𝕜
a✝ : ↑(characterSpace 𝕜 A)
⊢ { toFun := fun φ ↦ φ ((algebraMap 𝕜 A) k), continuous_toFun := ⋯ } a✝ =
    ((algebraMap 𝕜 C(↑(characterSpace 𝕜 A), 𝕜)) k) a✝

Tactic:
simp [AlgHomClass.commutes]

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

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id s) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id s)) * a = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
⊢ φ f * a = 0

Tactic:
induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simp [map_zero]
  | id => exact hmul_id
  | star_id => exact hmul_star_id
  | add _ _ h₁ h₂ => simp only [map_add, add_mul, h₁, h₂, zero_add]
  | mul _ _ _ h => simp only [map_mul, mul_assoc, h, mul_zero]
  | smul _ _ h => rw [map_smul, smul_mul_assoc, h, smul_zero]
  | frequently f h => exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ (u_1 : Set β), IsOpen[inst✝] u_1 → f x ∩ u ⊆ u_1 → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ u_1

Tactic:
intro t

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst✝] u
t : Set β
⊢ IsOpen[inst✝] t → f x ∩ u ⊆ t → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ t
Module: Mathlib.Topology.Sets.VietorisTopology

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

Tactic:
intro t

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
⊢ t ∈
      {f |
        f.Finite ∧ f ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}} →
    ∀ x ∈ ⋂₀ t,
      ∃ v ∈ (fun u ↦ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
        x ∈ v ∧ v ⊆ ⋂₀ t
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
U : ℕ → Set β
hU : ∀ (i : ℕ), y₀ ∈ U i ∧ IsOpen[inst✝¹] (U i)
hUbasis : (𝓝 y₀).HasAntitoneBasis fun i ↦ U i
hev : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, (f (x n) ∩ U k).Nonempty
g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
key : ∀ (n k : ℕ), k ≤ n → (f (x n) ∩ U k).Nonempty → (f (x n) ∩ U (g n)).Nonempty
y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀
hy : ∀ (n : ℕ), (f (x n) ∩ U (g n)).Nonempty → y n ∈ f (x n) ∩ U (g n)
k : ℕ
a✝ : True
n : ℕ
⊢ (f (x n) ∩ U k).Nonempty → k ≤ n → y n ∈ U k

Tactic:
hk

Goal state after:
α : 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
U : ℕ → Set β
hU : ∀ (i : ℕ), y₀ ∈ U i ∧ IsOpen[inst✝¹] (U i)
hUbasis : (𝓝 y₀).HasAntitoneBasis fun i ↦ U i
hev : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, (f (x n) ∩ U k).Nonempty
g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
key : ∀ (n k : ℕ), k ≤ n → (f (x n) ∩ U k).Nonempty → (f (x n) ∩ U (g n)).Nonempty
y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀
hy : ∀ (n : ℕ), (f (x n) ∩ U (g n)).Nonempty → y n ∈ f (x n) ∩ U (g n)
k : ℕ
a✝ : True
n : ℕ
hk : (f (x n) ∩ U k).Nonempty
⊢ k ≤ n → y n ∈ U k
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hg : HasOpenCGraph g
hf : ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] {x | (f x ∩ u).Nonempty}
⊢ ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] {x | (f x ∩ g x ∩ u).Nonempty}

Tactic:
intro t

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hg : HasOpenCGraph g
hf : ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] {x | (f x ∩ u).Nonempty}
t : Set β
⊢ IsOpen[inst✝] t → IsOpen[inst✝¹] {x | (f x ∩ g x ∩ t).Nonempty}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case a.refine_2
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
⊢ t ⊆ V.image (U.image s ∩ V.preimage t)

Tactic:
· intro z hz
      obtain ⟨x, hx, y, hxy, hyz⟩ := hts hz
      exact ⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hyz⟩

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
inst✝ : NormOneClass A
a : A
k : 𝕜
h : ‖a‖ < ‖k‖
⊢ ‖a‖ * ‖1‖ < ‖k‖

Tactic:
by rwa [norm_one, mul_one]

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

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
hμ : μ ∈ frontier (σ 𝕜 x)
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
⊢ False

Tactic:
rw [← frontier_compl, (spectrum.isClosed _).isOpen_compl.frontier_eq, Set.mem_sdiff] at hμ

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
hμ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ∧ μ ∉ (σ 𝕜 x)ᶜ
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
⊢ False
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_2
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
replace h : ∀ x ∈ spectrum ℝ a, ‖t - x‖₊ ≤ t := by
      simpa [spectralRadius, iSup₂_le_iff, ← spectrum.singleton_sub_eq] using h

Goal state after:
case refine_2
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, ‖↑t - x‖₊ ≤ t
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ 0 ≤ a

Tactic:
obtain ⟨x, hx, -, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts ha₁ ha₂

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
x : A
hx : IsSelfAdjoint x
ha₁ : IsSelfAdjoint (x * x)
ha₂ : QuasispectrumRestricts (x * x) ⇑ContinuousMap.realToNNReal
⊢ 0 ≤ x * x
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ spectralRadius ℂ a = ↑‖a‖₊

Tactic:
have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ spectralRadius ℂ a = ↑‖a‖₊
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
ha : p a
⊢ Isometry ⇑(cfcₙHom ha)

Tactic:
have : CompactSpace (σₙ 𝕜 a) := by
      have h_cpct : CompactSpace (spectrum 𝕜 a) := inferInstance
      simp only [← isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_zero] at h_cpct ⊢
      exact h_cpct |>.union isCompact_singleton
    rw [cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom]
    refine isometry_cfcHom a |>.comp ?_
    simp only [MulHom.coe_coe, NonUnitalStarAlgHom.coe_toNonUnitalAlgHom]
    refine AddMonoidHomClass.isometry_of_norm _ fun f ↦ ?_
    let ι : C(σ 𝕜 a, σₙ 𝕜 a) := ⟨_, continuous_inclusion <| spectrum_subset_quasispectrum 𝕜 a⟩
    change ‖(f : C(σₙ 𝕜 a, 𝕜)).comp ι‖ = ‖(f : C(σₙ 𝕜 a, 𝕜))‖
    apply le_antisymm (ContinuousMap.norm_le _ (by positivity) |>.mpr ?_)
      (ContinuousMap.norm_le _ (by positivity) |>.mpr ?_)
    · rintro ⟨x, hx⟩
      exact (f : C(σₙ 𝕜 a, 𝕜)).norm_coe_le_norm ⟨x, spectrum_subset_quasispectrum 𝕜 a hx⟩
    · rintro ⟨x, hx⟩
      obtain (rfl | hx') : x = 0 ∨ x ∈ σ 𝕜 a := by
        simpa [quasispectrum_eq_spectrum_union_zero] using hx
      · change ‖f 0‖ ≤ _
        simp
      · exact (f : C(σₙ 𝕜 a, 𝕜)).comp ι |>.norm_coe_le_norm ⟨x, hx'⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
⊢ WithSeminorms (gaugeSeminormFamily 𝕜 E)

Tactic:
refine SeminormFamily.withSeminorms_of_hasBasis _ ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ (gaugeSeminormFamily 𝕜 E).basisSets) id
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: 𝕜✝ : Type u_1
E : Type u_2
F✝ : Type u_3
inst✝⁷ : RCLike 𝕜✝
𝕜 : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
⊢ Continuous (↑extendRCLikeₗ).toFun

Tactic:
by
    rw [(ContinuousLinearMap.isEmbedding_restrictScalars ℝ).continuous_iff]
    let smulI : F →L[ℝ] F := (I : 𝕜) • ContinuousLinearMap.id 𝕜 F |>.restrictScalars ℝ
    let mulI : 𝕜 →L[ℝ] 𝕜 := ContinuousLinearMap.mul ℝ 𝕜 (I : 𝕜)
    exact ofRealCLM.postcomp F - mulI.postcomp F ∘L smulI.precomp 𝕜 ∘L ofRealCLM.postcomp F
      |>.continuous

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

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
rw [LinearMap.mem_span_iff_continuous]

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
⊢ Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ ↔
    ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst✝¹, _] ⇑(p i)
bdd : BddAbove (range p)
⊢ Continuous[inst✝¹, _] ⇑(⨆ i, p i)

Tactic:
refine Seminorm.continuous_of_lowerSemicontinuous _ ?_

Goal state after:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst✝¹, _] ⇑(p i)
bdd : BddAbove (range p)
⊢ LowerSemicontinuous ⇑(⨆ i, p i)
Module: Mathlib.Analysis.Normed.Operator.Completeness

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf : ⇑f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' closedBall f₀ r)
hr : 0 ≤ r
x : E'
this : IsClosed[Pi.topologicalSpace] {g | ‖g x - f₀ x‖ ≤ r * ‖x‖}
⊢ ‖(f - f₀) x‖ ≤ r * ‖x‖

Tactic:
refine this.closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf : ⇑f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' closedBall f₀ r)
hr : 0 ≤ r
x : E'
this : IsClosed[Pi.topologicalSpace] {g | ‖g x - f₀ x‖ ≤ r * ‖x‖}
g : E' →SL[σ₁₂] F
hg : g ∈ closedBall f₀ r
⊢ g ∈ DFunLike.coe ⁻¹' {g | ‖g x - f₀ x‖ ≤ r * ‖x‖}