awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
⊢ Eq (α := ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) xj :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)
    ((𝒰.f j)
        ((CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) fj) uk :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)
have a : Eq (α := ↥S) ((𝒰.f j) ((d.natTrans.app j) xj : ↥(𝒰.X j)) : ↥S)
  ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)
Tactic: dsimp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
⊢ Eq (α := ↥S) ((𝒰.f j) ((d.natTrans.app j) xj : ↥(𝒰.X j)) : ↥S)
    ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)
have a : Eq (α := ↥S) ((d.natTrans.app j ≫ 𝒰.f j) xj : ↥S) ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)
Tactic: rw [← Scheme.Hom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
⊢ ∃ (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
    (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) y = x
have h : ∀ (xk : ↥(d.functor.obj k)) (h1 : (d.functor.map fj) xk = xj) (h2 : (d.natTrans.app k) xk = uk),
  ∃ (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
    (pullback.lift (d.functor.map fi) (d.functor.map fj) sorry) y = x
Tactic: obtain ⟨xk, h1, h2⟩ := exists_preimage_of_isPullback (d.equifibered fj) xj uk <| by
      apply (𝒰.f j).injective
      dsimp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
      rw [← Scheme.Hom.comp_apply]
      simp [xj, h2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1_1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2_1 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
xk : ↥(d.functor.obj k)
h1 : (d.functor.map fj) xk = xj
h2 : (d.natTrans.app k) xk = uk
⊢ ∃ (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
    (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) y = x
have h : (pullback.lift (d.functor.map fi) (d.functor.map fj) sorry) xk = x
Tactic: use xk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1_1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2_1 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
xk : ↥(d.functor.obj k)
h1 : (d.functor.map fj) xk = xj
h2 : (d.natTrans.app k) xk = uk
⊢ (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) xk = x
have h : Eq (α := ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
  ((pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
      ((pullback.lift (d.functor.map fi) (d.functor.map fj) sorry) xk :
        ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
            (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))) :
    ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
  ((pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
      x :
    ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
Tactic: apply (pullback.snd (d.cover.f i) _).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
⊢ Eq (α := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
have h : ∀ (x : ↥d.glued),
  Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x ↔
    Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
x : ↥d.glued
⊢ Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x ↔
    Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x
have h : Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x →
  ∀ (ui : ↥(𝒰.X i)) (h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase x : ↥S)),
    Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x
Tactic: refine ⟨fun ⟨ui, h⟩ ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
x : ↥d.glued
h :
  Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x →
    ∀ (ui : ↥(𝒰.X i)) (h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase x : ↥S)),
      Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x
⊢ Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x ↔
    Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x
have h₁ : Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x →
  Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x
Tactic: refine ⟨fun ⟨ui, h⟩ ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
x : ↥d.glued
h_1 : Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x
ui : ↥(𝒰.X i)
h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase x : ↥S)
⊢ Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x
have h₁ : ∀ (j : 𝒰.I₀) (xj : ↥(d.functor.obj j)),
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
      (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
      ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) →
    ∀ (h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)),
      Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
        ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
Tactic: obtain ⟨j, xj, rfl⟩ := IsLocallyDirected.ι_jointly_surjective _ x
Cleared hypotheses: x, h_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
ui : ↥(𝒰.X i)
j : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
⊢ Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
have h₁ : ∀ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (uk : ↥(𝒰.X k))
  (h :
    Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
      ((d.natTrans.app j) xj :
        ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)))
  (h :
    Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
      (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)),
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
Tactic: obtain ⟨k, fi, fj, uk, rfl, h⟩ := 𝒰.exists_of_f_eq_f ui (d.natTrans.app j xj) <| by
      simp only [h, functorOfLocallyDirected_obj, ← Scheme.Hom.comp_apply, ι_toBase]
Cleared hypotheses: ui, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
⊢ Eq (α := ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
    ((CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) fj) uk :
      ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
have a : Eq (α := ↥S)
  ((𝒰.f j)
      ((d.natTrans.app j) xj :
        ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
    ↥S)
  ((𝒰.f j)
      ((CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) fj) uk :
        ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
    ↥S)
Tactic: apply (𝒰.f j).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
⊢ Eq (α := ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) xj :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)
    ((𝒰.f j)
        ((CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) fj) uk :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)
have a : Eq (α := ↥S) ((𝒰.f j) ((d.natTrans.app j) xj : ↥(𝒰.X j)) : ↥S)
  ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)
Tactic: simp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
⊢ Eq (α := ↥S) ((𝒰.f j) ((d.natTrans.app j) xj : ↥(𝒰.X j)) : ↥S)
    ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)
have a : Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
  ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)
Tactic: rw [← Scheme.Hom.comp_apply, ← ι_toBase, Scheme.Hom.comp_apply, ← h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
⊢ Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
have h₁ : ∀ (xk : ↥(d.functor.obj k)) (h2 : (d.natTrans.app k) xk = uk),
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
      (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
      ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor)) →
    ∀
      (h :
        Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
          ((d.natTrans.app j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) :
            ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)))
      (h :
        Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
          (d.toBase ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor)) :
            ↥S)),
      Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
        ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))
Tactic: obtain ⟨xk, rfl, h2⟩ := exists_preimage_of_isPullback (d.equifibered fj) xj uk <| by
      apply (𝒰.f j).injective
      simp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
      rw [← Scheme.Hom.comp_apply, ← ι_toBase, Scheme.Hom.comp_apply, ← h]
      simp [← Scheme.Hom.comp_apply]
Cleared hypotheses: xj, h_1, h_2, h