mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))
I :
  (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y))) =
    (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))
⊢ IsometryRel.setoid (NonemptyCompacts.kuratowskiEmbedding X) (NonemptyCompacts.kuratowskiEmbedding Y)

Tactic:
exact ⟨cast I ((f.trans e).trans g)⟩

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

Goal state before:
pp: case refine_1
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x✝¹ x✝ : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
a✝¹ : ⟦x✝¹⟧ = toGHSpace X
a✝ : ⟦x✝⟧ = toGHSpace Y
ht : hausdorffDist ↑x✝¹ ↑x✝ = t
⊢ 0 ≤ t

Tactic:
rw [← ht]

Goal state after:
case refine_1
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x✝¹ x✝ : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
a✝¹ : ⟦x✝¹⟧ = toGHSpace X
a✝ : ⟦x✝⟧ = toGHSpace Y
ht : hausdorffDist ↑x✝¹ ↑x✝ = t
⊢ 0 ≤ hausdorffDist ↑x✝¹ ↑x✝
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
x✝² x✝¹ : α
x✝ : x✝² ≤ x✝¹
⊢ {x✝², x✝¹} ∈ univ

Tactic:
by trivial

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

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
hS : ∀ t ∈ S, ∃ u, {x | x u} = t
⊢ ∃ u, {x | x u} = ⋃₀ S

Tactic:
choose f hf using hS
    use ⨆ t, ⨆ ht, f t ht
    simp_rw [map_iSup, iSup_Prop_eq, ofPred_exists, hf, sUnion_eq_biUnion]

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

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
C : Set ↑T
h : IsClosed[instTopologicalSpaceSubtype] C
a : α
ha : C = hull T a
⊢ hull T (kernel C) = C

Tactic:
ha,

Goal state after:
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
C : Set ↑T
h : IsClosed[instTopologicalSpaceSubtype] C
a : α
ha : C = hull T a
⊢ hull T (kernel (hull T a)) = hull T a
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)

Tactic:
← Ioo_insert_left h,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (insert a (Ioo a b)) = 𝓝 a ⊔ 𝓟 (Ioo a b)
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 : IsUpperSet s
⊢ IsOpen[L] s ↔ IsOpen[S] s

Tactic:
rw [@IsLawson.topology_eq_lawson α _ L _, @IsScott.topology_eq α univ _ S _]

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

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ unop W
⊢ (if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) =
    (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) ≫
      if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop V then A else ⊤_ C)

Tactic:
have hV : p₀ ∈ unop V := leOfHom iWV.unop hW

Goal state after:
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ unop W
hV : p₀ ∈ unop V
⊢ (if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) =
    (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) ≫
      if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop V then A else ⊤_ C)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
this✝¹ : Presheaf.IsLocallySurjective S.g.hom
W : Opens ↑X
Wle : W ≤ U
hW : x ∈ W
t₁ : ↑(S.X₂.obj.obj (op W))
ht₁ : (ConcreteCategory.hom (S.g.hom.app (op W))) t₁ = (s |_ W) Wle
t₂ : ToType (S.X₂.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W))) :=
  ((StructuredArrow.right t).snd |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ -
    (t₁ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
this✝ : (ConcreteCategory.hom (S.g.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₂ = 0
t₃ : ↑(S.X₁.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W)))
ht₃ : (ConcreteCategory.hom (S.f.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₃ = t₂
t₄ : ↑(S.X₁.obj.obj (op W))
ht₄ : (t₄ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = t₃
f : Fin 2 → Opens ↑X := ![unop (StructuredArrow.right t).fst, W]
sf : (i : Fin 2) → ↑(S.X₂.obj.obj (op (f i))) :=
  fun x ↦
    match x with
    | 0 => (StructuredArrow.right t).snd
    | 1 => t₁ + (ConcreteCategory.hom (S.f.hom.app (op W))) t₄
this : (sf 0 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = (sf 1 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
t₅ : ToType (S.X₂.obj.obj (op (iSup f)))
ht₅ : IsGluing S.X₂.obj f sf t₅
right✝ : ∀ (y : ToType (S.X₂.obj.obj (op (iSup f)))), (fun t₅ ↦ IsGluing S.X₂.obj f sf t₅) y → y = t₅
le : iSup f ≤ U
⊢ f 0 ≤ U ∧ f 1 ≤ U

Tactic:
exact ⟨tle, Wle⟩

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t

Tactic:
apply (hs ht).imp <;> grind

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case left
t₀ t₁ : ↑I
⊢ ∀ (a : ↑I), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁

Tactic:
intro s
    exact convex_uIcc (t₀ : ℝ) t₁ left_mem_uIcc right_mem_uIcc
      (one_minus_nonneg s) (nonneg s) (sub_add_cancel _ _)

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ ↑y1 ↑y2
this : IsPreconnected univ
hJ1 : IsClosed J1
hJ2 : IsClosed J2
h_univ : univ ⊆ J1 ∪ J2
⊢ univ ∩ (J1 ∩ J2) = ∅

Tactic:
simp [hJ1J2]

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: case right
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
hsup_y : ∀ x ∈ X, IsLUB {x_1 | ∃ y ∈ Y, f x y = x_1} (sup_y x)
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
hinf_x : ∀ y ∈ Y, IsGLB {x | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)
sup_inf : β
hsup_inf : IsLUB {x | ∃ y ∈ Y, inf_x y = x} sup_inf
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
s : Finset ↑Y
hs : ∀ x ∈ X, ∃ i ∈ s, t < f x ↑i
hs' : ∀ x ∈ X, ∃ y ∈ Subtype.val '' ↑s, t < f x y
y0 : (∀ x ∈ X, ∃ y ∈ Subtype.val '' ↑s, t < f x y) → F
hy0 : ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val '' ↑s, t < f x y), y0 ht ∈ Y
ht0 : ∀ x ∈ X, t < f x (y0 hs')
a : E
ha : a ∈ X
h : IsMinOn (fun x ↦ f x (y0 hs')) X a
⊢ f a (y0 hs') ≤ inf_x (y0 hs')

Tactic:
simpa [le_isGLB_iff (hinf_x (y0 hs') (hy0 hs')), mem_lowerBounds]

Goal state after: