mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ max 1 ‖1‖₊

Tactic:
grw [nnnorm_pow_le' a n.succ_pos, ← le_max_left]

Goal state after:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.vietoris α] fun x ↦ x.1 ∪ x.2

Tactic:
simp_rw [continuous_iff, powerset, preimage_ofPred_eq, union_subset_iff, ofPred_and]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (U : Set α), IsOpen[inst✝] U → IsOpen[instTopologicalSpaceProd] ({a | a.1 ⊆ U} ∩ {a | a.2 ⊆ U})) ∧
    ∀ (F : Set α), IsClosed[inst✝] F → IsClosed[instTopologicalSpaceProd] ({a | a.1 ⊆ F} ∩ {a | a.2 ⊆ F})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) K₁ K₂

Tactic:
wlog h' : ¬(K₁ ≤ K₂) generalizing K₁ K₂

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
this :
  ∀ (K₁ K₂ : Compacts α),
    K₁ ≠ K₂ → ¬K₁ ≤ K₂ → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) K₁ K₂
h' : ¬¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ {⊥}ᶜ ∩ {a | ↑a ⊆ s} ⊆ {⊥}ᶜ ∩ closure {a | (↑a).Finite ∧ ↑a ⊆ s}

Tactic:
closure_finite_subsets,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ {⊥}ᶜ ∩ {a | ↑a ⊆ s} ⊆ {⊥}ᶜ ∩ {K | ↑K ⊆ closure[inst✝] s}
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : PolynormableSpace 𝕜 E
S : Submodule 𝕜 E
f : StrongDual 𝕜 ↥S
q : Seminorm 𝕜 E
hq_cont : Continuous[inst✝⁴, _] ⇑q
hq : (↑f).toSeminorm ≤ q.comp S.subtype
⊢ ∃ g, ∀ (x : ↥S), g ↑x = f x

Tactic:
obtain ⟨g, hg, _⟩ := Dual.exists_continuous_extension_of_le_seminorm S f.toLinearMap hq_cont hq

Goal state after:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : PolynormableSpace 𝕜 E
S : Submodule 𝕜 E
f : StrongDual 𝕜 ↥S
q : Seminorm 𝕜 E
hq_cont : Continuous[inst✝⁴, _] ⇑q
hq : (↑f).toSeminorm ≤ q.comp S.subtype
g : StrongDual 𝕜 E
hg : ∀ (x : ↥S), g ↑x = ↑f x
right✝ : ∀ (x : E), ‖g x‖ ≤ q x
⊢ ∃ g, ∀ (x : ↥S), g ↑x = f x
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∉ c.U
⊢ approx 0 c x = 1

Tactic:
rw [← mem_compl_iff] at hx
    exact indicator_of_mem hx _

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

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

Tactic:
by
  simp only [lineMap_apply_module]
  rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

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

Tactic:
simp only [lineMap_apply_module']

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r r' : k
h : a < b
⊢ r • (b - a) + a ≤ r' • (b - a) + a ↔ r ≤ r'
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

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

Tactic:
simp only [lineMap_apply_module']

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r r' : k
h : a < b
⊢ r • (b - a) + a < r' • (b - a) + a ↔ r < r'
Module: Mathlib.Topology.ContinuousMap.Ideals

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

Tactic:
rwa [ht'] at hy

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
⊢ ∀ a_1 ∈ {a, b}, ∀ b_1 ∈ {a, b}, a_1 * star b_1 = star b_1 * a_1

Tactic:
grind [commute_star_comm]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺) a * cfcₙ (fun x ↦ x⁻) a = 0

pp: case neg
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺) a * cfcₙ (fun x ↦ x⁻) a = 0

Tactic:
· rw [← cfcₙ_mul _ _, ← cfcₙ_zero ℝ a]
    refine cfcₙ_congr (fun x _ ↦ ?_)
    simp only [_root_.posPart_def, _root_.negPart_def]
    simpa using le_total x 0

Goal state after:
case neg
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺) a * cfcₙ (fun x ↦ x⁻) a = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺) (-a) = a⁻

Tactic:
negPart_def,

Goal state after:
case pos
A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺) (-a) = cfcₙ (fun x ↦ x⁻) a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
⊢ cfcₙ (fun x ↦ x⁺) (-a) = a⁻

Tactic:
negPart_def,

Goal state after:
case neg
A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
⊢ cfcₙ (fun x ↦ x⁺) (-a) = cfcₙ (fun x ↦ x⁻) a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = -a⁻

Tactic:
negPart_def,

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = -cfcₙ (fun x ↦ x⁻) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ spectrum ℝ (cfc (fun x ↦ id x ^ 2) a), 0 ≤ x

Tactic:
cfc_map_spectrum ..

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ (fun x ↦ id x ^ 2) '' spectrum ℝ a, 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
n : ℕ
⊢ (↑n)⁺ = ↑n

Tactic:
by
  rw [← map_natCast (algebraMap ℝ≥0 A), posPart_algebraMap_nnreal]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra ℝ A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : ContinuousStar A
inst✝ : CompleteSpace A
r : ℝ
⊢ ∀ i ∈ {a | IsStrictlyPositive a}, spectrum ℝ≥0 (id i) ⊆ {0}ᶜ

Tactic:
exact fun a ha ↦ by simpa using spectrum.zero_notMem _ ha.isUnit

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
tfae_1_iff_9 : 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : 0 ≤ a → a = sqrt a * sqrt a
tfae_2_to_3 : a = sqrt a * sqrt a → ∃ b, 0 ≤ b ∧ a = b * b
tfae_3_to_4 : (∃ b, 0 ≤ b ∧ a = b * b) → ∃ b, IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : (∃ b, IsSelfAdjoint b ∧ a = b * b) → ∃ b, a = star b * b
⊢ [0 ≤ a, a = sqrt a * sqrt a, ∃ b, 0 ≤ b ∧ a = b * b, ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE

Tactic:
tfae_have 5 → 6 := fun ⟨b, hb⟩ => ⟨star b, star_star b |>.symm ▸ hb⟩

Goal state after:
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
tfae_1_iff_9 : 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : 0 ≤ a → a = sqrt a * sqrt a
tfae_2_to_3 : a = sqrt a * sqrt a → ∃ b, 0 ≤ b ∧ a = b * b
tfae_3_to_4 : (∃ b, 0 ≤ b ∧ a = b * b) → ∃ b, IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : (∃ b, IsSelfAdjoint b ∧ a = b * b) → ∃ b, a = star b * b
tfae_5_to_6 : (∃ b, a = star b * b) → ∃ b, a = b * star b
⊢ [0 ≤ a, a = sqrt a * sqrt a, ∃ b, 0 ≤ b ∧ a = b * b, ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ↑(f (a • x + b • y)) ≤ ↑(a • f x + b • f y)

Tactic:
simpa using hf₂.2 hx hy ha hb hab

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ↑(a • f x + b • f y) ≤ ↑(f (a • x + b • y))

Tactic:
simpa using hf₂.2 hx hy ha hb hab

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ ≤ ↑↑(Fintype.card ι) * ‖(linearEquiv ℂ A ((i : ι) → E i)) x‖

Tactic:
simp only [NNReal.coe_natCast, linearEquiv_apply]

Goal state after:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ ≤ ↑(Fintype.card ι) * ‖(equiv A ((i : ι) → E i)) x‖
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ a * ‖a‖ • a⁻¹ = (algebraMap ℝ α) ‖a‖

Tactic:
rw [mul_smul_comm, mul_inv_cancel₀ h, Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Goal state before:
pp: F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst✝⁷ : NonUnitalCStarAlgebra A₁
inst✝⁶ : NonUnitalCStarAlgebra A₂
inst✝⁵ : PartialOrder A₁
inst✝⁴ : PartialOrder A₂
inst✝³ : StarOrderedRing A₁
inst✝² : StarOrderedRing A₂
inst✝¹ : FunLike F A₁ A₂
inst✝ : LinearMapClass F ℂ A₁ A₂
h : ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ
φ : F
a : A₁
ha : 0 ≤ a
⊢ 0 ≤ φ a

Tactic:
simpa using! map_nonneg (toOneByOne (Fin 1) ℂ A₂).symm <|
    h φ 1 _ <| map_nonneg (toOneByOne (Fin 1) ℂ A₁) ha

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
z : ↑(quasispectrum 𝕜 a)
x : X
cont_x : ContinuousOn (f x) (quasispectrum 𝕜 a)
zero_x : f x 0 = 0
⊢ f x ↑z = (mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) z

Tactic:
mkD_apply_of_continuousOn cont_x zero_x

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
z : ↑(quasispectrum 𝕜 a)
x : X
cont_x : ContinuousOn (f x) (quasispectrum 𝕜 a)
zero_x : f x 0 = 0
⊢ f x ↑z = f x ↑z
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ spectrum ℂ (cfc (fun x ↦ ↑x.re) a) = (fun x ↦ ↑x.re) '' spectrum ℂ a

Tactic:
cfc_map_spectrum ..

Goal state after:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ (fun x ↦ ↑x.re) '' spectrum ℂ a = (fun x ↦ ↑x.re) '' spectrum ℂ a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ spectrum ℂ (cfc (fun x ↦ ↑x.im) a) = (fun x ↦ ↑x.im) '' spectrum ℂ a

Tactic:
cfc_map_spectrum ..

Goal state after:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ (fun x ↦ ↑x.im) '' spectrum ℂ a = (fun x ↦ ↑x.im) '' spectrum ℂ a
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e f : Pretrivialization F proj
⊢ f.target ∩ ↑f.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ

Tactic:
inter_comm,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e f : Pretrivialization F proj
⊢ ↑f.symm ⁻¹' e.source ∩ f.target = (e.baseSet ∩ f.baseSet) ×ˢ univ
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ e.baseSet ×ˢ univ ∩ ↑e.symm ⁻¹' proj ⁻¹' e'.baseSet = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Tactic:
inter_comm,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ ↑e.symm ⁻¹' proj ⁻¹' e'.baseSet ∩ e.baseSet ×ˢ univ = (e.baseSet ∩ e'.baseSet) ×ˢ univ
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ x ∈ Z.baseSet j

Tactic:
exact hx.2

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ContinuousOn (fun p ↦ (p.1, Z.coordChange j i p.1 p.2)) ((Z.baseSet i ∩ Z.baseSet j) ×ˢ univ)

Tactic:
by
    simpa [inter_comm] using continuous_fst.continuousOn.prodMk (Z.continuousOn_coordChange j i)

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
ht :
  t ∈
    ⋃ i,
      ⋃ s,
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' s}
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
ht :
  ∃ i i_1,
    IsOpen[instTopologicalSpaceProd] i_1 ∧
      t = (Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' i_1
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      (Z.localTrivAsPartialEquiv i).invFun ⁻¹'
        ((Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))

Tactic:
simp only [preimage_inter]

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))