awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
k :
  (b : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R) →
    (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.right b ⟶ Y
h :
  ∀ (a : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).L),
    (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.fst a ≫
        f (idx 𝒰 ((MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).fst a)) =
      (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.snd a ≫
        f (idx 𝒰 ((MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).snd a))
⊢ (ulift (P := IsOpenImmersion) 𝒰).gluedCover.glued ⟶ Y

Tactic:
fapply Multicoequalizer.desc

Premises used: CategoryTheory.Limits.Multicoequalizer.desc
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
⊢ (b : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R) →
    (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.right b ⟶ Y

Tactic:
exact fun i ↦ f _
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
i j : (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J
h :
  Eq (α := pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
    (CategoryStruct.comp (Y := 𝒰.X (idx 𝒰 i)) ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.fst (i, j))
        (f (idx 𝒰 i)) :
      pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
    (CategoryStruct.comp (Y := 𝒰.X (idx 𝒰 j)) ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.snd (i, j))
        (f (idx 𝒰 j)) :
      pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
⊢ Eq (α := (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.left (i, j) ⟶ Y)
    ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.fst (i, j) ≫
      f (idx 𝒰 ((MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).fst (i, j))))
    ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.snd (i, j) ≫
      f (idx 𝒰 ((MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).snd (i, j))))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
i j : (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J
h :
  pullback.fst ((ulift (P := IsOpenImmersion) 𝒰).f i) ((ulift (P := IsOpenImmersion) 𝒰).f j) ≫ f (idx 𝒰 i) =
    ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.t i j ≫ (ulift (P := IsOpenImmersion) 𝒰).gluedCover.f j i) ≫
      f (idx 𝒰 j)
⊢ Eq (α := pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
    (CategoryStruct.comp (Y := 𝒰.X (idx 𝒰 i)) ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.fst (i, j))
        (f (idx 𝒰 i)) :
      pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
    (CategoryStruct.comp (Y := 𝒰.X (idx 𝒰 j)) ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.snd (i, j))
        (f (idx 𝒰 j)) :
      pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)

Tactic:
change pullback.fst _ _ ≫ f _ = (_ ≫ _) ≫ f _

Premises used: CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
i j : (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J
⊢ pullback.fst ((ulift (P := IsOpenImmersion) 𝒰).f i) ((ulift (P := IsOpenImmersion) 𝒰).f j) ≫ f (idx 𝒰 i) =
    ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.t i j ≫ (ulift (P := IsOpenImmersion) 𝒰).gluedCover.f j i) ≫
      f (idx 𝒰 j)

Tactic:
simpa [pullbackSymmetry_hom_comp_fst] using hf _ _

Premises used: CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
rw : (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₁ = (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₂
⊢ f₁ = f₂

Tactic:
rw [← cancel_epi 𝒰.ulift.fromGlued]

Premises used: AlgebraicGeometry.Scheme.Cover.fromGlued, CategoryTheory.cancel_epi, AlgebraicGeometry.Scheme.Cover.ulift
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
h₁ :
  ∀ (b : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R),
    Multicoequalizer.π (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram b ≫
        (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₁ =
      Multicoequalizer.π (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram b ≫
        (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₂
⊢ (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₁ = (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₂

Tactic:
apply Multicoequalizer.hom_ext

Premises used: CategoryTheory.Limits.Multicoequalizer.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
x : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R
h₁ : (ulift (P := IsOpenImmersion) 𝒰).f x ≫ f₁ = (ulift (P := IsOpenImmersion) 𝒰).f x ≫ f₂
⊢ Multicoequalizer.π (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram x ≫
      (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₁ =
    Multicoequalizer.π (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram x ≫
      (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₂

Tactic:
rw [fromGlued, Multicoequalizer.π_desc_assoc, Multicoequalizer.π_desc_assoc]

Premises used: CategoryTheory.Limits.Multicoequalizer.π_desc_assoc, AlgebraicGeometry.Scheme.Cover.fromGlued
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
x : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R
⊢ (ulift (P := IsOpenImmersion) 𝒰).f x ≫ f₁ = (ulift (P := IsOpenImmersion) 𝒰).f x ≫ f₂

Tactic:
h _
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
x : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R
⊢ (ulift (P := IsOpenImmersion) 𝒰).f x ≫ f₁ = (ulift (P := IsOpenImmersion) 𝒰).f x ≫ f₂

Tactic:
exact h _
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
x : 𝒰.I₀
⊢ 𝒰.f x ≫ glueMorphisms 𝒰 f hf = f x

Tactic:
Cover.hom_ext (𝒰.ulift.pullback₁ (𝒰.f x)) _ _ fun i ↦ ?_

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Scheme.Cover.ulift, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
x : 𝒰.I₀
refine :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).I₀),
    (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).f i ≫ 𝒰.f x ≫ glueMorphisms 𝒰 f hf =
      (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).f i ≫ f x
⊢ 𝒰.f x ≫ glueMorphisms 𝒰 f hf = f x

Tactic:
refine Cover.hom_ext (𝒰.ulift.pullback₁ (𝒰.f x)) _ _ fun i ↦ ?_

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Scheme.Cover.ulift, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).I₀
dsimp :
  Eq (α := pullback (Y := 𝒰.X (idx 𝒰 i)) (𝒰.f x) (𝒰.f (idx 𝒰 i)) ⟶ Y)
    (pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ 𝒰.f x ≫ glueMorphisms 𝒰 f hf) (pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f x)
⊢ (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).f i ≫ 𝒰.f x ≫ glueMorphisms 𝒰 f hf =
    (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).f i ≫ f x

Tactic:
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, ulift_X, ulift_f, PreZeroHypercover.pullback₁_f]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, CategoryTheory.PreZeroHypercover.pullback₁_X, AlgebraicGeometry.Scheme.Cover.ulift_X, AlgebraicGeometry.Scheme.Cover.ulift_f, CategoryTheory.PreZeroHypercover.pullback₁_f
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).I₀
simp_rw :
  Eq (α := pullback (Y := 𝒰.X (idx 𝒰 i)) (𝒰.f x) (𝒰.f (idx 𝒰 i)) ⟶ Y)
    (pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫
      CategoryStruct.comp (Y := (ulift (P := IsOpenImmersion) 𝒰).gluedCover.glued)
        ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.ι i)
        (Multicoequalizer.desc (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram Y
          (fun (i : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R) ↦ f (idx 𝒰 i)) ⋯))
    (pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f (idx 𝒰 i))
⊢ Eq (α := pullback (Y := 𝒰.X (idx 𝒰 i)) (𝒰.f x) (𝒰.f (idx 𝒰 i)) ⟶ Y)
    (pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ 𝒰.f x ≫ glueMorphisms 𝒰 f hf) (pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f x)

Tactic:
simp_rw [pullback.condition_assoc, ← ulift_f, ← ι_fromGlued, Category.assoc, glueMorphisms,
    IsIso.hom_inv_id_assoc, ulift_f, hf]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition_assoc, AlgebraicGeometry.Scheme.Cover.ulift_f, CategoryTheory.IsIso.hom_inv_id_assoc, AlgebraicGeometry.Scheme.Cover.glueMorphisms, AlgebraicGeometry.Scheme.Cover.ι_fromGlued
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).I₀
⊢ Eq (α := pullback (Y := 𝒰.X (idx 𝒰 i)) (𝒰.f x) (𝒰.f (idx 𝒰 i)) ⟶ Y)
    (pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫
      CategoryStruct.comp (Y := (ulift (P := IsOpenImmersion) 𝒰).gluedCover.glued)
        ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.ι i)
        (Multicoequalizer.desc (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram Y
          (fun (i : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R) ↦ f (idx 𝒰 i)) ⋯))
    (pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f (idx 𝒰 i))

Tactic:
simp [CategoryTheory.GlueData.ι]

Premises used: CategoryTheory.GlueData.ι
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f g : X ⟶ Y
H : ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
choose : ∀ (U : (x : ↥X) → X.Opens) (hxU : ∀ (x : ↥X), x ∈ U x) (hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g), f = g
⊢ f = g

Tactic:
choose U hxU hU using H

Premises used: CategoryTheory.GlueData.U
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f g : X ⟶ Y
U : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
rw :
  (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X } i)
⊢ PreZeroHypercover.presieve₀ { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι } ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f g : X ⟶ Y
U : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
x : ↥X
⊢ Membership.mem (γ := Set ↥X)
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := X)
          { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X } x))
      ⇑(PreZeroHypercover.f { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι } x))
    x

Tactic:
simpa using hxU x
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f g : X ⟶ Y
U : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X } i)

Tactic:
refine ⟨fun x ↦ ⟨x, by simpa using hxU x⟩, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f g : X ⟶ Y
U : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
𝒰 : X.OpenCover := { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι, mem₀ := ⋯ }
⊢ f = g

Tactic:
𝒰.hom_ext _ _ hU

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f g : X ⟶ Y
U : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
𝒰 : X.OpenCover := { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι, mem₀ := ⋯ }
⊢ f = g

Tactic:
exact 𝒰.hom_ext _ _ hU

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ Eq (α := pullback f (𝒰.f i) ⟶ Y) ((fst f (𝒰.f i) ≫ f) ≫ 𝟙 Y) (snd f (𝒰.f i) ≫ 𝒰.f i)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 Y = 𝟙 (𝒰.X j) ≫ 𝒰.f j

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (snd f (𝒰.f i))
i j : 𝒰.I₀
rw :
  Eq (α := pullback (X := pullback f (𝒰.f i)) (Y := pullback f (𝒰.f j)) (fst f (𝒰.f i)) (fst f (𝒰.f j)) ⟶ X)
    (CategoryStruct.comp (Y := pullback (𝒰.f i) (𝒰.f j))
      (Iso.hom (pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))) ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯)
      (fst (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) i))
    (CategoryStruct.comp (Y := pullback (𝒰.f i) (𝒰.f j))
      (Iso.hom (pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))) ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯)
      (snd (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) j))
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ X)
    (fst (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) i)
    (snd (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) j)

Tactic:
rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ map (fst f (𝒰.f i) ≫ f)
      (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd _ _) (𝟙 _) (𝟙 _) (by simp) (by simp))]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Limits.pullback.map, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ Eq (α := pullback (X := pullback f (𝒰.f i)) (Y := pullback f (𝒰.f j)) (fst f (𝒰.f i)) (fst f (𝒰.f j)) ⟶ X)
    (CategoryStruct.comp (Y := pullback (𝒰.f i) (𝒰.f j))
      (Iso.hom (pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))) ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯)
      (fst (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) i))
    (CategoryStruct.comp (Y := pullback (𝒰.f i) (𝒰.f j))
      (Iso.hom (pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))) ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯)
      (snd (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) j))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (snd f (𝒰.f i))
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫
      f ≫
        Cover.glueMorphisms 𝒰
          (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) ⋯ =
    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ 𝟙 X

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (snd f (𝒰.f i))
i : 𝒰.I₀
⊢ 𝒰.f i ≫
      Cover.glueMorphisms 𝒰
          (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) ⋯ ≫
        f =
    𝒰.f i ≫ 𝟙 Y

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
i : J
⊢ LE.le (α := (F.obj i).Opens) ⊤
    (Hom.opensRange (X :=
      F.obj
        (Sigma.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i))
          (Sigma.mk (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)) i (𝟙 i, 𝟙 i))))
      (F.map
        (Sigma.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i))
            (Sigma.mk (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)) i (𝟙 i, 𝟙 i))).1))

Tactic:
simp [Scheme.Hom.opensRange_of_isIso]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
obtain :
  ∀ (k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)) (y₁ : ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    (hy₁ :
      Eq (α := ↥(F.obj i)) ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) y₁ : ↥(F.obj i))
        ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))),
    ∃ (l : J) (fi : l ⟶ i) (fj : l ⟶ j) (fk : l ⟶ k) (α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι) (z : ↥(F.obj l)),
      IsOpenImmersion α ∧
        α ≫ pullback.fst (V F i j).ι (V F i k).ι =
            CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
              ((F.obj i).homOfLE ⋯) ∧
          α ≫ pullback.snd (V F i j).ι (V F i k).ι =
              CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme))
                (Iso.hom (Hom.isoOpensRange (F.map fi))) ((F.obj i).homOfLE ⋯) ∧
            α z = x
⊢ ∃ (l : J) (fi : l ⟶ i) (fj : l ⟶ j) (fk : l ⟶ k) (α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι) (z : ↥(F.obj l)),
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι =
          CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
            ((F.obj i).homOfLE ⋯) ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι =
            CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
              ((F.obj i).homOfLE ⋯) ∧
          α z = x

Tactic:
obtain ⟨k₁, y₁, hy₁⟩ := mem_iSup.mp ((pullback.fst (C := Scheme) _ _) x).2

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.mem_iSup, CategoryTheory.Limits.pullback.fst, Iff.mp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, Subtype.property