awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
have h₀ : (gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
    pullback.fst (𝒰.f x) (𝒰.f z) =
  pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f z)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (𝒰.f x) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f z)
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
have h₁ : (gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
    pullback.snd (𝒰.f x) (𝒰.f z) =
  pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y =
    𝟙
      (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z)))
have h₀ : (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
  𝟙
      (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
      pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    𝟙
        (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
          (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
⊢ gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y =
    𝟙
      (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z)))
have h₁ : (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
  𝟙
      (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
      pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    𝟙
        (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
          (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
have h₀ : gluedCoverT' 𝒰 x y z ≫
    gluedCoverT' 𝒰 y z x ≫
      gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
  pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
Tactic: simp_rw [Category.id_comp, Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
      pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    𝟙
        (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
          (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
have h₁ : gluedCoverT' 𝒰 x y z ≫
    gluedCoverT' 𝒰 y z x ≫
      gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
  pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
Tactic: simp_rw [Category.id_comp, Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
      Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))
have h₀ : (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
    pullback.fst (𝒰.f y) (𝒰.f x) =
  (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
      Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) ≫
    pullback.fst (𝒰.f y) (𝒰.f x)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x)
⊢ gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
      Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))
have h₁ : (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
    pullback.snd (𝒰.f y) (𝒰.f x) =
  (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
      Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) ≫
    pullback.snd (𝒰.f y) (𝒰.f x)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
⊢ (gluedCover 𝒰).glued ⟶ X
have k : (b : (MultispanShape.prod (gluedCover 𝒰).J).R) → (gluedCover 𝒰).diagram.right b ⟶ X
Tactic: fapply Multicoequalizer.desc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
k : (b : (MultispanShape.prod (gluedCover 𝒰).J).R) → (gluedCover 𝒰).diagram.right b ⟶ X
⊢ (gluedCover 𝒰).glued ⟶ X
have h : ∀ (a : (MultispanShape.prod (gluedCover 𝒰).J).L),
  (gluedCover 𝒰).diagram.fst a ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst a) =
    (gluedCover 𝒰).diagram.snd a ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd a)
Tactic: fapply Multicoequalizer.desc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y : (gluedCover 𝒰).J
⊢ Eq (α := (gluedCover 𝒰).diagram.left (x, y) ⟶ X)
    ((gluedCover 𝒰).diagram.fst (x, y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst (x, y)))
    ((gluedCover 𝒰).diagram.snd (x, y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd (x, y)))
have h : Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ X)
  (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst (x, y)))
  ((Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y)) ≫ pullback.fst (𝒰.f y) (𝒰.f x)) ≫
    𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd (x, y)))
Tactic: change pullback.fst _ _ ≫ _ = ((pullbackSymmetry _ _).hom ≫ pullback.fst _ _) ≫ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y : ↥(gluedCover 𝒰).glued
h : Eq (α := ↥X) ((fromGlued 𝒰) x : ↥X) ((fromGlued 𝒰) y : ↥X)
⊢ x = y
have obtain : ∀ (i : (gluedCover 𝒰).J) (x : ↥((gluedCover 𝒰).U i))
  (h : Eq (α := ↥X) ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued) : ↥X) ((fromGlued 𝒰) y : ↥X)),
  ((gluedCover 𝒰).ι i) x = y
Tactic: obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
y : ↥(gluedCover 𝒰).glued
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
h : Eq (α := ↥X) ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued) : ↥X) ((fromGlued 𝒰) y : ↥X)
⊢ ((gluedCover 𝒰).ι i) x = y
have obtain : ∀ (j : (gluedCover 𝒰).J) (y : ↥((gluedCover 𝒰).U j))
  (h :
    Eq (α := ↥X) ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued) : ↥X)
      ((fromGlued 𝒰) (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued) : ↥X)),
  Eq (α := ↥(gluedCover 𝒰).glued) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)
    (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued)
Tactic: obtain ⟨j, y, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h :
  Eq (α := ↥X) ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued) : ↥X)
    ((fromGlued 𝒰) (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued) : ↥X)
⊢ Eq (α := ↥(gluedCover 𝒰).glued) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)
    (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued)
have h₁ : Eq (α := ↥X)
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (((gluedCover 𝒰).ι i).base ≫ (fromGlued 𝒰).base) :
        (a : ↥((gluedCover 𝒰).U i)) → ↥X)
      x :
    ↥X)
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (((gluedCover 𝒰).ι j).base ≫ (fromGlued 𝒰).base) :
        (a : ↥((gluedCover 𝒰).U j)) → ↥X)
      y :
    ↥X)
Tactic: rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : Eq (α := ↥X) (((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x : ↥X) (((gluedCover 𝒰).ι j ≫ fromGlued 𝒰) y : ↥X)
⊢ Eq (α := ↥(gluedCover 𝒰).glued) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)
    (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued)
have h₁ : Eq (α := ↥X) ((𝒰.f i) x : ↥X) ((𝒰.f j) y : ↥X)
Tactic: rw [ι_fromGlued, ι_fromGlued] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : Eq (α := ↥X) ((𝒰.f i) x : ↥X) ((𝒰.f j) y : ↥X)
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (W := forgetToTop.obj (pullback (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j)))
      (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j))) ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ Eq (α := ↥(gluedCover 𝒰).glued) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)
    (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued)
have rw : (gluedCover 𝒰).Rel (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x)
  (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y)
Tactic: rw [𝒰.gluedCover.ι_eq_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥(gluedCover 𝒰).glued
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) x)
have obtain : ∀ (i : (gluedCover 𝒰).J) (x : ↥((gluedCover 𝒰).U i)),
  IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
    (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
Tactic: obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
⊢ IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
    (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
have this : Hom.stalkMap ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x = Iso.hom (X.presheaf.stalkCongr sorry) ≫ Hom.stalkMap (𝒰.f i) x
Tactic: have := Hom.stalkMap_congr_hom _ _ (𝒰.ι_fromGlued i) x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this : Hom.stalkMap ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x = Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x
⊢ IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
    (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
have this₁ : Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) =
  (Iso.hom (X.presheaf.stalkCongr sorry) ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x)
Tactic: rw [Hom.stalkMap_comp, ← IsIso.eq_comp_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this :
  Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) =
    (Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x)
⊢ IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
    (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
have rw : IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
  ((Iso.hom (X.presheaf.stalkCongr sorry) ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
⊢ IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U)
have rw : ∀ (x : ↥X), Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x → ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
Tactic: rw [isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
have rw : ∀ (hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)) (x : ↥X)
  (hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x), ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
Tactic: rw [𝒰.gluedCover.isOpen_iff] at hU
Cleared hypotheses: hU, x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
have h : Subset (α := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U) ∧
  IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
    Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
Tactic: use 𝒰.fromGlued '' U ∩ Set.range (𝒰.f (𝒰.idx x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ Subset (α := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x)))
      (⇑(fromGlued 𝒰) '' U) ∧
    IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
      Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
have right : IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
  Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
Tactic: use Set.inter_subset_left
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
    Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
have right : IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
right : IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x)))
⊢ IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
    Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
have right₁ : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x)))
have right : IsOpen (X := ↥X)
  (Set.image (α := ↥(𝒰.X (idx 𝒰 x))) (⇑(𝒰.f (idx 𝒰 x)))
    (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U)))
Tactic: rw [← Set.image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ IsOpen (X := ↥X)
    (Set.image (α := ↥(𝒰.X (idx 𝒰 x))) (⇑(𝒰.f (idx 𝒰 x)))
      (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U)))
have right : IsOpen (X := ↥(𝒰.X (idx 𝒰 x))) (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U))
Tactic: apply (𝒰.f (𝒰.idx x)).isOpenEmbedding.isOpenMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ IsOpen (X := ↥(𝒰.X (idx 𝒰 x))) (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U))
have h : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x)) →
  Eq (α := Set ↥(𝒰.X (idx 𝒰 x))) (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U))
    (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)
Tactic: convert! hU (𝒰.idx x) using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
e_1 : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ Eq (α := Set ↥(𝒰.X (idx 𝒰 x))) (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U))
    (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)
have h : Eq (α := Set ↥(𝒰.X (idx 𝒰 x)))
  (Set.preimage (β := ↥(gluedCover 𝒰).glued)
    (⇑(TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x))))) :
          C(↥(𝒰.X (idx 𝒰 x)), ↥(gluedCover 𝒰).glued)) :
      (a : ↥(𝒰.X (idx 𝒰 x))) → ↥(gluedCover 𝒰).glued)
    (Set.preimage (β := ↥X) (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) : (a : ↥(gluedCover 𝒰).glued) → ↥X)
      ((fun (a : ↥(gluedCover 𝒰).glued) ↦ (fromGlued 𝒰) a) '' U)))
  (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)
Tactic: simp only [← ι_fromGlued, gluedCover_U, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp,
      Set.preimage_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
e_1 : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ Eq (α := Set ↥(𝒰.X (idx 𝒰 x)))
    (Set.preimage (β := ↥(gluedCover 𝒰).glued)
      (⇑(TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x))))) :
            C(↥(𝒰.X (idx 𝒰 x)), ↥(gluedCover 𝒰).glued)) :
        (a : ↥(𝒰.X (idx 𝒰 x))) → ↥(gluedCover 𝒰).glued)
      (Set.preimage (β := ↥X) (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) : (a : ↥(gluedCover 𝒰).glued) → ↥X)
        ((fun (a : ↥(gluedCover 𝒰).glued) ↦ (fromGlued 𝒰) a) '' U)))
    (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)
have h : Set.preimage (β := ↥X) (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) : (a : ↥(gluedCover 𝒰).glued) → ↥X)
    ((fun (a : ↥(gluedCover 𝒰).glued) ↦ (fromGlued 𝒰) a) '' U) =
  U
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
⊢ Epi (fromGlued 𝒰).base
have rw : Function.Surjective (α := ↥(gluedCover 𝒰).glued) (β := ↥X) ⇑(fromGlued 𝒰)
Tactic: rw [TopCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
⊢ ∃ (a : ↥(gluedCover 𝒰).glued), (fromGlued 𝒰) a = x
have obtain : ∀ (y : ↥(𝒰.X (idx 𝒰 x))) (h : (𝒰.f (idx 𝒰 x)) y = x), ∃ (a : ↥(gluedCover 𝒰).glued), (fromGlued 𝒰) a = x
Tactic: obtain ⟨y, h⟩ := 𝒰.covers x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ ∃ (a : ↥(gluedCover 𝒰).glued), (fromGlued 𝒰) a = x
have h₁ : (fromGlued 𝒰) (((gluedCover 𝒰).ι (idx 𝒰 x)) y : ↥(gluedCover 𝒰).glued) = x
Tactic: use 𝒰.gluedCover.ι (𝒰.idx x) y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ (fromGlued 𝒰) (((gluedCover 𝒰).ι (idx 𝒰 x)) y : ↥(gluedCover 𝒰).glued) = x
have h₁ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
        (↑((gluedCover 𝒰).U (idx 𝒰 x)).toPresheafedSpace : TopCat))
        (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x)))) ≫ (fromGlued 𝒰).base) :
      (a : ↥((gluedCover 𝒰).U (idx 𝒰 x))) → ↥X)
    y =
  x
Tactic: rw [← ConcreteCategory.comp_apply]