mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : TopologicalSpace A
inst✝¹ : Module 𝕜 A
inst✝ : Subsingleton A
φ : ↑(characterSpace 𝕜 A)
x : A
⊢ ↑φ 0 = 0 0

Tactic:
map_zero,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : TopologicalSpace A
inst✝¹ : Module 𝕜 A
inst✝ : Subsingleton A
φ : ↑(characterSpace 𝕜 A)
x : A
⊢ 0 = 0 0
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case smul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ : C(↑s, 𝕜)
r : 𝕜
f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ r • (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0

Tactic:
hf,

Goal state after:
case smul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ : C(↑s, 𝕜)
r : 𝕜
f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ r • 0 = 0
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case star
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ star ((evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f) = 0

Tactic:
hf,

Goal state after:
case star
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ star 0 = 0
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
⊢ { toFun := fun φ ↦ φ 0, continuous_toFun := ⋯ } = 0

Tactic:
ext; simp only [map_zero, coe_mk, coe_zero, Pi.zero_apply]

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

Goal state before:
pp: case add
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Fact (0 ∈ s)
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id s}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f x✝ y✝ : C(↑s, 𝕜)₀
hx✝ : x✝ ∈ NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})
hy✝ : y✝ ∈ NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})
hf : p x✝
hg : p y✝
⊢ p (x✝ + y✝)

Tactic:
| add _ _ _ _ hf hg =>

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Fact (0 ∈ s)
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id s}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f : C(↑s, 𝕜)₀
⊢ p f

Tactic:
by
  refine closure (fun f hf => ?_) f
  induction hf using NonUnitalAlgebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq] at hf
    obtain (rfl | rfl) := hf
    all_goals assumption
  | zero => exact zero
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg
  | smul _ _ _ hf => exact smul _ _ hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ (a : Set β),
    IsOpen[inst✝] a → ((f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, a ∈ 𝓝ˢ (f x')) ↔ f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ a)

Tactic:
simp +contextual [← subset_interior_iff_mem_nhdsSet, IsOpen.interior_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ ↑t, {x | (x, y) ∈ Prod.swap ⁻¹' U}
x : α
hx : x ∈ ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2
⊢ x ∈ U.image ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1

Tactic:
obtain ⟨y, hy, hxy⟩ := Set.mem_iUnion₂.mp (ht₂ hx)

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ ↑t, {x | (x, y) ∈ Prod.swap ⁻¹' U}
x : α
hx : x ∈ ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2
y : α
hy : y ∈ ↑t
hxy : x ∈ {x | (x, y) ∈ Prod.swap ⁻¹' U}
⊢ x ∈ U.image ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1
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) ≤ ε⁻¹
n : ℕ
⊢ spectralRadius 𝕜 a ≤ ↑‖a ^ (n + (N + 1))‖₊ ^ (1 / ↑(n + (N + 1))) * ε⁻¹

Tactic:
simp only [← add_assoc]

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) ≤ ε⁻¹
n : ℕ
⊢ spectralRadius 𝕜 a ≤ ↑‖a ^ (n + N + 1)‖₊ ^ (1 / ↑(n + N + 1)) * ε⁻¹
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
this : {U | IsOpen[inst✝¹] U} = (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}
⊢ generateFrom
      ((fun x ↦ {t | t ⊆ f ⁻¹' x}) '' {V | IsOpen[inst✝] V} ∪
        (fun x ↦ {s | (s ∩ f ⁻¹' x).Nonempty}) '' {V | IsOpen[inst✝] V}) =
    generateFrom
      ((fun a ↦ {a_1 | f '' a_1 ⊆ a}) '' {V | IsOpen[inst✝] V} ∪
        (fun a ↦ {a_1 | (f '' a_1 ∩ a).Nonempty}) '' {V | IsOpen[inst✝] V})

Tactic:
image_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
this : {U | IsOpen[inst✝¹] U} = (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}
⊢ generateFrom
      ((fun x ↦ {t | t ⊆ f ⁻¹' x}) '' {V | IsOpen[inst✝] V} ∪
        (fun x ↦ {s | (s ∩ f ⁻¹' x).Nonempty}) '' {V | IsOpen[inst✝] V}) =
    generateFrom
      ((fun x ↦ {t | t ⊆ f ⁻¹' x}) '' {V | IsOpen[inst✝] V} ∪
        (fun a ↦ {a_1 | (f '' a_1 ∩ a).Nonempty}) '' {V | IsOpen[inst✝] V})
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal

Tactic:
refine ⟨fun ha ↦ ⟨.of_nonneg ha, .nnreal_of_nonneg ha⟩, ?_⟩

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal → 0 ≤ a
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
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
⊢ ‖cfcₙ f a‖ < c

Tactic:
refine cfcₙ_cases (‖·‖ < c) a f ?_ fun hf hf0 ha ↦ ?_
  · simpa using (norm_nonneg _).trans_lt <| h 0 (quasispectrum.zero_mem 𝕜 a)
  · simp only [← cfcₙ_apply f a, (IsGreatest.norm_cfcₙ f a hf hf0 ha |>.lt_iff)]
    rintro - ⟨x, hx, rfl⟩
    exact h x 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
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
⊢ f x = ↑(f ↑x.re).re

Tactic:
RCLike.star_def,

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
hf_real : ∀ x ∈ σ ℂ a, (starRingEnd ℂ) (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
⊢ 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
hf_real : ∀ x ∈ σₙ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ f x = ↑(f ↑x.re).re

Tactic:
RCLike.star_def,

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
hf_real : ∀ x ∈ σₙ ℂ a, (starRingEnd ℂ) (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ f x = ↑(f ↑x.re).re
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ IsConnected s

Tactic:
by
  refine .subset_closure ?_ hs₁ (by simpa only [closure_setOfPred_im_lt] using hs₂)
  exact (convex_halfSpace_im_lt r).isConnected ⟨(r - 1) * I, by simp⟩

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
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ liminf (fun i ↦ (↑‖a ^ i‖₊ ^ (1 / ↑i))⁻¹) atTop

Tactic:
← one_div

Goal state after:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ liminf (fun i ↦ 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ 0 ≤ ‖↑f‖

Tactic:
by positivity

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✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ 0 ≤ ‖(↑f).comp ι‖

Tactic:
by positivity

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✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ‖(↑f).comp ι‖ = ‖↑f‖

Tactic:
apply le_antisymm (ContinuousMap.norm_le _ (by positivity) |>.mpr ?_)
      (ContinuousMap.norm_le _ (by positivity) |>.mpr ?_)

Goal state after:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σ 𝕜 a)), ‖((↑f).comp ι) x‖ ≤ ‖↑f‖

𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σₙ 𝕜 a)), ‖↑f x‖ ≤ ‖(↑f).comp ι‖
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✝ : DiscreteTopology α
K : Compacts α
⊢ {K} = {K_1 | ↑K_1 ⊆ ↑K} ∩ {x | ∀ i ∈ ↑K, (↑x ∩ {i}).Nonempty}

Tactic:
inter_singleton_nonempty,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : DiscreteTopology α
K : Compacts α
⊢ {K} = {K_1 | ↑K_1 ⊆ ↑K} ∩ {x | ∀ i ∈ ↑K, i ∈ ↑x}
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✝ : RegularSpace α
⊢ RegularSpace (Compacts α)

Tactic:
by
  simp_rw [regularSpace_generateFrom induced_generateFrom_eq, image_union, image_image, powerset,
    preimage_ofPred_eq, Filter.disjoint_iff]
  rintro _ (⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩) K hK
  · obtain ⟨V, W, hV, hW, hKV, hUW, hVW⟩ :=
      SeparatedNhds.of_isCompact_isClosed K.isCompact hU.isClosed_compl
        (disjoint_compl_right_iff_subset.mpr hK)
    refine ⟨{K | (↑K ∩ W).Nonempty}, ?_, {K | ↑K ⊆ V},
      (isOpen_subsets_of_isOpen hV).mem_nhds_iff.mpr hKV, by grind [Set.Nonempty]⟩
    simp_rw [(isOpen_inter_nonempty_of_isOpen hW).mem_nhdsSet, compl_ofPred,
      ← inter_compl_nonempty_iff]
    grw [hUW]
  · obtain ⟨x, hx₁, hx₂⟩ := hK
    obtain ⟨V, W, hV, hW, hxV, hUW, hVW⟩ :=
      SeparatedNhds.of_isCompact_isClosed (isCompact_singleton (x := x)) hU.isClosed_compl
        (by simpa)
    refine ⟨{K | ↑K ⊆ W}, ?_, {K | (↑K ∩ V).Nonempty}, ?_, by grind [Set.Nonempty]⟩
    · simp_rw [(isOpen_subsets_of_isOpen hW).mem_nhdsSet, compl_ofPred, not_nonempty_iff_eq_empty,
        ← disjoint_iff_inter_eq_empty, ← subset_compl_iff_disjoint_right]
      gcongr
    · rw [(isOpen_inter_nonempty_of_isOpen hV).mem_nhds_iff]
      exact ⟨x, hx₁, hxV <| Set.mem_singleton x⟩

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

Goal state before:
pp: case neg
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 <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)

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

Goal state before:
pp: case a
α : 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 := ⋯
⊢ (Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite}

Tactic:
image_subset_iff,

Goal state after:
case a
α : 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
⊢ (univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    Finset.univ.sup ⁻¹' {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite}
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
⊢ 0 ≤ (1 + r) / 2

Tactic:
by positivity

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
⊢ 0 ≤ (1 - r) / 2

Tactic:
by positivity

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

Goal state before:
pp: 𝕜 : 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‖
⊢ 0 < ‖x‖

Tactic:
by positivity

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

Goal state before:
pp: 𝕜 : 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‖
⊢ 0 ≤ ‖x‖⁻¹

Tactic:
by positivity

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

Goal state before:
pp: 𝕜 : 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‖
y : ↥(𝕜 ∙ x)
⊢ 0 < ‖x‖

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous[⨅ i, induced (⇑(f i)) t𝕜, t𝕜] ⇑φ

Tactic:
by
  let _ := ⨅ i, induced (f i) t𝕜
  constructor
  · exact Submodule.span_induction
      (Set.forall_mem_range.mpr fun i ↦ continuous_iInf_dom continuous_induced_dom) continuous_zero
      (fun _ _ _ _ ↦ .add) (fun c _ _ h ↦ h.const_smul c)
  · intro φ_cont
    refine mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_
    simp_rw [Submodule.mem_iInf, LinearMap.mem_ker] at hx ⊢
    have : Inseparable x 0 := by
      -- Maybe missing lemmas about `Inseparable`?
      simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
    simpa only [map_zero] using (this.map φ_cont).eq

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

Goal state before:
pp: 𝕜 : 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 : ‖x‖ ≤ ‖g‖ * ‖x‖
⊢ 0 < ‖x‖

Tactic:
by positivity

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𝕜
this : IsTopologicalAddGroup E
⊢ ⨅ i, Filter.comap (⇑(f i)) (𝓝 ((f i) 0)) = ⨅ i, Filter.comap (⇑(f i).toSeminorm) (𝓝 0)

Tactic:
map_zero,

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𝕜
this : IsTopologicalAddGroup E
⊢ ⨅ i, Filter.comap (⇑(f i)) (𝓝 0) = ⨅ i, Filter.comap (⇑(f i).toSeminorm) (𝓝 0)
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx n c x
c : CU P
⊢ 0 ≤ approx (n + 1) c x

Tactic:
simp only [approx, midpoint_eq_smul_add]
    refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : x ∈ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x

Tactic:
calc
      approx n₂ c₂ x = 0 := approx_of_mem_C _ _ (h hx)
      _ ≤ approx n₁ c₁ x := approx_nonneg _ _ _

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
h : x ∉ c.U
⊢ c.lim x = 1

Tactic:
simp only [CU.lim, approx_of_notMem_U c _ h, ciSup_const]

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

Goal state before:
pp: case refine_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ⊆ s
f : C(X, R)
hf : f ∈ I
h' : f ∉ idealOfSet R s
⊢ False

Tactic:
rcases notMem_idealOfSet.mp h' with ⟨x, hx, hfx⟩

Goal state after:
case refine_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ⊆ s
f : C(X, R)
hf : f ∈ I
h' : f ∉ idealOfSet R s
x : X
hx : x ∈ sᶜ
hfx : f x ≠ 0
⊢ False