mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
U V : SetRel α α
⊢ hausdorffEntourage (U ○ V) = hausdorffEntourage U ○ hausdorffEntourage V

Tactic:
apply subset_antisymm
  · intro ⟨s, t⟩ ⟨hst, hts⟩
    simp only [mem_comp, mem_hausdorffEntourage] at *
    refine ⟨U.image s ∩ V.preimage t, ⟨?_, Set.inter_subset_left⟩, ⟨Set.inter_subset_right, ?_⟩⟩
    · intro x hx
      obtain ⟨z, hz, y, hxy, hyz⟩ := hst hx
      exact ⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hxy⟩
    · intro z hz
      obtain ⟨x, hx, y, hxy, hyz⟩ := hts hz
      exact ⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hyz⟩
  · intro ⟨s₁, s₃⟩ ⟨s₂, ⟨h₁₂, h₂₁⟩, ⟨h₂₃, h₃₂⟩⟩
    simp only at *
    grw [mem_hausdorffEntourage, preimage_comp, ← h₂₃, ← h₁₂, image_comp, ← h₂₁, ← h₃₂]
    exact ⟨subset_rfl, subset_rfl⟩

Goal state after:
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✝ : Subsingleton A
a : A
⊢ spectralRadius 𝕜 a = 0

Tactic:
by
  simp [spectralRadius]

Goal state after:
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
⊢ spectralRadius 𝕜 1 = 1

Tactic:
by
  simp [spectralRadius]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), UpperHemicontinuousOn (F n) s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, f x' ⊆ u

Tactic:
obtain ⟨V, hV, hVsym, hVcomp⟩ := comp_symm_mem_uniformity_sets hW

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), UpperHemicontinuousOn (F n) s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, f x' ⊆ u
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
U : SetRel β β
hUsub : id U ⊆ V
hUmem : U ∈ uniformity β
hUopen : IsOpen[instTopologicalSpaceProd] U
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
hFN_image : F N x₀ ⊆ U.image (f x₀)
hF : ∀ (n : ι), ∀ x ∈ s, UpperHemicontinuousWithinAt (F n) s x
hFN_uhc : ∀ᶠ (x : α) in 𝓝[s] x₀, F N x ⊆ U.image (f x₀)
x : α
hFNx : F N x ⊆ U.image (f x₀)
hx_s : x ∈ s
⊢ f x ⊆ u

Tactic:
intro y

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
U : SetRel β β
hUsub : id U ⊆ V
hUmem : U ∈ uniformity β
hUopen : IsOpen[instTopologicalSpaceProd] U
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
hFN_image : F N x₀ ⊆ U.image (f x₀)
hF : ∀ (n : ι), ∀ x ∈ s, UpperHemicontinuousWithinAt (F n) s x
hFN_uhc : ∀ᶠ (x : α) in 𝓝[s] x₀, F N x ⊆ U.image (f x₀)
x : α
hFNx : F N x ⊆ U.image (f x₀)
hx_s : x ∈ s
y : β
⊢ y ∈ f x → y ∈ u
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
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1

Tactic:
· rw [← coe_inv h, coe_lt_coe, NNReal.lt_inv_iff_mul_lt h] at hr
          simpa only [← mul_pow, mul_comm] using! pow_le_one' hr.le n.succ

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ ψ { toContinuousMap := ContinuousMap.restrict (σₙ 𝕜 a) (ContinuousMap.id 𝕜), map_zero' := ⋯ } = a

Tactic:
exact inr_injective (R := 𝕜) <| coe_ψ _ ▸ cfcₙAux_id hp₁ a ha

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
⊢ (inrNonUnitalStarAlgHom 𝕜 A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha

Tactic:
let _ := RCLike.nonUnitalContinuousFunctionalCalculus hp₁

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
x✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p := RCLike.nonUnitalContinuousFunctionalCalculus fun {x} ↦ hp₁
⊢ (inrNonUnitalStarAlgHom 𝕜 A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: s t : Set ℝ
⊢ (convexHull ℝ) (⇑equivRealProdLm ⁻¹' s ×ˢ t) = ⇑equivRealProdLm ⁻¹' (convexHull ℝ) (s ×ˢ t)

Tactic:
by
      simpa only [← LinearEquiv.image_symm_eq_preimage]
        using! ((equivRealProdLm.symm.toLinearMap).image_convexHull (s ×ˢ t)).symm

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsSemitopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σ ℝ a, 0 ≤ f x
ha : 0 ≤ a
⊢ cfc f a = cfc (fun x ↦ (f ↑x).toNNReal) a

Tactic:
cfc_nnreal_eq_real ..

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsSemitopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σ ℝ a, 0 ≤ f x
ha : 0 ≤ a
⊢ cfc f a = cfc (fun x ↦ ↑(f ↑x.toNNReal).toNNReal) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.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✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc f a‖₊

Tactic:
cfc_nnreal_eq_real ..

Goal state after:
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (fun x ↦ ↑(f x.toNNReal)) a‖₊
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
n : ℕ
⊢ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n) = ↑‖a ^ n‖₊ ^ (↑2 * (1 / ↑n))

Tactic:
rpow_mul,

Goal state after:
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
n : ℕ
⊢ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n) = (↑‖a ^ n‖₊ ^ ↑2) ^ (1 / ↑n)
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
⊢ ∀ (i : ℕ), True → ∃ i', True ∧ v i' ⊆ u i

Tactic:
intro n _
      obtain ⟨W, ⟨hW_nhds, hW_abs⟩, hWn⟩ :=
        (nhds_hasBasis_absConvex 𝕜 E).mem_iff.mp (hu_basis.mem_of_mem trivial)
      obtain ⟨m, hm⟩ := hu_basis.mem_iff.mp hW_nhds
      exact ⟨m, trivial, (absConvexHull_min (interior_subset.trans hm) hW_abs).trans hWn⟩

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ LocallyCompactSpace (NonemptyCompacts α) ↔ LocallyCompactSpace α

Tactic:
refine ⟨fun _ => ⟨fun x U hU => ?_⟩, fun _ => inferInstance⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x✝ : LocallyCompactSpace (NonemptyCompacts α)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
⊢ IsStarNormal a ↔ ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A

Tactic:
let _ : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
  have : IsAddTorsionFree A := IsAddTorsionFree.of_module_rat A
  refine ⟨fun ha x ↦ ?_, fun ha ↦ ?_⟩
  /- If `a` is normal, then clearly `exp (x • a) * exp (- x • star a) = exp (I • x • 2 • ℑ a)`
  and the latter is clearly an exponential unitary. -/
  · convert! (selfAdjoint.expUnitary (x • (2 : ℝ) • ℑ a)).2
    have hcomm := star_comm_self (x := a) |>.symm.smul_left x |>.smul_right (-x)
    rw [← exp_add_of_commute hcomm]
    simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_comm x I, smul_smul I I, smul_add x,
      sub_eq_add_neg]
  /- Take any `x : ℝ` and suppose `u := exp (x • a) * exp (- x • a)` is unitary. Then
  `exp (- x • a) * exp (x • star a) = star u = u⁻¹ = exp (x • star a) * exp (- x • a)`. -/
  · have key : ∀ x : ℝ, exp (- x • a) * exp (x • star a) = exp (x • star a) * exp (- x • a) := by
      intro x
      let u : unitary A := ⟨_, ha x⟩
      convert! congr(($(Unitary.star_eq_inv u) : A))
      · simp [u, star_exp]
      · simp_rw [u, ← Unitary.val_inv_toUnits_apply, neg_smul, ← Units.mul_eq_one_iff_eq_inv,
          Unitary.val_toUnits_apply]
        let _ := invertibleExp (𝔸 := A)
        rw [mul_assoc]
        simp [← invOf_exp]
    /- Compute the second derivative with respect to `x` of each side of this expression and
    evaluate at `x = 0`. -/
    have h_deriv (a b c : A) (y : ℝ) :
        deriv (fun x : ℝ ↦ exp (x • a) * c * exp (x • b)) y =
          exp (y • a) * (a * c + c * b) * exp (y • b) := by
      rw [mul_add, add_mul, ← mul_assoc _ a, ← mul_assoc _ c b, mul_assoc _ b]
      exact (hasDerivAt_exp_smul_const a y).mul_const c |>.mul
        (hasDerivAt_exp_smul_const' b y) |>.deriv
    have h_deriv₂ (a b : A) :
        deriv (fun y ↦ deriv (fun x : ℝ ↦ exp (x • a) * exp (x • b)) y) 0 =
          a ^ 2 + 2 • (a * b) + b ^ 2 := by
      conv => enter [1, 1, y, 1, x, 1]; rw [← mul_one (exp (x • a))]
      simp_rw [h_deriv, zero_smul, NormedSpace.exp_zero, mul_one, one_mul]
      noncomm_ring
    have h₃ := h_deriv₂ (-a) (star a)
    have h₄ := h_deriv₂ (star a) (-a)
    simp only [smul_neg, even_two, Even.neg_pow, neg_smul] at h₃ h₄ key
    /- By `key`, these second derivatives evaluated at zero must be equal, so we find
    `a ^ 2 + 2 • (- a * star a) + (star a) ^ 2 = star ^ 2 + 2 • (star a * a) + a ^ 2`,
    and then elementary algebra shows `star a * a = a * star a`, so `a` is normal.  -/
    simp_rw [key] at h₃
    rw [h₃] at h₄
    rw [isStarNormal_iff, commute_iff_eq]
    apply nsmul_right_injective two_ne_zero
    rw [← sub_eq_zero] at h₄ ⊢
    rw [← h₄]
    noncomm_ring

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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
⊢ polar 𝕜 (ball 0 r) = polar 𝕜 (closedBall 0 r)

Tactic:
← closure_ball _ hr.ne',

Goal state after:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
⊢ polar 𝕜 (ball 0 r) = polar 𝕜 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 r))
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
P : Type u_3
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x : E
⊢ (k⁻¹ • fun x ↦ x -ᵥ c) ((fun x ↦ k • x +ᵥ c) x) = x

Tactic:
by simp [inv_smul_smul₀ hk]

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

Goal state before:
pp: case h.right
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SeparableSpace E
w y : WeakDual 𝕜 E
⊢ w ≠ y → ∃ n, w (denseSeq E n) ≠ y (denseSeq E n)

Tactic:
w_ne_y

Goal state after:
case h.right
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SeparableSpace E
w y : WeakDual 𝕜 E
w_ne_y : w ≠ y
⊢ ∃ n, w (denseSeq E n) ≠ y (denseSeq E n)
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : C(X, ℝ≥0)
c : ℝ≥0
hc : 0 < c
x : X
hx : x ∈ {x | c ≤ f x}
⊢ ({ toFun := (⇑f ⊔ ⇑(const X c))⁻¹, continuous_toFun := ⋯ } * f) x = 1 x

Tactic:
by
    simpa only [coe_const, mul_apply, coe_mk, Pi.inv_apply, Pi.sup_apply,
      Function.const_apply, sup_eq_left.mpr (Set.mem_ofPred.mp hx), ne_eq, Pi.one_apply]
      using inv_mul_cancel₀ (hc.trans_le hx).ne'

Goal state after:
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✝ : T2Space A
a : A
⊢ (-a)⁻ = a⁺

Tactic:
rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]

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

Goal state before:
pp: case h₁
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal

Tactic:
first | rfl | assumption

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

Goal state before:
pp: case h₁.ha
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint a

Tactic:
first | rfl | assumption

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

Goal state before:
pp: case h₁.ht
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖a‖₊ ≤ ‖a‖₊

Tactic:
first | rfl | assumption

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

Goal state before:
pp: case h₂
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts b ⇑ContinuousMap.realToNNReal

Tactic:
first | rfl | assumption

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

Goal state before:
pp: case h₂.ha
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint b

Tactic:
first | rfl | assumption

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

Goal state before:
pp: case h₂.ht
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖b‖₊ ≤ ‖b‖₊

Tactic:
first | rfl | assumption

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

Goal state before:
pp: case add
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a x y : A
x_mem : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
y_mem : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1
hy : ∀ x ∈ spectrum ℝ y, 0 ≤ x
⊢ ∀ x_1 ∈ spectrum ℝ (x + y), 0 ≤ x_1

Tactic:
rw [← SpectrumRestricts.nnreal_iff] at hx hy ⊢
      rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem
      exact hx.nnreal_add (.of_nonneg x_mem) (.of_nonneg y_mem) hy

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
ha : 0 ≤ a
⊢ sqrt (a ^ 2) = a

Tactic:
simp only [sqrt_nnrpow, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_self]

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
ha : 0 ≤ a
⊢ a ^ 1 = a
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
y : ℝ
ha : 0 ≤ a
⊢ cfc (fun x ↦ x ^ y) a = cfc (fun x ↦ x ^ y) a

Tactic:
cfc_nnreal_eq_real ..

Goal state after:
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
y : ℝ
ha : 0 ≤ a
⊢ cfc (fun x ↦ ↑(x.toNNReal ^ y)) a = cfc (fun x ↦ x ^ y) a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: 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 : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)

pp: 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 : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : ¬0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
case pos =>
    have : IsStrictlyPositive a := by grind
    simp [sqrt_eq_rpow, div_eq_mul_inv, one_mul, rpow_rpow _ _ _ hx]

Goal state after:
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 : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : ¬0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)