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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁵ : 0 ≤ ε₂
this✝⁴ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝⁴
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝³ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝² : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝¹ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this✝ : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
⊢ hausdorffDist (range Φ) univ ≤ ε₃

Tactic:
rcases exists_mem_of_nonempty Y with ⟨xY, _⟩

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝¹ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁵ : 0 ≤ ε₂
this✝⁴ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝⁴
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝³ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝² : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝¹ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this✝ : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
xY : Y
h✝ : xY ∈ univ
⊢ hausdorffDist (range Φ) univ ≤ ε₃
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ S.Exact ↔ ∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact

Tactic:
constructor

Goal state after:
case mp
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ S.Exact → ∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact

case mpr
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ (∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact) → S.Exact
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
have hip : i < N p := ((E p) x).2

Goal state after:
case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
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 : Presheaf C X✝
⊢ colimMap
        ((OpenNhds.inclusion p₀).op.whiskerLeft
          {
            app := fun U ↦
              if h : p₀ ∈ unop U then X.germ (unop U) p₀ h ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯
              else (⋯ ▸ terminalIsTerminal).from (X.obj U),
            naturality := ⋯ }) ≫
      (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    𝟙 (colimit ((OpenNhds.inclusion p₀).op ⋙ X))

Tactic:
ext

Goal state after:
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 : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝ ≫
      colimMap
          ((OpenNhds.inclusion p₀).op.whiskerLeft
            {
              app := fun U ↦
                if h : p₀ ∈ unop U then X.germ (unop U) p₀ h ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯
                else (⋯ ▸ terminalIsTerminal).from (X.obj U),
              naturality := ⋯ }) ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝ ≫ 𝟙 (colimit ((OpenNhds.inclusion p₀).op ⋙ X))
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

Goal state after:
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
⊢ ((StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app ((skyscraperPresheafFunctor p₀).obj Y) ≫
          (skyscraperPresheafFunctor p₀).map ((StalkSkyscraperPresheafAdjunctionAuxs.counit p₀).app Y)).app
      (op U✝) =
    (𝟙 ((skyscraperPresheafFunctor p₀).obj Y)).app (op U✝)
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
ι : Type v
Us : ι → Opens ↑X
⊢ Nonempty (IsLimit ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op))

Tactic:
constructor

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
ι : Type v
Us : ι → Opens ↑X
⊢ IsLimit ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op)
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T ↔ ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T → ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))

case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ (∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))) → IsLocallySurjective T
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
⊢ IsLocallySurjective T

Tactic:
constructor

Goal state after:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
⊢ ∀ {U : Opens ↑X} (s : ToType (𝒢.obj (op U))), Presheaf.imageSieve T s ∈ (Opens.grothendieckTopology ↑X) U
Module: Mathlib.Topology.Sheaves.Points

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
x✝³ x✝² : (grothendieckTopology X).Point
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ x✝¹ = x✝

Tactic:
ext

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
x✝⁵ x✝⁴ : (grothendieckTopology X).Point
x✝³ x✝² : x✝⁵ ⟶ x✝⁴
x✝¹ : Opens X
x✝ : x✝⁴.fiber.obj x✝¹
⊢ (ConcreteCategory.hom (x✝³.hom.app x✝¹)).toFun x✝ = (ConcreteCategory.hom (x✝².hom.app x✝¹)).toFun x✝
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd

Tactic:
obtain (rfl | h₁ | h₁) : i = j ∨ Nonempty (i.val ⟶ j.val) ∨ Nonempty (j.val ⟶ i.val) := by
      grind [Subtype.ext_iff, h i.property j.property]

Goal state after:
case inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i : ↑c
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f i)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f i)).op)) (StructuredArrow.right ↑i).snd

case inr.inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑i ⟶ ↑j)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd

case inr.inr
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑j ⟶ ↑i)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
⊢ ((Pi.lift fun i ↦ F.map (leSupr U i).op) ≫
      Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) =
    (Pi.lift fun i ↦ F.map (leSupr U i).op) ≫
      Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
j✝ : Discrete (ι × ι)
⊢ ((Pi.lift fun i ↦ F.map (leSupr U i).op) ≫
        Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    ((Pi.lift fun i ↦ F.map (leSupr U i).op) ≫
        Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ (𝟙 c.pt ≫ Pi.lift fun i ↦ c.π.app (op (single i))) =
    (Pi.lift fun i ↦ c.π.app (op (single i))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)

Tactic:
ext

Goal state after:
case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j✝ : Discrete ι
⊢ (𝟙 c.pt ≫ Pi.lift fun i ↦ c.π.app (op (single i))) ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝ =
    ((Pi.lift fun i ↦ c.π.app (op (single i))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)) ≫
      limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.one)

Tactic:
ext

Goal state after:
case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j✝ : Discrete (ι × ι)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    ((Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.one)) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ (f.hom ≫ Pi.lift fun i ↦ c'.π.app (op (single i))) = Pi.lift fun i ↦ c.π.app (op (single i))

Tactic:
ext

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
j✝ : Discrete ι
⊢ (f.hom ≫ Pi.lift fun i ↦ c'.π.app (op (single i))) ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝ =
    (Pi.lift fun i ↦ c.π.app (op (single i))) ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ (f.hom ≫ Pi.lift fun b ↦ c'.π.app (op (Pairwise.pair b.1 b.2))) = Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))

Tactic:
ext

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
j✝ : Discrete (ι × ι)
⊢ (f.hom ≫ Pi.lift fun b ↦ c'.π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε

Tactic:
have hip : i < N p := ((E p) x).2

Goal state after:
case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 c.pt ≫ Fork.ι c = Pi.lift fun i ↦ ((coneEquivInverse F U).obj c).π.app (op (single i))

Tactic:
ext

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j✝ : Discrete ι
⊢ (𝟙 c.pt ≫ Fork.ι c) ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝ =
    (Pi.lift fun i ↦ ((coneEquivInverse F U).obj c).π.app (op (single i))) ≫
      limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one =
    Pi.lift fun b ↦ ((coneEquivInverse F U).obj c).π.app (op (Pairwise.pair b.1 b.2))

Tactic:
ext

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j✝ : Discrete (ι × ι)
⊢ (𝟙 c.pt ≫ c.π.app WalkingParallelPair.one) ≫ limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    (Pi.lift fun b ↦ ((coneEquivInverse F U).obj c).π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ (𝟙 c.pt ≫ Pi.lift fun i ↦ ((coneEquivInverse F U).obj c).π.app (op (single i))) = Fork.ι c

Tactic:
ext

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j✝ : Discrete ι
⊢ (𝟙 c.pt ≫ Pi.lift fun i ↦ ((coneEquivInverse F U).obj c).π.app (op (single i))) ≫
      limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝ =
    Fork.ι c ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ ((coneEquivInverse F U).obj c).π.app (op (Pairwise.pair b.1 b.2))) =
    c.π.app WalkingParallelPair.one

Tactic:
ext

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j✝ : Discrete (ι × ι)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ ((coneEquivInverse F U).obj c).π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    c.π.app WalkingParallelPair.one ≫ limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝