awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
h₁ :
  Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
h₂ :
  Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (↑i : X.Opens).ι)
⊢ Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
have h₃ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
Tactic: rw [← pullback.condition_assoc, pullback.condition_assoc (f := I.glueDataObjι i),
          X.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
        (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
        (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙
          (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)
have h₁ : (CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)))
        (pullback.lift (I.glueDataT'Aux i j k k sorry) (I.glueDataT'Aux i j k i sorry) sorry ≫
          pullback.lift (I.glueDataT'Aux j k i i sorry) (I.glueDataT'Aux j k i j sorry) sorry ≫
            pullback.lift (I.glueDataT'Aux k i j j sorry) (I.glueDataT'Aux k i j k sorry) sorry)
        (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι =
  ((𝟙
          (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
        pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ (CategoryStruct.comp (Y :=
          pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
          (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
              pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
          (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι =
    ((𝟙
            (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι
have h₁ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.fst (I.glueDataObjι i) (X.homOfLE sorry) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
  (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
Tactic: simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
          glueDataT'Aux_snd_ι, limit.lift_π_assoc, cospan_left, glueDataT'Aux_fst_assoc,
          glueDataT_fst_assoc, Scheme.homOfLE_ι, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
have h₁ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.fst (I.glueDataObjι i) (X.homOfLE sorry) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
  (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
Tactic: rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
h₁ :
  Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
⊢ Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
have h₂ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ X.homOfLE sorry ≫ (↑i : X.Opens).ι)
  (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
Tactic: rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
h₁ :
  Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
h₂ :
  Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (↑i : X.Opens).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
⊢ Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
have h₃ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
  (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
Tactic: rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V) (I.glueData.ι U)
have this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE sorry)
Tactic: have : IsIso (X.homOfLE inf_le_left : (U.1 ⊓ V.1).toScheme ⟶ U) :=
    ⟨X.homOfLE (by simpa), by simp, by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
⊢ inv (X.homOfLE ⋯) = X.homOfLE ⋯
have rw : X.homOfLE sorry ≫ X.homOfLE sorry = 𝟙 (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)
Tactic: rw [eq_comm, ← hom_comp_eq_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V) (I.glueData.ι U)
have H : inv (X.homOfLE sorry) = X.homOfLE sorry
Tactic: have H : inv (X.homOfLE inf_le_left : (U.1 ⊓ V.1).toScheme ⟶ U) = X.homOfLE (by simpa) := by
    rw [eq_comm, ← hom_comp_eq_id]; simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V) (I.glueData.ι U)
have this₁ : I.glueData.t U V ≫ I.glueData.f V U ≫ I.glueData.ι V = I.glueData.f U V ≫ I.glueData.ι U
Tactic: have := I.glueData.glue_condition U V
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObjPullback U V ⟶ I.glueData.glued)
    (I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueData.ι U)
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V) (I.glueData.ι U)
have this₁ : Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
  (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
    I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE sorry) ≫ I.glueData.ι V)
  (I.glueData.ι U)
Tactic: rw [← IsIso.inv_comp_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (I.glueData.ι U)
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V) (I.glueData.ι U)
have rw : Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V)
  (𝟙 (I.glueData.U U) ≫
    inv (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE sorry) ≫ I.glueData.ι V)
Tactic: rw [← Category.id_comp (I.glueData.ι U), ← this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (I.glueData.ι U)
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V)
    (𝟙 (I.glueData.U U) ≫
      ((inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
          pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
        I.glueData.ι V)
have e_a : I.glueDataObjMap h =
  (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫ I.glueDataT U V) ≫
    pullback.fst (I.glueDataObjι V) (X.homOfLE sorry)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (I.glueData.ι U)
⊢ I.glueDataObjMap h =
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
      pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)
have e_a : I.glueDataObjMap h ≫ I.glueDataObjι V =
  ((inv (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫ I.glueDataT U V) ≫
      pullback.fst (I.glueDataObjι V) (X.homOfLE sorry)) ≫
    I.glueDataObjι V
Tactic: rw [← cancel_mono (glueDataObjι _ _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
a b : ↥I.glueData.glued
e : Eq (α := ↥X) (I.gluedTo a : ↥X) (I.gluedTo b : ↥X)
⊢ a = b
have obtain : ∀ (ia : I.glueData.J) (a : ↥(I.glueDataObj ia))
  (e :
    Eq (α := ↥X)
      (I.gluedTo
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
                (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
                  (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
              a :
            (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
        ↥X)
      (I.gluedTo b : ↥X)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
          (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
      a =
    b
Tactic: obtain ⟨ia, a : I.glueDataObj ia, rfl⟩ :=
    I.glueData.toGlueData.ι_jointly_surjective forget a
Cleared hypotheses: a, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
b : ↥I.glueData.glued
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
e :
  Eq (α := ↥X)
    (I.gluedTo
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
                (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
            a :
          (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
      ↥X)
    (I.gluedTo b : ↥X)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
          (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
      a =
    b
have obtain : ∀ (ib : I.glueData.J) (b : ↥(I.glueDataObj ib))
  (e :
    Eq (α := ↥X)
      (I.gluedTo
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
                (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
                  (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
              a :
            (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
        ↥X)
      (I.gluedTo
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ib)) :
                (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ib))) →
                  (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
              b :
            (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
        ↥X)),
  Eq (α := ↥I.glueData.glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
          (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
            (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
        a :
      (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ib)) :
          (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ib))) →
            (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
        b :
      (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
Tactic: obtain ⟨ib, b : I.glueDataObj ib, rfl⟩ :=
    I.glueData.toGlueData.ι_jointly_surjective forget b
Cleared hypotheses: b, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  Eq (α := ↥X)
    (I.gluedTo
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
                (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
            a :
          (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
      ↥X)
    (I.gluedTo
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ib)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ib))) →
                (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
            b :
          (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
      ↥X)
⊢ Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
have this : Eq (α := ↥X) ((I.glueData.ι ia ≫ I.gluedTo) a : ↥X) ((I.glueData.ι ib ≫ I.gluedTo) b : ↥X)
Tactic: have : (I.glueData.ι ia ≫ I.gluedTo) a = (I.glueData.ι ib ≫ I.gluedTo) b := e