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

Goal state before:
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:
have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹ := by
            simpa only [← coe_inv h, mem_ball_zero_iff, Metric.eball_coe] using! hy

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
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y • a‖ < 1
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✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
K' : Compacts α
h₁ : ↑K' ⊆ interior L
⊢ (∀ i ∈ u, (↑K' ∩ interior (M i)).Nonempty) → ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty

Tactic:
h₂

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
K' : Compacts α
h₁ : ↑K' ⊆ interior L
h₂ : ∀ i ∈ u, (↑K' ∩ interior (M i)).Nonempty
⊢ ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
⊢ 0 ≤ approx n c x

Tactic:
induction n generalizing c with
  | zero => exact indicator_nonneg (fun _ _ => zero_le_one) _
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add]
    refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst✝², _] f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
x : X
⊢ { toFun := fun x ↦ 1 - f x, continuous_toFun := ⋯ } x ∈ Icc 0 1

Tactic:
have : 0 ≤ f x ∧ f x ≤ 1 := by simpa using h'f x
    simp [this]

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
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ max (-x) 0 * max x 0 = 0 x

Tactic:
simpa using le_total 0 x

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)

Tactic:
by_cases htriv : 0 ≤ a

Goal state after:
case pos
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)

case neg
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : ¬0 ≤ a
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
⊢ ConvexOn ℝ s fun x ↦ ↑(cfcₙ f x)

Tactic:
h₂

Goal state after:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
⊢ ConvexOn ℝ s fun x ↦ cfc f ↑x
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalCStarAlgebra A
inst✝⁸ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : Module ℂ E
inst✝⁵ : SMul A E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module ℂ F
inst✝² : SMul A F
inst✝¹ : CStarModule A E
inst✝ : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2

Tactic:
gcongr; positivity

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹¹ : NormedRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : NormedAlgebra ℝ A
inst✝⁸ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁷ : ContinuousStar A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
have hs' := hs
  simp only [nhdsSet_iUnion, mem_iSup] at hs'
  have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s := by
    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      spectrum.isCompact_nnreal (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
    refine ⟨S, hS₂, ?_, hS₃⟩
    exact upperHemicontinuous_spectrum_nnreal A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet
  choose S hS₁ hS₂ hS₃ using this
  classical
  refine ha_cont.cfc_nnreal (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
    (by simpa +contextual using hS₁) ?_ ha' ?_
  all_goals simp +contextual only [↓reduceDIte]
  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x, ‖diagonal v x x‖₊ ^ 2) ^ (1 / 2) = (∑ x, ‖v x‖₊ ^ 2) ^ (1 / 2)

Tactic:
diagonal_apply_eq,

Goal state after:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x, ‖v x‖₊ ^ 2) ^ (1 / 2) = (∑ x, ‖v x‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
⊢ False

Tactic:
have (n : ℕ) : ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖ := by
    obtain ⟨hx₁, hx₂⟩ := Classical.choose_spec (hcontra (2 ^ (2 * n)))
    set x := Classical.choose (hcontra (2 ^ (2 * n)))
    have hx := (eq_zero_or_norm_pos x).resolve_left (fun hx ↦ by simp_all)
    refine ⟨‖x‖⁻¹ • x, smul_nonneg (by positivity) hx₁, ?_, ?_⟩
    · simp [norm_smul, inv_mul_cancel₀ hx.ne']
    · simpa [norm_smul] using (lt_inv_mul_iff₀' hx).mpr hx₂

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
this : ∀ (n : ℕ), ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ :
  (f, a) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f, a).2)
hs : IsCompact (quasispectrum ℝ≥0 a)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)
hk : IsCompact k
⊢ ∃ t,
    IsOpen[instTopologicalSpaceProd] t ∧
      (f, a) ∈ t ∧
        ContinuousOn (fun fa ↦ cfcₙ ((toFun {s}) fa.1) fa.2)
          ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
              {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)} ∩
            t)

Tactic:
have := (upperHemicontinuous_quasispectrum_nnreal A).isOpen k

Goal state after:
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ :
  (f, a) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f, a).2)
hs : IsCompact (quasispectrum ℝ≥0 a)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}
⊢ ∃ t,
    IsOpen[instTopologicalSpaceProd] t ∧
      (f, a) ∈ t ∧
        ContinuousOn (fun fa ↦ cfcₙ ((toFun {s}) fa.1) fa.2)
          ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
              {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)} ∩
            t)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹³ : NonUnitalNormedRing A
inst✝¹² : StarRing A
inst✝¹¹ : NormedSpace ℝ A
inst✝¹⁰ : IsScalarTower ℝ A A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : ContinuousStar A
inst✝⁷ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ

Tactic:
exact ha_cont.cfcₙ_nnreal_of_mem_nhdsSet f (by simpa) (by simpa)

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

Goal state before:
pp: case e_6
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (mkD ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
z : ↑(spectrum 𝕜 a)
⊢ (mkD ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z =
    (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z

Tactic:
← key₁,

Goal state after:
case e_6
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (mkD ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
z : ↑(spectrum 𝕜 a)
⊢ (mkD ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z = ∫ (x : X), f x ↑z ∂μ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: case mp
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ (x✝ ∈ Set.range fun x ↦ cfcₙ x a) → x✝ ∈ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}

Tactic:
rintro ⟨f, rfl⟩
    simp only [cfcₙ_nnreal_eq_real f a]
    exact ⟨_, fun _ _ ↦ by positivity, rfl⟩

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

Goal state before:
pp: A : Type u_1
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module ℝ A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : SMulCommClass ℝ A A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : IsTopologicalRing A
inst✝⁷ : T2Space A
inst✝⁶ : PartialOrder A
inst✝⁵ : NonnegSpectrumClass ℝ A
inst✝⁴ : StarOrderedRing A
inst✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ f a
⊢ ?m.203

Tactic:
simpa only [not_and_or] using
      em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a)

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

Goal state before:
pp: case e_6
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
key₁ :
  ∀ (z : ↑(quasispectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(quasispectrum 𝕜 a)),
    ∫ (x : X), f x ↑z ∂μ = (mkD ((quasispectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
z : ↑(quasispectrum 𝕜 a)
⊢ (mkD ((quasispectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z =
    (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z

Tactic:
← key₁,

Goal state after:
case e_6
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
key₁ :
  ∀ (z : ↑(quasispectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(quasispectrum 𝕜 a)),
    ∫ (x : X), f x ↑z ∂μ = (mkD ((quasispectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
z : ↑(quasispectrum 𝕜 a)
⊢ (mkD ((quasispectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z = ∫ (x : X), f x ↑z ∂μ
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ℓ z • x - ℓ x • z ∈ Y
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
h₂

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ℓ z • x - ℓ x • z ∈ Y
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case e_2
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src := l2OpNormedAddCommGroupAux.replaceTopology ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
⊢ IsTopologicalAddGroup.rightUniformSpace (Matrix m n 𝕜) = PseudoEMetricSpace.toUniformSpace

Tactic:
rw [@IsUniformAddGroup.rightUniformSpace_eq _ PseudoEMetricSpace.toUniformSpace _ _]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y = ↑(U.openPartialHomeomorphSubtypeCoe hU) (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y))

Tactic:
rw [(U.openPartialHomeomorphSubtypeCoe hU).right_inv hy.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 : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ { proj := x, snd := Z.coordChange i (Z.indexAt x) x (Z.coordChange (Z.indexAt x) i x v) } = { proj := x, snd := v }

Tactic:
rw [Z.coordChange_comp, Z.coordChange_self] <;> apply_rules [mem_baseSet_at, mem_inter]

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 : ι
⊢ ∀ ⦃x : B × F⦄,
    x ∈ Z.baseSet i ×ˢ univ →
      ({ proj := x.1, snd := Z.coordChange i (Z.indexAt x.1) x.1 x.2 }.proj,
          Z.coordChange (Z.indexAt { proj := x.1, snd := Z.coordChange i (Z.indexAt x.1) x.1 x.2 }.proj) i
            { proj := x.1, snd := Z.coordChange i (Z.indexAt x.1) x.1 x.2 }.proj
            { proj := x.1, snd := Z.coordChange i (Z.indexAt x.1) x.1 x.2 }.snd) =
        x

Tactic:
by
    rintro ⟨x, v⟩ hx
    simp only [prodMk_mem_set_prod_eq, and_true, mem_univ] at hx
    dsimp only
    rw [Z.coordChange_comp, Z.coordChange_self]
    exacts [hx, ⟨⟨hx, Z.mem_baseSet_at _⟩, hx⟩]

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

Goal state before:
pp: case left
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source

Tactic:
ext x
    simp only [mem_localTrivAsPartialEquiv_target, mfld_simps]
    rfl

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
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
⊢ IsOpen[instTopologicalSpaceProd] (f.source ∩ ↑f ⁻¹' s)

Tactic:
rw [PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)]

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
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
⊢ IsOpen[instTopologicalSpaceProd] ((Z.trivChange i j).source ∩ ↑(Z.trivChange i j).toPartialEquiv ⁻¹' s)