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

Goal state before:
pp: case refine_2
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁹ : CommSemiring R
inst✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst✝¹⁹, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁹, inst✝¹³] ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Continuous[_, inst✝¹³] (⇑(cfcₙHom hψa) ∘ fun g ↦ g.comp ι)

Tactic:
fun_prop

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

Goal state before:
pp: F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 ↑s).NeBot
hxφ : φ x = 0
⊢ Continuous[inst✝⁸, inst✝⁸] fun y ↦ y - φ y • 1

Tactic:
fun_prop

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

Goal state before:
pp: case e'_3
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ closure ↑(StarAlgebra.adjoin 𝕜 {Polynomial.X.toContinuousMapOn s}) = Set.univ

Tactic:
← Polynomial.toContinuousMapOnAlgHom_apply,

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ closure ↑(StarAlgebra.adjoin 𝕜 {(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X}) = Set.univ
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

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

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Ring A
inst✝¹⁸ : StarRing A
inst✝¹⁷ : TopologicalSpace A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁷, inst✝¹³] ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
⊢ Continuous[_, inst✝¹³] (⇑ψ ∘ ⇑(cfcHom ha))

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Ring A
inst✝¹⁸ : StarRing A
inst✝¹⁷ : TopologicalSpace A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁷, inst✝¹³] ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
⊢ Continuous[_, inst✝¹³] (⇑(cfcHom hψa) ∘ fun g ↦ g.comp ι)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
F : Set α
left✝ : (∅, F).1 ⊆ SetRel.preimage Set.univ (∅, F).2
hF : (∅, F).2 ⊆ SetRel.image Set.univ (∅, F).1
⊢ F ∈ {∅}

Tactic:
simpa using hF

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun r ↦ ↑ₐ r - a

Tactic:
fun_prop

Goal state after:
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
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ spectralRadius 𝕜 a < ↑‖↑u⁻¹‖₊

Tactic:
rwa [Units.val_inv_eq_inv_val, nnnorm_inv,
      coe_inv (nnnorm_ne_zero_iff.mpr (Units.val_mk0 hz ▸ hz : (u : 𝕜) ≠ 0)), lt_inv_iff_lt_inv]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompactSpace α
⊢ IsCompact Set.univ

Tactic:
by simpa [gi.l_surjective.range_eq]
    using isCompact_univ.image continuous_closure

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
this : {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} = ⋃ n, range '' univ.pi fun x ↦ s
n : ℕ+
⊢ ContinuousOn range (univ.pi fun x ↦ s)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : x ∈ ↑K
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
hy₂ : y ∈ closure[inst✝³.toTopologicalSpace] (UniformSpace.ball x U)
⊢ x ∈ U.preimage ↑L

Tactic:
(UniformSpace.isClosed_ball x hU₂).closure_eq

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : x ∈ ↑K
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
hy₂ : y ∈ UniformSpace.ball x U
⊢ x ∈ U.preimage ↑L
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ContinuousAt (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) μ

Tactic:
fun_prop

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
this : Continuous[_, instUniformSpace.toTopologicalSpace] ⇑(cfcₙAux ⋯ a ha)
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ ↑((cfcₙAux ⋯ a ha) x).toProd.2

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ (algebraMap ℝ ℂ) (Complex.reCLM x) = x

pp: case refine_2
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
⊢ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM → IsSelfAdjoint a

Tactic:
· have := eqOn_of_cfcₙ_eq_cfcₙ <|
      (cfcₙ_star (id : ℂ → ℂ) a).symm ▸ (cfcₙ_id ℂ a).symm ▸ ha.star_eq
    exact Complex.conj_eq_iff_re.mp (by simpa using this hx)

Goal state after:
case refine_2
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
⊢ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM → IsSelfAdjoint a
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

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

Tactic:
coe_nnnorm,

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

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

Tactic:
convexHull_prod

Goal state after:
s t : Set ℝ
⊢ ⇑equivRealProdLm ⁻¹' (convexHull ℝ) s ×ˢ (convexHull ℝ) t = (convexHull ℝ) s ×ℂ (convexHull ℝ) t
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 : α → β
⊢ Continuous[_, TopologicalSpace.vietoris α] fun x ↦ ↑x.1 ∪ ↑x.2

Tactic:
fun_prop

Goal state after:
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✝ : α → β
f : α → Compacts β
g : α → β → γ
hf : Continuous[inst✝², _] f
hg : Continuous[instTopologicalSpaceProd, inst✝] (Function.uncurry g)
x : α
⊢ Continuous[inst✝¹, inst✝] (g x)

Tactic:
fun_prop

Goal state after:
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 : α → Compacts β
g : α → β → γ
hf : Continuous[inst✝², _] f
hg : Continuous[instTopologicalSpaceProd, inst✝] (Function.uncurry g)
this : Continuous (Compacts.map (Function.uncurry g) hg)
⊢ Continuous[inst✝², _] fun x ↦ Compacts.map (Function.uncurry g) hg ({x} ×ˢ f x)

Tactic:
fun_prop

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
this : NormedAlgebra ℚ A
⊢ Continuous fun x ↦ exp (I • ↑x)

Tactic:
fun_prop

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

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
hKL : K ≤ L
⊢ ContinuousOn (fun x ↦ K ⊔ x) {K | (↑K).Nonempty ∧ ↑K ⊆ ↑L}

Tactic:
fun_prop

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

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ⇑f
⊢ Tendsto (⇑f) (cocompact α) (𝓝 0)

Tactic:
exact f.zero_at_infty'

Goal state after:
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✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this✝ : Fintype ↑u := hu'.fintype
this :
  {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite} =
    Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}
⊢ ContinuousOn Finset.univ.sup (univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U})

Tactic:
fun_prop

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 : ℂ
⊢ Differentiable ℂ fun z ↦ NormedSpace.exp (z • star b) * x * NormedSpace.exp (z • star (-a))

Tactic:
fun_prop

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

Goal state before:

Tactic:
‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
      rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
    _ ≤ ε * 1 := by gcongr; exact hy _ trivial
    _ = ε := mul_one _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]
  exact not_congr absConvexHull_eq_empty

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

Goal state before:
pp: 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)
a b : A
| deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 = a ^ 2 + 2 • (a * b) + b ^ 2

Tactic:
enter [1, 1, y, 1, x, 1]

Goal state after:
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)
a b : A
y x : ℝ
| NormedSpace.exp (x • a)
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 : α → β
⊢ Continuous fun x ↦ x.1.toCompacts ⊔ x.2.toCompacts

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Continuous fun x ↦ x.1.toCompacts ×ˢ x.2.toCompacts

Tactic:
fun_prop

Goal state after:
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✝ : α → β
f : α → NonemptyCompacts β
g : α → β → γ
hf : Continuous[inst✝², _] f
hg : Continuous[instTopologicalSpaceProd, inst✝] (Function.uncurry g)
x : α
⊢ Continuous[inst✝¹, inst✝] (g x)

Tactic:
fun_prop

Goal state after:
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 : α → NonemptyCompacts β
g : α → β → γ
hf : Continuous[inst✝², _] f
hg : Continuous[instTopologicalSpaceProd, inst✝] (Function.uncurry g)
⊢ Continuous[inst✝², _] fun x ↦ Compacts.map (g x) ⋯ (f x).toCompacts

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x ↦ r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2) • y - ((1 - r) / 2) • y = (fun x ↦ r • x) y

Tactic:
← sub_smul

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x ↦ r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2 - (1 - r) / 2) • y = (fun x ↦ r • x) y
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace (NonemptyCompacts α)
x : α
U : Set α
x✝ : x ∈ U ∧ IsOpen[inst✝] U
hx : x ∈ U
hU : IsOpen[inst✝] U
V : Set (NonemptyCompacts α)
hV₁ : IsOpen V
hV₂ : IsPreconnected V
hxV : {x} ∈ V
hKV : V ⊆ {K | ↑K ⊆ U}
⊢ ContinuousOn SetLike.coe V

Tactic:
fun_prop

Goal state after:
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.C
⊢ approx 0 c x = 0

Tactic:
exact indicator_of_notMem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
s : Set (WeakDual 𝕜 E)
⊢ IsVonNBounded 𝕜 s → Bornology.IsBounded s

Tactic:
intro h_vN

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
s : Set (WeakDual 𝕜 E)
h_vN : IsVonNBounded 𝕜 s
⊢ Bornology.IsBounded s
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SeparableSpace E
⊢ ∃ gs,
    (∀ (n : ℕ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (gs n)) ∧
      ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ n, gs n x ≠ gs n y

Tactic:
use (fun n φ ↦ φ (denseSeq E n))

Goal state after:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SeparableSpace E
⊢ (∀ (n : ℕ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((fun n φ ↦ φ (denseSeq E n)) n)) ∧
    ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ n, (fun n φ ↦ φ (denseSeq E n)) n x ≠ (fun n φ ↦ φ (denseSeq E n)) n y
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: α : Type u_4
𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst✝⁵ : TopologicalSpace α
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
g : α → WeakBilin B
h : ∀ (y : F), Continuous[inst✝⁵, _] fun a ↦ re ((B (g a)) y)
x : F
⊢ Continuous[inst✝⁵, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦
    ↑(re ((B (g a)) x)) - ↑(re ((B (g a)) (I • x))) * I

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ f ∉ idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0

Tactic:
simp_rw [mem_idealOfSet]; push Not; rfl

Goal state after: