mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : α → Set β
⊢ HasOpenLowerSections f ↔ ∀ (b : β), IsClosed[inst✝] (f ⁻¹' Iic {b}ᶜ)

Tactic:
simp_rw [← isOpen_compl_iff]
  exact hasOpenLowerSections_iff_isOpen_compl_preimage_Iic_compl

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

Goal state before:
pp: case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
⊢ (s₁, s₃) ∈ hausdorffEntourage (U ○ V)

Tactic:
grw [mem_hausdorffEntourage, preimage_comp, ← h₂₃, ← h₁₂, image_comp, ← h₂₁, ← h₃₂]

Goal state after:
case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
⊢ s₁ ⊆ s₁ ∧ s₃ ⊆ s₃
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s}

Tactic:
by
  rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩
  · convert isPreconnected_empty
    grind [Set.not_nonempty_empty]
  suffices {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} =
      ⋃ n : ℕ+, range (ι := Fin n) '' Set.pi univ fun _ => s by
    rw [this]
    /- The family of nonempty subsets of `s` with at most `n` elements is connected, since it is the
    image of `sⁿ` under the continuous map `(x₁, …, xₙ) ↦ {x₁, …, xₙ}`. It follows that their union
    over `n ≥ 1` is also connected. -/
    exact isPreconnected_iUnion
      ⟨{x}, mem_iInter_of_mem fun n => ⟨fun _ => x, by simpa⟩⟩
      (fun n => .image (isPreconnected_univ_pi fun _ => hs) _ (by fun_prop))
  refine subset_antisymm (fun t ht => ?_)
    (iUnion_subset fun _ => image_subset_iff.mpr fun f hf =>
      ⟨range_nonempty _, finite_range _, by grind⟩)
  obtain ⟨ht₁, ht₂, hts⟩ := ht
  obtain ⟨n, f, -, rfl⟩ := ht₂.fin_param
  rw [range_subset_iff] at hts
  rw [range_nonempty_iff_nonempty] at ht₁
  lift n to ℕ+ using Fin.pos'
  exact mem_iUnion_of_mem n <| mem_image_of_mem _ <| mem_univ_pi.mpr hts

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
⊢ x ∈ U.preimage ↑L

Tactic:
have hy₁ : ClusterPt y l := .of_inf_left hy

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
⊢ x ∈ U.preimage ↑L
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case neg
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : ¬t ⊆ U ∧ ¬t ⊆ V
htU : ¬Disjoint t U
htV : ¬Disjoint t V
⊢ (⋃₀ s ∩ (U ∩ V)).Nonempty

Tactic:
rw [not_disjoint_iff_nonempty_inter] at htU htV

Goal state after:
case neg
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : ¬t ⊆ U ∧ ¬t ⊆ V
htU : (t ∩ U).Nonempty
htV : (t ∩ V).Nonempty
⊢ (⋃₀ s ∩ (U ∩ V)).Nonempty
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: case refine_2
𝕜 : 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
a : A
ha : p a
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ IsClosed[Unitization.instUniformSpace.toTopologicalSpace]
    ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))

Tactic:
simp only [NonUnitalStarAlgHom.coe_range]

Goal state after:
case refine_2
𝕜 : 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
a : A
ha : p a
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ IsClosed[Unitization.instUniformSpace.toTopologicalSpace] (Set.range ⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A))
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
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (σ 𝕜 x) \ σ 𝕜 ↑x ∪ ∅)

Tactic:
sdiff_eq_compl_inter,

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
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((σ 𝕜 ↑x)ᶜ ∩ interior (σ 𝕜 x) ∪ ∅)
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:
sdiff_eq_compl_inter,

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)ᶜ ∩ σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: case right.right
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfcₙ (fun x ↦ √x) a * cfcₙ (fun x ↦ √x) a = a

Tactic:
rw [← cfcₙ_mul ..]
    nth_rw 2 [← cfcₙ_id ℝ a]
    apply cfcₙ_congr fun x hx ↦ ?_
    rw [QuasispectrumRestricts.nnreal_iff] at ha₂
    apply ha₂ x at hx
    simp [← sq, Real.sq_sqrt hx]

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : T2Space A
f : ℂ → ℂ
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
hf_real : ∀ x ∈ σ ℂ a, ↑(RCLike.re (f x)) = f x
⊢ f x = ↑(f ↑x.re).re

Tactic:
RCLike.re_eq_complex_re,

Goal state after:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : T2Space A
f : ℂ → ℂ
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
hf_real : ∀ x ∈ σ ℂ a, ↑(f x).re = f x
⊢ f x = ↑(f ↑x.re).re
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: 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✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
f : ℂ → ℂ
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
hf_real : ∀ x ∈ σₙ ℂ a, ↑(RCLike.re (f x)) = f x
⊢ f x = ↑(f ↑x.re).re

Tactic:
RCLike.re_eq_complex_re,

Goal state after:
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✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
f : ℂ → ℂ
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
hf_real : ∀ x ∈ σₙ ℂ a, ↑(f x).re = f x
⊢ f x = ↑(f ↑x.re).re
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: z w : ℂ
⊢ (convexHull ℝ) (⇑equivRealProd ⁻¹' (Prod.mk z.re '' {z.im, w.im} ∪ Prod.mk w.re '' {z.im, w.im})) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}

Tactic:
image_pair,

Goal state after:
z w : ℂ
⊢ (convexHull ℝ) (⇑equivRealProd ⁻¹' ({(z.re, z.im), (z.re, w.im)} ∪ {(w.re, z.im), (w.re, w.im)})) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
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
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ ‖(cfcHom ha) { toFun := (σ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ }‖₊ < c

Tactic:
simp only [← cfc_apply f a, (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.lt_iff)]

Goal state after:
case inr
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
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ ∀ x ∈ f '' σ ℝ≥0 a, x < c
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
· exact IsSelfAdjoint.mul_star_self a

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)
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
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ expUnitary (a + b) = expUnitary a * expUnitary b

Tactic:
by
  let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
  simpa only [Subtype.ext_iff, expUnitary_coe, AddSubgroup.coe_add, smul_add] using!
    exp_add_of_commute ((h.smul_left I).smul_right I)

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✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
huU : {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ⊆ U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ∧ IsCompact s

Tactic:
clear U huU

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ∧ IsCompact s
Module: Mathlib.Topology.Sets.VietorisTopology

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

Tactic:
by gcongr; grind

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:
LinearMap.smul_apply,

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‖ = ‖c‖ * ‖c⁻¹ • (B x) y‖
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : Module ℝ E := restrictScalars ℝ 𝕜 E
this : IsScalarTower ℝ 𝕜 E := IsScalarTower.restrictScalars ℝ 𝕜 E
fr : Dual ℝ ↥S := reLm ∘ₗ ↑ℝ f
g : Dual ℝ E
hg : ∀ (x : ↥S), g ↑x = fr x
hgp : ∀ (x : E), |g x| ≤ (Seminorm.restrictScalars ℝ p) x
x : E
⊢ ‖g.extendRCLike x‖ ≤ p x

Tactic:
· apply norm_extendRCLike_le_seminorm
    exact hgp

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

Goal state before:
pp: case refine_2
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hval : g x = ↑‖x‖
⊢ 1 ≤ ‖g‖

Tactic:
have hle := g.le_opNorm x

Goal state after:
case refine_2
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hval : g x = ↑‖x‖
hle : ‖g x‖ ≤ ‖g‖ * ‖x‖
⊢ 1 ≤ ‖g‖
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
this : Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ
⊢ φ ∈ ⨆ i, 𝕜 ∙ f i ↔ ∃ s, φ ∈ ⨆ i ∈ s, 𝕜 ∙ f i

Tactic:
rw [Submodule.mem_iSup_iff_exists_finset]

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

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ

Tactic:
WithSeminorms.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜),

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ (∀ (i : Fin 1), Continuous[t₁, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)) ↔
    ∃ s, ∀ (i : Fin 1), Continuous[t₂ s, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)
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
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖

Tactic:
eq z

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹‖ * ‖x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: case mp
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
H : Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ
⊢ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
WithSeminorms.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜),

Goal state after:
case mp
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
H : ∀ (i : Fin 1), Continuous[⨅ i, induced (⇑(f i)) inferInstance, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)
⊢ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm
Module: Mathlib.Analysis.Normed.Module.WeakDual

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

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:
· exact fun h => ((NormedSpace.isVonNBounded_iff 𝕜).mpr h).of_topologicalSpace_le
      Dual.dual_norm_topology_le_weak_dual_topology

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)
⊢ IsVonNBounded 𝕜 s → Bornology.IsBounded s
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r r' : k
h : a < b
⊢ r • (b - a) + a < r' • (b - a) + a ↔ r < r'

Tactic:
add_lt_add_iff_right,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r r' : k
h : a < b
⊢ r • (b - a) < r' • (b - a) ↔ r < r'
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔ f (r * (b - a) + a) ≤ r • (f b - f a + r⁻¹ • f a)

Tactic:
smul_add,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔ f (r * (b - a) + a) ≤ r • (f b - f a) + r • r⁻¹ • f a