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

Goal state before:
pp: case neg.refine_1
α : 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
⊢ (IsSuccPrelimit (ofLex (toLex (x, s))).1 → 0 ≤ (ofLex (toLex (x, s))).2) ∧
    (IsPredPrelimit (ofLex (toLex (x, s))).1 → (ofLex (toLex (x, s))).2 ≤ 0)

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), ?neg.refine_1✝⟩ ∧ ⟨toLex (x, s), ?neg.refine_1✝⟩ < ⟨toLex (y, r), ⋯⟩

Tactic:
· simp [hx, hs.1.le]

Goal state after:
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), ⋯⟩
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h✝ : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
hsx : ∀ (x : X), Summable fun n ↦ (f n) x * (1 / 2 / 2 ^ n)
x : X
h : x ∉ s
i : ℕ
hi : x ∈ (U i)ᶜ
j : ℕ
hj : j ≠ i
⊢ 0 ≤ (f j) x * (1 / 2 / 2 ^ j)

Tactic:
by positivity [(hfr j x).1]

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

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
h✝ : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
hsx : ∀ (x : X), Summable fun n ↦ (f n) x * (1 / 2 / 2 ^ n)
h : C(X, ℝ) := { toFun := fun x ↦ ∑' (n : ℕ), (f n) x * (1 / 2 / 2 ^ n), continuous_toFun := ⋯ }
x : X
⊢ 0 ≤ h x

pp: case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
h✝ : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
hsx : ∀ (x : X), Summable fun n ↦ (f n) x * (1 / 2 / 2 ^ n)
h : C(X, ℝ) := { toFun := fun x ↦ ∑' (n : ℕ), (f n) x * (1 / 2 / 2 ^ n), continuous_toFun := ⋯ }
x : X
⊢ h x ≤ 1

Tactic:
· exact tsum_nonneg fun n => by simp [(hfr n x).1]

Goal state after:
case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
h✝ : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
hsx : ∀ (x : X), Summable fun n ↦ (f n) x * (1 / 2 / 2 ^ n)
h : C(X, ℝ) := { toFun := fun x ↦ ∑' (n : ℕ), (f n) x * (1 / 2 / 2 ^ n), continuous_toFun := ⋯ }
x : X
⊢ h x ≤ 1
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 b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens ↑X
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (map' p₀ f ≫ map' p₀ g).app (op U)

Tactic:
split_ifs with h <;> cat_disch

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

Goal state before:
pp: case e_a
X : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : Preorder X
inst✝² : Topology.IsUpperSet X
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimits C
F : X ⥤ C
α : Type v
Us : α → Opens X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
x y : StructuredArrow (Opposite.op (iSup Us)) (principals X)
e : x ⟶ y
xx : StructuredArrow (Opposite.op (principalOpen x.right)) (principals X) :=
  { left := { as := PUnit.unit }, right := x.right,
    hom := 𝟙 ((fromPUnit (Opposite.op (principalOpen x.right))).obj { as := PUnit.unit }) }
yy : StructuredArrow (Opposite.op (principalOpen x.right)) (principals X) :=
  { left := { as := PUnit.unit }, right := y.right, hom := ⋯.hom.op }
ee : xx ⟶ yy := { left := 𝟙 xx.left, right := StructuredArrow.Hom.right e, w := ⋯ }
⊢ ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F).map ((projSup Us).map e) ≫
      limit.π (generator (principalOpen y.right) ⋙ F)
        { left := { as := PUnit.unit }, right := y.right, hom := 𝟙 (Opposite.op (principalOpen y.right)) } =
    limit.π (generator (principalOpen x.right) ⋙ F)
        { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) } ≫
      F.map ((generator (iSup Us)).map e)

Tactic:
exact (limit.lift_π _ _).trans (limit.w
        (StructuredArrow.proj _ (principals X) ⋙ F) ee).symm

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

Goal state before:
pp: case h.refine_2
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
⊢ ⟨W ⊓ (U' ⊓ V'), ⋯⟩ ⟶ V

Tactic:
change W ⊓ (U' ⊓ V') ⟶ V.val

Goal state after:
case h.refine_2
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
⊢ W ⊓ (U' ⊓ V') ⟶ ↑V
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans)
    fun i ↦ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ IsUltraUniformity (SeparationQuotient X)

Tactic:
rw [← SeparationQuotient.uniformity_eq] at this

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ IsUltraUniformity (SeparationQuotient X)
Module: Mathlib.Topology.UniformSpace.Uniformizable

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ⋂ d ∈ 𝓤 X, d ○ (uc ○ d) ⊆ ds ○ uc ○ ds

Tactic:
exact iInter₂_subset_of_subset ds hdsu (by simp [comp_assoc])

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

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ⋂ d ∈ 𝓤 X, d ○ (ds ○ uc ○ ds ○ d) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds

Tactic:
exact iInter₂_subset_of_subset ds hdsu (by simp [comp_assoc])

Goal state after: