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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ (∃ x_1 ∈ s, S.domRestrict x_1 = x) →
    ∃ a,
      (∃ x ∈ s, Sᶜ.domRestrict x = a) ∧
        ∃ a_1 ∈ s, ((∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict a_1) ∧ Sᶜ.domRestrict a_1 = a) ∧ (fun i ↦ a_1 ↑i) = x

Tactic:
rintro ⟨z, hz_mem, hzx⟩

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
z : (a : ι) → α a
hz_mem : z ∈ s
hzx : S.domRestrict z = x
⊢ ∃ a,
    (∃ x ∈ s, Sᶜ.domRestrict x = a) ∧
      ∃ a_1 ∈ s, ((∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict a_1) ∧ Sᶜ.domRestrict a_1 = a) ∧ (fun i ↦ a_1 ↑i) = x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i ≤ x

Tactic:
have h_mem := cantorSequence_mem_cantorSet hx n
  rw [cantorSequence_eq_self_sub_sum_cantorToTernary x n] at h_mem
  apply cantorSet_subset_unitInterval at h_mem
  simp only [Set.mem_Icc] at h_mem
  simpa using! h_mem.left

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case ha
y : ℕ → Bool
x : ℝ := ⋯
this : ofDigits (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = ofDigits fun i ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get n ≠ 1

pp: case hb
y : ℕ → Bool
x : ℝ := ⋯
this : ofDigits (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = ofDigits fun i ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), (bif y n then 2 else 0) ≠ 1

pp: y : ℕ → Bool
x : ℝ := ofDigits fun i ↦ bif y i then 2 else 0
this : (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = fun i ↦ bif y i then 2 else 0
⊢ (cantorToBinary x).get = y

Tactic:
· exact fun n ↦ cantorToTernary_ne_one

Goal state after:
case hb
y : ℕ → Bool
x : ℝ := ⋯
this : ofDigits (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = ofDigits fun i ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), (bif y n then 2 else 0) ≠ 1

y : ℕ → Bool
x : ℝ := ofDigits fun i ↦ bif y i then 2 else 0
this : (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = fun i ↦ bif y i then 2 else 0
⊢ (cantorToBinary x).get = y
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α) (a : α),
    Tendsto length (𝓝 l) (pure l.length) → Tendsto (fun p ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Tactic:
intro l a ih
    dsimp only [List.length]
    refine Tendsto.comp (tendsto_pure_pure (fun x => x + 1) _) ?_
    exact Tendsto.comp ih tendsto_snd

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

Goal state before:
pp: case inr
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ f, Isometry f

Tactic:
exact ⟨embeddingOfSubset x, embeddingOfSubset_isometry x (S_dense.mono x_range)⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsClosed[inst✝¹] s ↔ IsLowerSet s

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsOpen[inst✝¹] sᶜ ↔ IsLowerSet s
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a : α
⊢ nhdsKer {a} = Ici a

Tactic:
rw [nhdsKer_eq_upperClosure, upperClosure_singleton, UpperSet.coe_Ici]

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

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

Tactic:
· rintro ⟨F, ⟨hF, hs⟩, rfl⟩
    have := hF.to_subtype
    rw [subset_def, Subtype.forall'] at hs
    choose f hf using hs
    exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsClosed[inst✝¹] s ↔ IsUpperSet s

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsOpen[inst✝¹] sᶜ ↔ IsUpperSet s
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ IsClosed[t] s ↔ DirSupClosedOn D s

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ IsOpen[t] sᶜ ↔ DirSupClosedOn D s
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ IsClosed[inst✝¹] s ↔ IsLowerSet s ∧ DirSupClosed s

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : ¬IsPredPrelimit x
s : ℚ
hs : 0 < s ∧ q < s
⊢ ⟨toLex (x, q), ⋯⟩ < ⟨toLex (x, s), ⋯⟩ ∧ ⟨toLex (x, s), ⋯⟩ < ⟨toLex (y, r), ⋯⟩

Tactic:
simp [Prod.Lex.lt_iff, hs.2, h]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ ∀ (a₁ a₂ : Fill α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
simp only [ofLex_toLex, Subtype.forall, Prod.Lex.lt_iff, Subtype.mk_lt_mk,
      Lex.forall, Prod.forall]
    rintro x q ⟨hx₁, hx₂⟩ y r ⟨hy₁, hy₂⟩ (h | ⟨rfl, h⟩)
    · by_cases hx : IsPredPrelimit x
      · obtain ⟨z, hz, hz'⟩ := hx.lt_iff_exists_lt.1 h
        use some z
        simp [some, Prod.Lex.lt_iff, hz', hz]
      obtain ⟨s, hs⟩ := exists_gt (max 0 q)
      rw [max_lt_iff] at hs
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · simp [hx, hs.1.le]
      · simp [Prod.Lex.lt_iff, hs.2, h]
    · obtain ⟨s, hs, hs'⟩ := exists_between h
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · grind [ofLex_toLex]
      · simp [Prod.Lex.lt_iff, hs, hs']

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsOpen[L] sᶜ ↔ IsClosed[S] s

Tactic:
← isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsOpen[L] sᶜ ↔ IsOpen[S] sᶜ
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology ↑X) U
this : IndiscreteTopology ↑X
hne : U ≠ ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows

Tactic:
convert! Presieve.isSheafFor_top (F ⋙ coyoneda.obj (@op C c))
    rw [Sieve.arrows_eq_top_iff, ← Sieve.id_mem_iff_eq_top]
    have := U.eq_bot_or_top.resolve_left hne
    subst this
    obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
    · exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim
    obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial
    obtain rfl | rfl := U.eq_bot_or_top
    · cases hm
    · convert! hf

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

Goal state before:
pp: X : Type u_1
inst✝² : UniformSpace X
x : X
V : SetRel X X
inst✝¹ : V.IsSymm
inst✝ : V.IsTrans
h' : V ∈ 𝓤 X
⊢ IsClosed[inst✝².toTopologicalSpace] (ball x V)

Tactic:
← isOpen_compl_iff,

Goal state after:
X : Type u_1
inst✝² : UniformSpace X
x : X
V : SetRel X X
inst✝¹ : V.IsSymm
inst✝ : V.IsTrans
h' : V ∈ 𝓤 X
⊢ IsOpen[inst✝².toTopologicalSpace] (ball x V)ᶜ
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = comap (Prod.mk x) (𝓝ˢ (diagonal γ))

Tactic:
nhdsSet_diagonal,

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = comap (Prod.mk x) (⨆ x, 𝓝 (x, x))