mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } ∈ Ω^ N X x

Tactic:
rintro y ⟨i, iH | iH⟩

Goal state after:
case inl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
i : N
iH : y i = 0
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

case inr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
i : N
iH : y i = 1
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
⊢ ({ toFun := fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ },
          invFun := fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        ⟨{
            toFun := fun t ↦
              if ↑(t default) ≤ 2⁻¹ then
                q (Function.update t default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t default))))
              else p (Function.update t default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t default) - 1))),
            continuous_toFun := ⋯ },
          ⋯⟩)
      t =
    if ↑t ≤ 2⁻¹ then
      (Path.extend
          ({ toFun := fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ },
              invFun := fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ }
            q))
        (2 * ↑t)
    else
      (Path.extend
          ({ toFun := fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ },
              invFun := fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ }
            p))
        (2 * ↑t - 1)

Tactic:
refine ite_congr rfl (fun _ ↦ congrArg q ?_)
    fun _ ↦ congrArg p ?_
  <;> (ext i; rw [Unique.eq_default i]; simp)

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: E : Type u_3
inst✝ : EMetricSpace E
A : Set E
⊢ coveringNumber 0 A = A.encard

Tactic:
by
  refine le_antisymm (coveringNumber_le_encard_self A) ?_
  rw [← externalCoveringNumber_zero]
  exact externalCoveringNumber_le_coveringNumber 0 A

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (candidatesB X Y)

Tactic:
have : candidatesB X Y = (((((⋂ (x) (y), { f : Cb X Y | f (@inl X Y x, @inl X Y y) = dist x y }) ∩
      ⋂ (x) (y), { f : Cb X Y | f (@inr X Y x, @inr X Y y) = dist x y }) ∩
      ⋂ (x) (y), { f : Cb X Y | f (x, y) = f (y, x) }) ∩
      ⋂ (x) (y) (z), { f : Cb X Y | f (x, z) ≤ f (x, y) + f (y, z) }) ∩
      ⋂ x, { f : Cb X Y | f (x, x) = 0 }) ∩
      ⋂ (x) (y), { f : Cb X Y | f (x, y) ≤ maxVar X Y } := by
    ext
    simp only [candidatesB, candidates, mem_inter_iff, mem_iInter, mem_ofPred_eq]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (candidatesB X Y)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
⊢ coveringNumber (2 * ε) ∅ ≤ externalCoveringNumber ε ∅

pp: case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
· simp

Goal state after:
case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case mpr.inr.e_f
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
⊢ f = Function.const X (f hX.some)

Tactic:
simp [funext_iff, h _ hX.some]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x y z : Snowflaking X α hα₀ hα₁
⊢ edist (ofSnowflaking x) (ofSnowflaking z) ^ α ≤
    edist (ofSnowflaking x) (ofSnowflaking y) ^ α + edist (ofSnowflaking y) (ofSnowflaking z) ^ α

Tactic:
grw [edist_triangle x.ofSnowflaking y.ofSnowflaking z.ofSnowflaking,
      ENNReal.rpow_add_le_add_rpow _ _ hα₀.le hα₁]

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ lowerBasis α = (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Tactic:
lowerBasis,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ {s | ∃ t, t.Finite ∧ (↑(upperClosure t))ᶜ = s} = (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ

Tactic:
rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio]

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsUpper α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsUpper β
inst✝ : OrderTop β
⊢ IsLower (α × β)ᵒᵈ

Tactic:
exact instIsLowerProd (α := αᵒᵈ) (β := βᵒᵈ)

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ scottHausdorff α univ ≤ inst✝¹

Tactic:
rw [IsScott.topology_eq α univ, scott]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ scottHausdorff α univ ≤ upperSet α ⊔ scottHausdorff α univ
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)

pp: case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
⊢ (if p₀ ∈ unop U then A else ⊤_ C) = if p₀ ∈ unop V then A else ⊤_ C

Tactic:
rw [if_pos h, if_pos (by simpa using i.unop.le h)]

Goal state after:
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s t : Set X
hs : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
g : C(X, ℝ)
hg : t = ⇑g ⁻¹' {0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfg : ∀ (x : X), f x + g x ≠ 0
hp : s = (fun a ↦ f a / (f a + g a)) ⁻¹' {0}
this : t = (fun a ↦ f a / (f a + g a)) ⁻¹' {1}
⊢ SeparatedNhds s t

Tactic:
hp,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s t : Set X
hs : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
g : C(X, ℝ)
hg : t = ⇑g ⁻¹' {0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfg : ∀ (x : X), f x + g x ≠ 0
hp : s = (fun a ↦ f a / (f a + g a)) ⁻¹' {0}
this : t = (fun a ↦ f a / (f a + g a)) ⁻¹' {1}
⊢ SeparatedNhds ((fun a ↦ f a / (f a + g a)) ⁻¹' {0}) t
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj V)) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      (skyscraperPresheaf p₀ c).map inc

Tactic:
dsimp
    by_cases hV : p₀ ∈ V.unop
    · have hU : p₀ ∈ U.unop := leOfHom inc.unop hV
      split_ifs
      rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]
    · split_ifs
      exact ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext ..

Goal state after:
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: X✝ : TopCat
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
p₀ : ↑X
⊢ (forget C X ⋙ stalkFunctor C p₀).PreservesHomology

Tactic:
simp only [(forget C X ⋙ stalkFunctor C p₀).exact_tfae.out 2 0]
    intro S h
    have := ((forget C X ⋙ stalkFunctor C p₀).preservesFiniteColimits_tfae.out 3 0).mp
      (inferInstance : (PreservesFiniteColimits _))
    refine ShortComplex.ShortExact.mk' (this S h).left ?_ (this S h).right
    have := h.2
    exact Functor.map_mono (forget C X ⋙ stalkFunctor C p₀) _

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∈ unop U
⊢ 𝓕.germ (unop U) p₀ h ≫ fromStalk p₀ f ≫ eqToHom ⋯ = f.app U

pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∉ unop U
⊢ (⋯ ▸ terminalIsTerminal).from (𝓕.obj U) = f.app U

Tactic:
· simp

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∉ unop U
⊢ (⋯ ▸ terminalIsTerminal).from (𝓕.obj U) = f.app U
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map (WalkingParallelPairHom.id WalkingParallelPair.one)

Tactic:
· simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
⊢ ⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g

Tactic:
have Hcf : ∀ x, cf ≤ f x := fun x => hcf (mem_range_self x)

Goal state after:
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
⊢ ⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
⊢ ⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g

Tactic:
have Hcf : ∀ x, cf ≤ f x := fun x => hcf (mem_range_self x)

Goal state after:
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
⊢ ⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ (fun p ↦ dist p.1 p.2) ∈ candidates X Y

Tactic:
simp_rw [candidates, Set.mem_ofPred_eq, dist_comm, dist_triangle, dist_self, maxVar_bound,
    forall_const, and_true]

Goal state after:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ (∀ (x y : X), dist (inl x) (inl y) = dist x y) ∧ ∀ (x y : Y), dist (inr x) (inr y) = dist x y
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ ⊥ < ↑0

pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ ⊥ ∈ {n | ∀ (i : ℕ), n < ↑i → HasSmallInductiveDimensionLT X i}

Tactic:
· simp

Goal state after:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ ⊥ ∈ {n | ∀ (i : ℕ), n < ↑i → HasSmallInductiveDimensionLT X i}
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
h : HasSmallInductiveDimensionLT X (n + 1)
⊢ smallInductiveDimension X < ↑(n + 1)

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
⊢ ?m.78

Tactic:
refine zorn_subset_nonempty 𝒮 (fun c hc𝒮 hc hne@⟨x, hxc⟩ ↦ ?_) s hs

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
x✝ hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h✝ : hne = ⋯
⊢ ∃ ub ∈ 𝒮, ∀ s ∈ c, s ⊆ ub
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
x✝ hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h✝ : hne = ⋯
⊢ ⋃₀ c ⊆ 𝔅

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
x✝ hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h✝ : hne = ⋯
⊢ ⋂₀ ⋃₀ c = ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case pos
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
⊢ hZ_irred.genericPoint ∈ ⋂₀ B

Tactic:
Set.mem_sInter

Goal state after:
case pos
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
⊢ ∀ t ∈ B, hZ_irred.genericPoint ∈ t
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
⊢ insert i a ⊆ B

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsPreirreducible Z
Y₁ Y₂ : Set X
hY₁_cl : IsClosed[inst✝⁴] Y₁
hY₂_cl : IsClosed[inst✝⁴] Y₂
hc₁ : IsCompact Y₁ᶜ
hc₂ : IsCompact Y₂ᶜ
hsub : Z ⊆ Y₁ ∪ Y₂
x₁ : X
hx₁ : x₁ ∈ Z ∩ Y₁ᶜ
x₂ : X
hx₂ : x₂ ∈ Z ∩ Y₂ᶜ
⊢ False

Tactic:
have hY₁ : Y₁ ∈ 𝔅 := .inr ⟨hY₁_cl, hc₁⟩

Goal state after:
case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsPreirreducible Z
Y₁ Y₂ : Set X
hY₁_cl : IsClosed[inst✝⁴] Y₁
hY₂_cl : IsClosed[inst✝⁴] Y₂
hc₁ : IsCompact Y₁ᶜ
hc₂ : IsCompact Y₂ᶜ
hsub : Z ⊆ Y₁ ∪ Y₂
x₁ : X
hx₁ : x₁ ∈ Z ∩ Y₁ᶜ
x₂ : X
hx₂ : x₂ ∈ Z ∩ Y₂ᶜ
hY₁ : Y₁ ∈ 𝔅
⊢ False