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

Goal state before:
pp: 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
⊢ S.π.app ((projSup Us).obj y) ≫
      limit.π (generator (principalOpen y.right) ⋙ F)
        { left := { as := PUnit.unit }, right := y.right, hom := 𝟙 (Opposite.op (principalOpen y.right)) } =
    S.π.app ((projSup Us).obj x) ≫
      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:
← S.w ((projSup Us).map e),

Goal state after:
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
⊢ (S.π.app ((projSup Us).obj x) ≫
        ((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)) } =
    S.π.app ((projSup Us).obj x) ≫
      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)
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
x y : C
f : x ⟶ y
U : Opens ↑X
hxU : p₀ ∈ U
⊢ ((skyscraperPresheafFunctor p₀).obj x).germ U p₀ hxU ≫
      (skyscraperPresheafFunctor p₀ ⋙ Presheaf.stalkFunctor C p₀).map f ≫
        (skyscraperPresheafStalkOfSpecializes p₀ y ⋯).hom =
    ((skyscraperPresheafFunctor p₀).obj x).germ U p₀ hxU ≫
      (skyscraperPresheafStalkOfSpecializes p₀ x ⋯).hom ≫ (𝟭 C).map f

Tactic:
simp [hxU]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : Cb X Y
C : ℝ
⊢ BddAbove (range fun x ↦ ⨅ y, f (inl x, inr y) + C)

Tactic:
obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove

Goal state after:
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
⊢ BddAbove (range fun x ↦ ⨅ y, f (inl x, inr y) + C)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty X
f : Cb X Y
C : ℝ
⊢ BddAbove (range fun y ↦ ⨅ x, f (inl x, inr y) + C)

Tactic:
obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove

Goal state after:
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty X
f : Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
⊢ BddAbove (range fun y ↦ ⨅ x, f (inl x, inr y) + C)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
z : Y
⊢ ∃ y ∈ range (optimalGHInjl X Y), dist (optimalGHInjr X Y z) y ≤ r

Tactic:
have I1 : (⨆ y, ⨅ x, optimalGHDist X Y (inl x, inr y)) < r :=
      lt_of_le_of_lt (le_max_right _ _) hr

Goal state after:
case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
z : Y
I1 : ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y) < r
⊢ ∃ y ∈ range (optimalGHInjl X Y), dist (optimalGHInjr X Y z) y ≤ r
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := fun n ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := fun n ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := toInductiveLimit I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : ℕ → Set (UniformSpace.Completion Z0) := fun n ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
n : ℕ
⊢ Isometry (Φ n ∘ (Y n).embed)

Tactic:
exact (toInductiveLimit_isometry _ _).comp (Y n).isom

Goal state after: