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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing 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
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f g : C(↑(σₙ R a), R)₀
⊢ (cfcₙHom ha) f ≤ (cfcₙHom ha) g ↔ f ≤ g

Tactic:
rw [← sub_nonneg, ← map_sub, cfcₙHom_nonneg_iff, sub_nonneg]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
      (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
    n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν

Tactic:
sum,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
      (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
    n ^ 2 • X ^ 2 * 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : TopologicalSpace A
inst✝⁵ : T2Space A
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst✝⁶] ⇑φ
hψ : Continuous[_, inst✝⁶] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
⊢ ⇑φ = ⇑ψ

Tactic:
← Set.eqOn_univ,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : TopologicalSpace A
inst✝⁵ : T2Space A
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst✝⁶] ⇑φ
hψ : Continuous[_, inst✝⁶] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
⊢ Set.EqOn (⇑φ) (⇑ψ) Set.univ
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ ContinuousSMul 𝕜 (WeakBilin B)

Tactic:
by
  refine ⟨continuous_induced_rng.2 ?_⟩
  refine cast (congr_arg _ ?_) (continuous_fst.fun_smul ((coeFn_continuous B).comp continuous_snd))
  ext
  simp only [Function.comp_apply, Pi.smul_apply, map_smulₛₗ, RingHom.id_apply, LinearMap.smul_apply]

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

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
⊢ 0 ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
exact zero_mem _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ LowerHemicontinuousWithinAt (fun x ↦ {f x}) s x ↔ ContinuousWithinAt f s x

Tactic:
by
  refine ⟨?_, fun hf ↦ (lowerHemicontinuous_singleton_id.lowerHemicontinuousWithinAt _ _).comp
    hf (mapsTo_image _ _)⟩
  simp only [lowerHemicontinuousWithinAt_iff, Set.singleton_inter_nonempty,
    ContinuousWithinAt, tendsto_iff_forall_eventually_mem]
  intro h t ht
  obtain ⟨u, hut, huo, hux⟩ := mem_nhds_iff.mp ht
  exact (h u huo hux).mono fun _ hx' ↦ hut hx'

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuous fun x ↦ f x ∩ u

Tactic:
rw [upperHemicontinuous_iff] at hf ⊢
  exact fun x ↦ (hf x).inter hu

Goal state after:
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}
t : Set β
ht : IsOpen[inst✝] t
⊢ IsOpen[inst✝¹] {x | (f x ∩ g x ∩ t).Nonempty}

Tactic:
isOpen_iff_forall_mem_open

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 β
ht : IsOpen[inst✝] t
⊢ ∀ x ∈ {x | (f x ∩ g x ∩ t).Nonempty}, ∃ t_1 ⊆ {x | (f x ∩ g x ∩ t).Nonempty}, IsOpen[inst✝¹] t_1 ∧ x ∈ t_1
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ Filter.comap (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) (𝓤 (Set α)) ≤
    𝓤 (Set α)

Tactic:
(𝓤 α).basis_sets.uniformity_hausdorff.comap _ |>.le_basis_iff
    (𝓤 α).basis_sets.uniformity_hausdorff,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
⊢ ∀ i' ∈ 𝓤 α,
    ∃ i ∈ 𝓤 α,
      (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹'
          (hausdorffEntourage ∘ id) i ⊆
        (hausdorffEntourage ∘ id) i'
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹

Tactic:
← ENNReal.inv_lt_inv,

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1⁻¹ < ε⁻¹
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹

Tactic:
refine le_trans ?_ (le_iSup _ (N + 1))

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨅ i, ↑‖a ^ (i + (N + 1))‖₊ ^ (1 / ↑(i + (N + 1))) * ε⁻¹
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
by
  open UniformSpace TopologicalSpace.vietoris in
  simp_rw [nhds_eq_comap_uniformity,
    uniformity_hasBasis_open.uniformity_hausdorff |>.comap _ |>.ge_iff, Function.comp_id,
    hausdorffEntourage, Set.preimage_ofPred_eq, Set.ofPred_and]
  intro U ⟨hU₁, hU₂⟩
  have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
  let := TopologicalSpace.vietoris α
  refine Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
    SetRel.self_subset_image _
  obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁
  obtain ⟨t, ht₁, ht₂⟩ := hs.exists_prodMk_finset_mem_hausdorffEntourage hV₁
  dsimp only at ht₁ ht₂
  filter_upwards [(Filter.eventually_all_finset t).mpr fun x hx =>
    isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (ht₁ hx)]
    with u (hu : ↑t ⊆ V.preimage ↑u)
  grw [ht₂, ← SetRel.preimage_eq_image, hu, ← hVU, SetRel.preimage_comp]

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
⊢ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
rw [frontier_eq_closure_inter_closure (s := σ 𝕜 (x : A)),
    (spectrum.isClosed (x : A)).closure_eq]

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
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 ↑x ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
⊢ IsOpen {p | Disjoint ↑p.1 ↑p.2}

Tactic:
isOpen_iff_forall_mem_open

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
⊢ ∀ x ∈ {p | Disjoint ↑p.1 ↑p.2}, ∃ t ⊆ {p | Disjoint ↑p.1 ↑p.2}, IsOpen t ∧ x ∈ t
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
⊢ Isometry ⇑(cfcHom ha)

Tactic:
obtain ⟨ha', haf⟩ := h a |>.mp ha
    have := SpectrumRestricts.cfc f halg.isClosedEmbedding h0 h
    rw [cfcHom_eq_restrict f ha ha' haf]
    refine .of_dist_eq fun g₁ g₂ ↦ ?_
    simp only [starAlgHom_apply, isometry_cfcHom a ha' |>.dist_eq]
    refine le_antisymm ?_ ?_
    all_goals refine ContinuousMap.dist_le dist_nonneg |>.mpr fun x ↦ ?_
    · simpa [halg.dist_eq] using ContinuousMap.dist_apply_le_dist _
    · let x' : σ S a := Subtype.map (algebraMap R S) (fun _ ↦ spectrum.algebraMap_mem S) x
      apply le_of_eq_of_le ?_ <| ContinuousMap.dist_apply_le_dist x'
      simp only [ContinuousMap.comp_apply, ContinuousMap.coe_mk, StarAlgHom.ofId_apply,
        halg.dist_eq, x']
      congr!
      all_goals ext; exact haf.left_inv _ |>.symm

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σₙ 𝕜 a
ha : p a
⊢ ‖x‖₊ ≤ ‖a‖₊

Tactic:
by
  simpa only [cfcₙ_id 𝕜 a] using! nnnorm_apply_le_nnnorm_cfcₙ (id : 𝕜 → 𝕜) a hx

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

Goal state before:
pp: A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable ℂ fun z ↦ resolvent a z
⊢ False

Tactic:
have H₃ := H₁.apply_eq_of_tendsto_cocompact 0 <| by
    simpa [Metric.cobounded_eq_cocompact] using resolvent_tendsto_cobounded a (𝕜 := ℂ)

Goal state after:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable ℂ fun z ↦ resolvent a z
H₃ : resolvent a 0 = 0
⊢ False
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U)

Tactic:
isOpen_iff_forall_mem_open

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
⊢ ∀ x ∈ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U, ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U, IsOpen t ∧ x ∈ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U)

Tactic:
isOpen_iff_forall_mem_open

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
⊢ ∀ x ∈ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U,
    ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U, IsOpen t ∧ x ∈ t
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case e'_5
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * NormedSpace.exp (-(star z • b)) = ↑(expUnitary (2 • ℑ (z • star b)))

Tactic:
simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_smul I I, sub_eq_add_neg]
    grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]

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

Goal state before:
pp: case e'_6
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (star z • a) * NormedSpace.exp (z • star (-a)) = ↑(expUnitary (2 • ℑ (star z • a)))

Tactic:
simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_smul I I, sub_eq_add_neg]
    grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
⊢ expMulMulExp a b x z = ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))

Tactic:
by
  let _ : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
  nth_rw 1 [expMulMulExp, ← (h.smul_right (star z)).exp_neg_mul_mul_exp_eq_self]
  simp_rw [← mul_assoc, mul_assoc (_ * _ * x)]
  congr!
  all_goals
    simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_smul I I, sub_eq_add_neg]
    grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : y ∈ B.polar Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖(B x) y‖ = ‖c‖ * (‖c‖⁻¹ * ‖(B x) y‖)

Tactic:
mul_inv_cancel_left₀ hc.ne'

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : y ∈ B.polar Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖(B x) y‖ = ‖(B x) y‖
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
s : AbsConvexOpenSets 𝕜 E
⊢ {y | gauge (↑s) y < 1} = ↑s

Tactic:
exact setOfPred_gauge_lt_one_eq_self_of_isOpen (s.coe_convex.lift ℝ) s.coe_zero_mem s.coe_isOpen

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
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ (gaugeSeminormFamily 𝕜 E).basisSets) id

Tactic:
refine (nhds_hasBasis_absConvex_open 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs => ?_

Goal state after:
case refine_1
𝕜 : 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
s : Set E
hs : 0 ∈ s ∧ IsOpen[inst✝⁷] s ∧ AbsConvex 𝕜 s
⊢ ∃ i' ∈ (gaugeSeminormFamily 𝕜 E).basisSets, id i' ⊆ id s

case refine_2
𝕜 : 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
s : Set E
hs : s ∈ (gaugeSeminormFamily 𝕜 E).basisSets
⊢ ∃ i, (0 ∈ i ∧ IsOpen[inst✝⁷] i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a)
⊢ IsStarNormal a

Tactic:
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

Goal state after:
case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a)
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
⊢ IsStarNormal a
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (((topDualPairing 𝕜 E).flip.flip.polar ∘ ⇑OrderDual.ofDual) ((topDualPairing 𝕜 E).flip.polar s))

Tactic:
simpa [LinearMap.flip_flip] using!
          (isClosed_polar _ _).preimage (ContinuousLinearMap.apply 𝕜 𝕜 (E := E)).continuous

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
fr : Dual ℝ E
p : Seminorm 𝕜 E
hp : ∀ (x : E), |fr x| ≤ p x
x : E
hx : ¬fr.extendRCLike x = 0
hsq : ‖fr.extendRCLike x‖ ^ 2 ≤ ‖fr.extendRCLike x‖ * p x
⊢ ‖fr.extendRCLike x‖ ≤ p x

Tactic:
exact (mul_le_mul_iff_left₀ (norm_pos_iff.2 hx)).1 <| by simpa [pow_two, mul_comm] using hsq

Goal state after:
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, 𝕜)
hI : IsClosed ↑I
⊢ I.IsMaximal ↔ ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Tactic:
refine
    ⟨?_, fun h =>
      let ⟨x, hx⟩ := h
      hx ▸ idealOf_compl_singleton_isMaximal 𝕜 x⟩
  intro hI'
  obtain ⟨x, hx⟩ := setOfIdeal_eq_compl_singleton I
  exact
    ⟨x, by
      simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using
        congr_arg (idealOfSet 𝕜) hx.symm⟩

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ (∃ f, f a = z) → z ∈ spectrum ℂ a

Tactic:
· rintro ⟨f, rfl⟩
    exact AlgHom.apply_mem_spectrum f a

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

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ spectralRadius ℂ ((gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)

Tactic:
unfold spectralRadius

Goal state after:
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ ⨆ k ∈ spectrum ℂ ((gelfandTransform ℂ A) (star a * a)), ↑‖k‖₊ = ⨆ k ∈ spectrum ℂ (star a * a), ↑‖k‖₊
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ UniformEquicontinuousOn f s

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn]
  rw [← lipschitzOnWith_ofFun_iff] at h
  exact h.uniformContinuousOn

Goal state after: