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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ LipschitzWith 2 ⇑(addEquiv 𝕜 A)

Tactic:
← Real.toNNReal_ofNat

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ LipschitzWith 2.toNNReal ⇑(addEquiv 𝕜 A)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)

Tactic:
have := congr(φ $(f.toNNReal_add_add_neg_add_neg_eq g))

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
this : φ ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = φ ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
⊢ ∀ ⦃a₂ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A⦄, φ.realContinuousMapZeroOfNNReal = a₂.realContinuousMapZeroOfNNReal → φ = a₂

Tactic:
ψ

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
⊢ φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal → φ = ψ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
f : C(X, ℝ≥0)₀
⊢ φ f = ψ f

Tactic:
simpa using congr($(h) ((ContinuousMapZero.mk ⟨toReal, continuous_coe⟩ rfl).comp f))

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
⊢ f ∈ A.topologicalClosure

Tactic:
have h_f_re : I f_re ∈ A.topologicalClosure := key ⟨f_re, rfl⟩

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
⊢ f ∈ A.topologicalClosure
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case l₂
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
| 𝓝 x

Tactic:
rw [← sub_zero x, ← zero_smul K 1, ← hxφ]

Goal state after:
case l₂
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
| 𝓝 (x - φ x • 1)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : ℕ → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
⊢ (f x₀ ∩ t).Nonempty

Tactic:
obtain ⟨y₀, hy₀, φ, hφ, hyφ⟩ := hK.subseq_of_frequently_in (x := y) <| by
    refine Eventually.frequently ?_
    filter_upwards [hx hf] with n hn
    exact hn (hy n).1

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : ℕ → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
y₀ : β
hy₀ : y₀ ∈ K
φ : ℕ → ℕ
hφ : StrictMono φ
hyφ : Tendsto (y ∘ φ) atTop (𝓝 y₀)
⊢ (f x₀ ∩ t).Nonempty
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
⊢ Continuous[inst✝¹, TopologicalSpace.vietoris β] f ↔
    (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
      ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)

Tactic:
by
  refine ⟨fun hf =>
      ⟨fun U hU => hU.powerset_vietoris.preimage hf, fun F hF => hF.powerset_vietoris.preimage hf⟩,
    fun ⟨h₁, h₂⟩ => ?_⟩
  rw [continuous_generateFrom_iff]
  rintro _ (⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩)
  · exact h₁ U hU
  · simp_rw [preimage_ofPred_eq, ← not_disjoint_iff_nonempty_inter, ← compl_ofPred,
      isOpen_compl_iff, ← subset_compl_iff_disjoint_right]
    exact h₂ Uᶜ hU.isClosed_compl

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht✝ : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
u : Set α
hu : u.Finite
ht : t ⊆ ⋃ y ∈ u, {x | (x, y) ∈ U}
⊢ ∃ t_1, t_1.Finite ∧ ∀ x ⊆ t, ∃ i, ∃ (_ : i ∈ t_1), x ∈ {x | (x, i) ∈ hausdorffEntourage U}

Tactic:
refine ⟨u.powerset, hu.powerset, fun s hs => ⟨u ∩ U.image s, by grind, fun x hx => ?_,
    fun x ⟨_, hx⟩ => hx⟩⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht✝ : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
u : Set α
hu : u.Finite
ht : t ⊆ ⋃ y ∈ u, {x | (x, y) ∈ U}
s : Set α
hs : s ⊆ t
x : α
hx : x ∈ (s, u ∩ U.image s).1
⊢ x ∈ U.preimage (s, u ∩ U.image s).2
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✝ : 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' := ⋯ }
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
exists L

Goal state after:
α : 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' := ⋯ }
⊢ f ≤ 𝓝 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_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ frontier ((σ 𝕜 ↑x)ᶜ ∩ σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
frontier_inter_subset,

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
this : CompleteSpace ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ frontier (σ 𝕜 ↑x)ᶜ ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 ↑x)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_1
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, 0 ≤ x
y : ℝ≥0
hy : ↑y ∈ spectrum ℝ a
hx : ↑t - ↑y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ ↑y
hyt : ↑y ≤ ↑t
⊢ ↑‖↑t - ↑y‖₊ ≤ ↑t

Tactic:
rw [← NNReal.coe_sub (by exact_mod_cast hyt)]

Goal state after:
case refine_1
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, 0 ≤ x
y : ℝ≥0
hy : ↑y ∈ spectrum ℝ a
hx : ↑t - ↑y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ ↑y
hyt : ↑y ≤ ↑t
⊢ ↑‖↑(t - y)‖₊ ≤ ↑t
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
ha : p a
⊢ IsGreatest ((fun x ↦ ‖x‖) '' σₙ 𝕜 a) ‖a‖

Tactic:
by
  simpa only [cfcₙ_id 𝕜 a] using! IsGreatest.norm_cfcₙ (id : 𝕜 → 𝕜) a

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 (spectralRadius ℂ a))

Tactic:
convert!
    (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
      (tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using 1

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ (fun _n ↦ ↑‖a‖₊) = (fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n ↦ 2 ^ n
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
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ ↑K
hxU : x ∈ U
M : Set α
hM : IsCompact M
right✝ : x ∈ interior M ∧ M ⊆ U ∩ interior L
⊢ M ⊆ L

Tactic:
by grind [interior_subset]

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

Goal state before:
pp: case pos
F : Type u_1
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ⇑f ⁻¹' closedBall 0 1
C : ℝ
hC : ⇑f '' K ⊆ closedBall 0 C
x✝ y x : α
hx : x ∈ K
⊢ f x ∈ closedBall 0 (max C 1)

Tactic:
exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝ : LocallyCompactSpace (NonemptyCompacts α)
x : α
U : Set α
hU : ↑{x} ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K | ↑K ⊆ interior U}
⊢ ∀ i ∈ K, ↑i ⊆ U

Tactic:
by grind [interior_subset]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
S : Subspace ℝ E
f : Dual ℝ ↥S
p : Seminorm ℝ E
hp : ∀ (x : ↥S), f x ≤ p ↑x
⊢ ?m.34

Tactic:
by
    refine exists_extension_of_le_sublinear ⟨S, f⟩ p (fun _ hc _ => ?_) ?_ hp
    · simp [map_smul_eq_mul, abs_of_nonneg hc.le]
    · exact fun x y => map_add_le_add p x y

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Completeness

Goal state before:
pp: case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f✝ g : E →SL[σ₁₂] F
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf : f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' s)
⊢ f ∈ closure[Pi.topologicalSpace] (range DFunLike.coe)

pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f✝ g : E →SL[σ₁₂] F
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf : f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' s)
⊢ ∃ C, ∀ (x : E'), ‖(linearMapOfMemClosureRangeCoe f ?refine_1) x‖ ≤ C * ‖x‖

Tactic:
· refine closure_mono (image_subset_iff.2 fun g _ => ?_) hf
    exact ⟨g, rfl⟩

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f✝ g : E →SL[σ₁₂] F
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf : f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' s)
⊢ ∃ C, ∀ (x : E'), ‖(linearMapOfMemClosureRangeCoe f ⋯) x‖ ≤ C * ‖x‖
Module: Mathlib.Analysis.Normed.Algebra.Basic

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : NormedField L
inst✝ : NormedAlgebra K L
F : IntermediateField K L
k : K
hk : 1 < ‖k‖
⊢ 1 < ‖(algebraMap K ↥F) k‖

Tactic:
simp [hk]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist ((lineMap p₁ p₂) c) p₂ = ‖1 - c‖ * dist p₁ p₂

Tactic:
dist_lineMap_right

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ ‖1 - c‖ * dist p₁ p₂ = ‖1 - c‖ * dist p₁ p₂
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
dist_midpoint_right

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ ‖2‖⁻¹ * dist p₁ p₂ = ‖2‖⁻¹ * dist p₁ p₂
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_5
F : Type u_7
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
f : WeakDual ℝ F
x : F
⊢ im ((extendRCLikeL f) x) = -f (I • x)

Tactic:
simp [extendRCLikeL_apply, extendRCLikeₗ_apply]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: 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ᶜ
P : Set X → Set X → Prop := fun C x ↦ IsCompact C
c u : Set X
c_comp : P c u
u_open : IsOpen[inst✝²] u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
ck : c ⊆ interior k
ku : k ⊆ u
A : closure[inst✝²] (interior k) ⊆ k
⊢ ∃ v, IsOpen[inst✝²] v ∧ c ⊆ v ∧ closure[inst✝²] v ⊆ u ∧ P c v ∧ P (closure[inst✝²] v) u

Tactic:
refine ⟨interior k, isOpen_interior, ck, A.trans ku, c_comp,
        k_comp.of_isClosed_subset isClosed_closure A⟩

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
x : X
hx : x ∈ mᶜ
n : ℕ
this : mᶜ ⊆ (U n ∩ interior m)ᶜ
⊢ (f n) x = 0

Tactic:
exact fm n (this hx)

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst✝¹] c
Pc : P c u0
⊢ IsOpen[inst✝¹] u0 → c ⊆ u0 → ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u0 ∧ P c v ∧ P (closure[inst✝¹] v) u0

Tactic:
u0IsOpen

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst✝¹] c
Pc : P c u0
u0IsOpen : IsOpen[inst✝¹] u0
⊢ c ⊆ u0 → ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u0 ∧ P c v ∧ P (closure[inst✝¹] v) u0
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c : Urysohns.CU P := { C := closure[inst✝¹] u, U := tᶜ, P_C_U := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
x : X
hx : x ∈ t
⊢ c.lim x = 1 x

Tactic:
apply Urysohns.CU.lim_of_notMem_U

Goal state after:
case h.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := ⋯
c : Urysohns.CU P := ⋯
x : X
hx : x ∈ t
⊢ x ∉ c.U
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 : ℝ
ha' : 0 ≤ ↑a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 ↑a
hz' : z⁻¹ = 0
⊢ False

Tactic:
exact spectrum.zero_notMem ℝ≥0 a.isUnit <| inv_eq_zero.mp hz' ▸ hz

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
⊢ sqrt 1 = 1

Tactic:
by simp [sqrt_eq_cfc]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ CFC.sqrt ↑a = ↑(CFC.sqrt a)

Tactic:
by_cases ha : 0 ≤ a <;> have ha' := by rwa [← Unitization.inr_nonneg_iff] at ha

Goal state after:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
ha' : 0 ≤ ↑a
⊢ CFC.sqrt ↑a = ↑(CFC.sqrt a)

case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
ha' : ¬0 ≤ ↑a
⊢ CFC.sqrt ↑a = ↑(CFC.sqrt a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : 0 ≤ a
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a

Tactic:
have : IsSelfAdjoint a := .of_nonneg ha

Goal state after:
A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : 0 ≤ a
this : IsSelfAdjoint a
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a