mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ ⋃₀ S = univ

Tactic:
exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ instTopologicalSpaceProd = lower (α × β)

Tactic:
refine le_antisymm (le_generateFrom ?_) ?_
    · rintro _ ⟨x, rfl⟩
      exact (isClosed_Ici.prod isClosed_Ici).isOpen_compl
    rw [(IsLower.isTopologicalBasis.prod
      IsLower.isTopologicalBasis).eq_generateFrom, le_generateFrom_iff_subset_isOpen,
      image2_subset_iff]
    rintro _ ⟨s, hs, rfl⟩ _ ⟨t, ht, rfl⟩
    dsimp
    simp_rw [coe_upperClosure, compl_iUnion, prod_eq, preimage_iInter, preimage_compl]
    -- without `let`, `refine` tries to use the product topology and fails
    let _ : TopologicalSpace (α × β) := lower (α × β)
    refine (hs.isOpen_biInter fun a _ => ?_).inter (ht.isOpen_biInter fun b _ => ?_)
    · exact GenerateOpen.basic _ ⟨(a, ⊥), by simp [Ici_prod_eq, prod_univ]⟩
    · exact GenerateOpen.basic _ ⟨(⊥, b), by simp [Ici_prod_eq, univ_prod]⟩

Goal state after:
Module: Mathlib.Topology.Order.Category.AlexDisc

Goal state before:
pp: X : AlexDisc
⊢ ↑X.toTopCat ≃ₜ WithUpperSet ↑(topToPreord.obj ((forget₂ AlexDisc TopCat).obj X))

Tactic:
exact homeoWithUpperSetTopologyorderIso X

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

Goal state before:
pp: case h
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
a : α
ha' : (hull T a)ᶜ = R
⊢ {a}.Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure {a}))ᶜ = Subtype.val ⁻¹' Subtype.val '' (hull T a)ᶜ

Tactic:
simp only [finite_singleton, upperClosure_singleton, UpperSet.coe_Ici, image_val_compl,
      Subtype.image_preimage_coe, sdiff_self_inter, preimage_sdiff, Subtype.coe_preimage_self,
      true_and]

Goal state after:
case h
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
a : α
ha' : (hull T a)ᶜ = R
⊢ (Subtype.val ⁻¹' Ici a)ᶜ = univ \ Subtype.val ⁻¹' Ici a
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝¹ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q < 0
y : α
hy : y ⋖ x
x✝ : α
⊢ x✝ ∈ ⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩ ↔ x✝ ∈ Ioi y

Tactic:
simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_right

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
⊢ IsOpen[inst✝] s → IsOpen[inst✝¹] (f.preimage s)

Tactic:
os

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst✝] s
⊢ IsOpen[inst✝¹] (f.preimage s)
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen[scott α univ] U}
⊢ lower α = induced (⇑WithLower.toLower) WithLower.instTopologicalSpace

Tactic:
let _ := lower α
    exact (@IsLower.withLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩).isInducing.eq_induced

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝³ : 0 ≤ ε₂
this✝² : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝²
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝¹ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
⊢ hausdorffDist univ s ≤ ε₁

Tactic:
have : 0 ≤ ε₁ := le_trans dist_nonneg Dxs

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁴ : 0 ≤ ε₂
this✝³ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝³
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝² : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝¹ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : 0 ≤ ε₁
⊢ hausdorffDist univ s ≤ ε₁
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
⊢ IsSheafOpensLeCover (principalsKanExtension F)

Tactic:
intro ι Us

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
ι : Type v
Us : ι → Opens ↑X
⊢ Nonempty (IsLimit ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op))
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 = ∅}
h𝒮 : 𝒮.Nonempty
⊢ False

Tactic:
obtain ⟨s, hs⟩ := h𝒮

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 ∈ 𝒮
⊢ False
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ↑I
h : t₀ ≤ t₁
⊢ range ⇑(γ.subpath t₀ t₁) = ⇑γ '' Icc t₀ t₁

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ↑I
h : t₁ ≤ t₀
⊢ range ⇑(γ.subpath t₀ t₁) = ⇑γ '' Icc t₁ t₀

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ IsUltraUniformity X

Tactic:
refine .mk_of_hasBasis (h.hasBasis.comap (Prod.map f f)) ?_ ?_

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map f f ⁻¹' id i)

case refine_2
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map f f ⁻¹' id i)