mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
  rw [← isOpen_compl_iff, isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ), isUpperSet_compl,
    dirSupInaccOn_univ, dirSupInacc_compl]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
| a

Tactic:
← OrderDual.ofDual_toDual a,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
| OrderDual.ofDual (OrderDual.toDual a)
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen[inst✝¹] f.Dom

Tactic:
rw [← PFun.preimage_univ]; exact h _ isOpen_univ

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen[inst✝¹] f.Dom

Tactic:
by
  rw [← PFun.preimage_univ]; exact h _ isOpen_univ

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: 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✝
x : X
y : Y
ys : y ∈ s✝
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : PTendsto' f (𝓝 x) (𝓝 y)
⊢ f.preimage s ∈ 𝓝 x

Tactic:
ptendsto'_def

Goal state after:
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✝
x : X
y : Y
ys : y ∈ s✝
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimalGHInjr X Y),
      image_univ, ← hausdorffDist_optimal]

Goal state after:
case refine_3
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) =
    hausdorffDist (F '' range (optimalGHInjl X Y)) (F '' range (optimalGHInjr X Y))
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2.refine_2
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)) (i : ↑(candidatesB X Y)), dist (↑i x) (↑i y) ≤ 2 * ↑(maxVar X Y) * dist x y

Tactic:
· rintro x y ⟨f, hf⟩
      exact (candidates_lipschitz hf).dist_le_mul _ _

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ IsEmpty X

Tactic:
by cases h; assumption

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 ∈ 𝒮
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
t : Set (Set X)
ht : t ⊆ B'
hf : t.Finite
⊢ B' ⊆ B

Tactic:
by simp [B']

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case h
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
s : ℝ
hs : s ∈ Icc 0 1
hst : (fun θ ↦ (1 - θ) • ↑t₀ + θ • ↑t₁) s = ↑t
⊢ ↑(Icc.convexComb t₀ t₁ ⟨s, hs⟩) = ↑t

Tactic:
exact hst

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

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
⊢ False

Tactic:
have clV : ClusterPt (x, y) (𝓟 <| Vᶜ) := hxy.of_inf_right

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
⊢ False
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜
B : Type u_3
inst✝¹⁸ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁷ : NormedAddCommGroup F₁
inst✝¹⁶ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁵ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
⊢ ∀ ⦃x : TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun x ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x⦄,
    x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
      {
          proj :=
            (x.proj,
                (Trivialization.continuousLinearMapAt 𝕜 e₂ x.proj).compContinuousAlternatingMap
                  (x.snd.compContinuousLinearMap (Trivialization.symmL 𝕜 e₁ x.proj))).1,
          snd :=
            (Trivialization.symmL 𝕜 e₂
                  (x.proj,
                      (Trivialization.continuousLinearMapAt 𝕜 e₂ x.proj).compContinuousAlternatingMap
                        (x.snd.compContinuousLinearMap
                          (Trivialization.symmL 𝕜 e₁ x.proj))).1).compContinuousAlternatingMap
              ((x.proj,
                      (Trivialization.continuousLinearMapAt 𝕜 e₂ x.proj).compContinuousAlternatingMap
                        (x.snd.compContinuousLinearMap (Trivialization.symmL 𝕜 e₁ x.proj))).2.compContinuousLinearMap
                (Trivialization.continuousLinearMapAt 𝕜 e₁
                  (x.proj,
                      (Trivialization.continuousLinearMapAt 𝕜 e₂ x.proj).compContinuousAlternatingMap
                        (x.snd.compContinuousLinearMap (Trivialization.symmL 𝕜 e₁ x.proj))).1)) } =
        x

Tactic:
rintro ⟨x, L⟩ ⟨h₁, h₂⟩
    simp only [TotalSpace.mk_inj]
    ext v
    simp [Function.comp_def, h₁, h₂]

Goal state after: