mathlib-initiative/mathlib-tactics huggingface dataset:
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
Y : C
U✝ : Opens ↑X
⊢ ((if h : p₀ ∈ U✝ then (skyscraperPresheaf p₀ Y).germ U✝ p₀ ⋯ ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then Y else ⊤_ C)) ≫
      if h : p₀ ∈ U✝ then
        eqToHom ⋯ ≫
          (colimit.isoColimitCocone
                { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                  isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }).hom ≫
            eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then (skyscraperPresheaf p₀ Y).stalk p₀ else ⊤_ C)) =
    (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)

Tactic:
split_ifs with h

Goal state after:
case pos
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
Y : C
U✝ : Opens ↑X
h : p₀ ∈ U✝
⊢ ((skyscraperPresheaf p₀ Y).germ U✝ p₀ ⋯ ≫ eqToHom ⋯) ≫
      eqToHom ⋯ ≫
        (colimit.isoColimitCocone
              { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }).hom ≫
          eqToHom ⋯ =
    (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)

case neg
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
Y : C
U✝ : Opens ↑X
h : p₀ ∉ U✝
⊢ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then Y else ⊤_ C) ≫
      (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then (skyscraperPresheaf p₀ Y).stalk p₀ else ⊤_ C) =
    (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)
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
Y : C
⊢ (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app ((skyscraperPresheafFunctor p₀).obj Y) ≫
      (skyscraperPresheafFunctor p₀).map ((StalkSkyscraperPresheafAdjunctionAuxs.counit p₀).app Y) =
    𝟙 ((skyscraperPresheafFunctor p₀).obj Y)

Tactic:
ext
    simp only [skyscraperPresheafFunctor_obj, Functor.id_obj, skyscraperPresheaf_obj,
      Presheaf.stalkFunctor_obj, unit_app, counit_app,
      skyscraperPresheafStalkOfSpecializes, skyscraperPresheafFunctor_map, Presheaf.comp_app,
      toSkyscraperPresheaf_app, Category.id_comp, SkyscraperPresheafFunctor.map'_app]
    split_ifs with h
    · simp [Presheaf.germ]
      rfl
    · simp
      rfl

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) := ⋯
𝒮 : Set (Set (Set X)) := ⋯
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := ⋯
Z : Set X := ⋯
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₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
⊢ (Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty

Tactic:
rw [Set.inter_comm]

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₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
⊢ (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ Z).Nonempty
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : ∃ i, (i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans) ∧ id i ⊆ V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
obtain ⟨U, ⟨U_in, U_sym, U_trans⟩, U_sub⟩ := V_in

Goal state after:
case mp
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_sub : ball x V ⊆ s
U : SetRel X X
U_sub : id U ⊆ V
U_in : U ∈ 𝓤 X
U_sym : U.IsSymm
U_trans : U.IsTrans
⊢ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X : Type u_1
this✝ : UniformSpace X := ⊤
this : ⊤.HasBasis (fun x ↦ True) fun x ↦ Set.univ
⊢ IsUltraUniformity X

Tactic:
rw [← top_uniformity] at this

Goal state after:
X : Type u_1
this✝ : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun x ↦ True) fun x ↦ Set.univ
⊢ IsUltraUniformity X
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ᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst✝²] V₁
V₂_cl : IsClosed[inst✝²] V₂
U₁_op : IsOpen[inst✝²] U₁
U₂_op : IsOpen[inst✝²] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst✝²] U₃
⊢ False

Tactic:
let W := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃

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ᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst✝²] V₁
V₂_cl : IsClosed[inst✝²] V₂
U₁_op : IsOpen[inst✝²] U₁
U₂_op : IsOpen[inst✝²] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst✝²] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
⊢ False
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: case intro.refine_2
𝕜 : 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✝⁶ : Finite ι
inst✝⁵ : VectorBundle 𝕜 F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
val✝ : Fintype ι
⊢ ContinuousOn (fun b ↦ ContinuousAlternatingMap.compContinuousLinearMapCLM ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
refine ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM.comp_continuousOn ?_

Goal state after:
case intro.refine_2
𝕜 : 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✝⁶ : Finite ι
inst✝⁵ : VectorBundle 𝕜 F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
val✝ : Fintype ι
⊢ ContinuousOn (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))