awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
refine_2 :
  ((Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₁ :
  ((Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom) ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₂ :
  (Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom) ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₃ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₄ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₅ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ (f ⁻¹ᵁ U.ι ''ᵁ V).ι ≫ f =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₆ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V).ι ≫ f =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₇ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
⊢ (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)
have refine_2₈ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ∣_ V ≫ V.ι ≫ U.ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _), Iso.trans_hom, Category.assoc, Category.assoc,
      Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc,
      Scheme.Hom.isoImage_hom_ι_assoc,
      Scheme.Hom.isoImage_hom_ι,
      morphismRestrict_ι_assoc, morphismRestrict_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
refine_2 :
  ((Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₁ :
  ((Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom) ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₂ :
  (Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom) ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₃ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₄ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₅ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ (f ⁻¹ᵁ U.ι ''ᵁ V).ι ≫ f =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₆ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V).ι ≫ f =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₇ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₈ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ∣_ V ≫ V.ι ≫ U.ι
⊢ (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)
have refine_2₉ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = ((f ∣_ U) ⁻¹ᵁ V).ι ≫ f ∣_ U ≫ U.ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _), Iso.trans_hom, Category.assoc, Category.assoc,
      Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc,
      Scheme.Hom.isoImage_hom_ι_assoc,
      Scheme.Hom.isoImage_hom_ι,
      morphismRestrict_ι_assoc, morphismRestrict_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
refine_2 :
  ((Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₁ :
  ((Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom) ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₂ :
  (Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom) ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₃ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₄ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₅ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ (f ⁻¹ᵁ U.ι ''ᵁ V).ι ≫ f =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₆ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V).ι ≫ f =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₇ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₈ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ∣_ V ≫ V.ι ≫ U.ι
refine_2₉ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = ((f ∣_ U) ⁻¹ᵁ V).ι ≫ f ∣_ U ≫ U.ι
⊢ (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)
have refine_2₁₀ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f
Tactic: rw [← cancel_mono (Scheme.Opens.ι _), Iso.trans_hom, Category.assoc, Category.assoc,
      Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc,
      Scheme.Hom.isoImage_hom_ι_assoc,
      Scheme.Hom.isoImage_hom_ι,
      morphismRestrict_ι_assoc, morphismRestrict_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
r : (↑Γ(Y, U) : Type u)
⊢ Arrow.mk (X :=
      (↑((f ∣_ U) ⁻¹ᵁ
            (↑U : Scheme).basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
                  (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.obj (op (⋯.functor.obj ⊤))) : Type u))
                r)) :
        Scheme))
      (f ∣_ U ∣_
        (↑U : Scheme).basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
              (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.obj (op (⋯.functor.obj ⊤))) : Type u))
            r)) ≅
    Arrow.mk (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)) (f ∣_ Y.basicOpen r)
have refine : U.ι ''ᵁ
    (↑U : Scheme).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
          (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.obj (op (sorry.functor.obj ⊤))) : Type u))
        r) =
  Y.basicOpen r
Tactic: refine morphismRestrictRestrict _ _ _ ≪≫ morphismRestrictEq _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
V V' : X.Opens
i : V ≤ V'
⊢ resLE (𝟙 X) V' V i = X.homOfLE i
have simp : X.homOfLE i ≫ 𝟙 (↑(𝟙 X ⁻¹ᵁ V') : Scheme) = X.homOfLE i
Tactic: simp only [resLE, morphismRestrict_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
⊢ X.homOfLE i ≫ resLE f U V e = resLE f U V' ⋯
have simp_rw : resLE (𝟙 X) V V' i ≫ resLE f U V e = resLE f U V' sorry
Tactic: simp_rw [← resLE_id, resLE_comp_resLE, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
simp_rw : resLE (𝟙 X) V V' i ≫ resLE f U V e = resLE f U V' ⋯
⊢ X.homOfLE i ≫ resLE f U V e = resLE f U V' ⋯
have simp_rw₁ : resLE (𝟙 X ≫ f) U V' sorry = resLE f U V' sorry
Tactic: simp_rw [← resLE_id, resLE_comp_resLE, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
⊢ resLE f U V e ≫ Y.homOfLE i = resLE f U' V ⋯
have simp_rw : resLE f U V e ≫ resLE (𝟙 Y) U' U i = resLE f U' V sorry
Tactic: simp_rw [← resLE_id, resLE_comp_resLE, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
simp_rw : resLE f U V e ≫ resLE (𝟙 Y) U' U i = resLE f U' V ⋯
⊢ resLE f U V e ≫ Y.homOfLE i = resLE f U' V ⋯
have simp_rw₁ : resLE (f ≫ 𝟙 Y) U' V sorry = resLE f U' V sorry
Tactic: simp_rw [← resLE_id, resLE_comp_resLE, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U' V' ⋯)
have subst : P (resLE f U V e) ↔ P (resLE f U V' sorry)
Tactic: subst e₁
Cleared hypotheses: U', e₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V' ⋯)
have subst : P (resLE f U V e) ↔ P (resLE f U V sorry)
Tactic: subst e₂
Cleared hypotheses: V', e₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U : Scheme).Opens
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O
have rw : resLE f U V e ⁻¹ᵁ O = (V.ι ≫ f) ⁻¹ᵁ U.ι ''ᵁ O
Tactic: rw [← comp_preimage, ← resLE_comp_ι f e, comp_preimage, preimage_image_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U : Scheme).Opens
rw : resLE f U V e ⁻¹ᵁ O = (V.ι ≫ f) ⁻¹ᵁ U.ι ''ᵁ O
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O
have rw₁ : resLE f U V e ⁻¹ᵁ O = (resLE f U V e ≫ U.ι) ⁻¹ᵁ U.ι ''ᵁ O
Tactic: rw [← comp_preimage, ← resLE_comp_ι f e, comp_preimage, preimage_image_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U : Scheme).Opens
rw : resLE f U V e ⁻¹ᵁ O = (V.ι ≫ f) ⁻¹ᵁ U.ι ''ᵁ O
rw₁ : resLE f U V e ⁻¹ᵁ O = (resLE f U V e ≫ U.ι) ⁻¹ᵁ U.ι ''ᵁ O
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O
have rw₂ : resLE f U V e ⁻¹ᵁ O = resLE f U V e ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ O
Tactic: rw [← comp_preimage, ← resLE_comp_ι f e, comp_preimage, preimage_image_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U : Scheme).Opens
rw : resLE f U V e ⁻¹ᵁ O = (V.ι ≫ f) ⁻¹ᵁ U.ι ''ᵁ O
rw₁ : resLE f U V e ⁻¹ᵁ O = (resLE f U V e ≫ U.ι) ⁻¹ᵁ U.ι ''ᵁ O
rw₂ : resLE f U V e ⁻¹ᵁ O = resLE f U V e ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ O
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O
have rw₃ : resLE f U V e ⁻¹ᵁ O = resLE f U V e ⁻¹ᵁ O
Tactic: rw [← comp_preimage, ← resLE_comp_ι f e, comp_preimage, preimage_image_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U : Scheme).Opens
W : (↑V : Scheme).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ appLE (resLE f U V e) O W e' = appLE f (U.ι ''ᵁ O) (V.ι ''ᵁ W) ⋯
have dsimp : (app (f ∣_ U) O ≫ app (X.homOfLE e) ((f ∣_ U) ⁻¹ᵁ O)) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) =
  app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE sorry).op
Tactic: dsimp [appLE, resLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U : Scheme).Opens
W : (↑V : Scheme).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ (app (f ∣_ U) O ≫ app (X.homOfLE e) ((f ∣_ U) ⁻¹ᵁ O)) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op
have simp : app f (U.ι ''ᵁ O) ≫
    X.presheaf.map (homOfLE sorry).op ≫
      X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) =
  app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE sorry).op
Tactic: simp only [morphismRestrict_app', appLE, homOfLE_leOfHom, homOfLE_app, Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U : Scheme).Opens
W : (↑V : Scheme).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫
      X.presheaf.map (homOfLE ⋯).op ≫
        X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op
have rw : app f (U.ι ''ᵁ O) ≫ X.presheaf.map ((homOfLE sorry).op ≫ Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (homOfLE sorry)) =
  app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE sorry).op
Tactic: rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Iso.hom (U.stalkIso ((resLE f U V e) x)) ≫ Y.presheaf.stalkSpecializes ⋯) ≫ stalkMap f (↑x : ↥X) =
    stalkMap (resLE f U V e) x ≫ (V.stalkIso x).hom
have rw : (Y.presheaf.stalkSpecializes sorry ≫ stalkMap f (↑x : ↥X)) ≫ stalkMap V.ι x =
  Iso.hom (Y.presheaf.stalkCongr sorry) ≫ stalkMap f (V.ι x) ≫ stalkMap V.ι x
Tactic: rw [Category.assoc, ← Iso.eq_inv_comp, ← Category.assoc, ← Iso.comp_inv_eq,
      Opens.stalkIso_inv, Opens.stalkIso_inv, ← stalkMap_comp,
      stalkMap_congr_hom _ _ (resLE_comp_ι f e), stalkMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ U.topIso.hom ≫ (Arrow.mk (Scheme.Hom.appLE f U V e)).hom =
    (Arrow.mk (Scheme.Hom.appTop (Scheme.Hom.resLE f U V e))).hom ≫ V.topIso.hom
have simp : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V sorry = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom sorry)
Tactic: simp only [Arrow.mk_left, Arrow.mk_right, Scheme.Opens.topIso_hom,
    eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom ⋯)
have rw : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V sorry = Scheme.Hom.app (Scheme.Hom.resLE f U V e) ⊤ ≫ X.presheaf.map (eqToHom sorry)
Tactic: rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
rw : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.app (Scheme.Hom.resLE f U V e) ⊤ ≫ X.presheaf.map (eqToHom ⋯)
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom ⋯)
have rw₁ : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V sorry =
  Scheme.Hom.appLE (Scheme.Hom.resLE f U V e) ⊤ (Scheme.Hom.resLE f U V e ⁻¹ᵁ ⊤) sorry ≫ X.presheaf.map (eqToHom sorry)
Tactic: rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
rw : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.app (Scheme.Hom.resLE f U V e) ⊤ ≫ X.presheaf.map (eqToHom ⋯)
rw₁ :
  Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ =
    Scheme.Hom.appLE (Scheme.Hom.resLE f U V e) ⊤ (Scheme.Hom.resLE f U V e ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (eqToHom ⋯)
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom ⋯)
have rw₂ : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V sorry =
  Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) (V.ι ''ᵁ Scheme.Hom.resLE f U V e ⁻¹ᵁ ⊤) sorry ≫ X.presheaf.map (eqToHom sorry)
Tactic: rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
rw : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.app (Scheme.Hom.resLE f U V e) ⊤ ≫ X.presheaf.map (eqToHom ⋯)
rw₁ :
  Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ =
    Scheme.Hom.appLE (Scheme.Hom.resLE f U V e) ⊤ (Scheme.Hom.resLE f U V e ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (eqToHom ⋯)
rw₂ :
  Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ =
    Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) (V.ι ''ᵁ Scheme.Hom.resLE f U V e ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (eqToHom ⋯)
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom ⋯)
have rw₃ : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V sorry = Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V sorry
Tactic: rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (resLE g UX UY ⋯) (resLE iY UT UY ⋯) (resLE iX US UX hUSX) (resLE f US UT hUST)
have refine_1 : IsPullback (Y.homOfLE sorry) (resLE iY UT UY sorry) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) sorry) (T.homOfLE hUST)
Tactic: refine .paste_horiz (v₁₂ := iY.resLE _ _
    ((g.preimage_mono hUSX).trans_eq congr(($H.w) ⁻¹ᵁ US) :)) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
refine_1 : IsPullback (Y.homOfLE ⋯) (resLE iY UT UY ⋯) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (T.homOfLE hUST)
⊢ IsPullback (resLE g UX UY ⋯) (resLE iY UT UY ⋯) (resLE iX US UX hUSX) (resLE f US UT hUST)
have refine_2 : IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) sorry) (resLE iX US UX hUSX) (f ∣_ US)
Tactic: refine .paste_horiz (v₁₂ := iY.resLE _ _
    ((g.preimage_mono hUSX).trans_eq congr(($H.w) ⁻¹ᵁ US) :)) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (Y.homOfLE ⋯) (resLE iY UT UY ⋯) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (T.homOfLE hUST)
have refine_1 : resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) sorry ⁻¹ᵁ opensRange (T.homOfLE hUST) = opensRange (Y.homOfLE sorry)
Tactic: refine (IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_).flip
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ⁻¹ᵁ opensRange (T.homOfLE hUST) = opensRange (Y.homOfLE ⋯)
have refine_1 : Eq (α := (↑(g ⁻¹ᵁ UX) : Scheme).Opens) (((g ⁻¹ᵁ UX).ι ≫ iY) ⁻¹ᵁ UT) ((g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY)
Tactic: simp only [Scheme.opensRange_homOfLE, ← Scheme.Hom.comp_preimage, Scheme.Hom.resLE_comp_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ Eq (α := (↑(g ⁻¹ᵁ UX) : Scheme).Opens) (((g ⁻¹ᵁ UX).ι ≫ iY) ⁻¹ᵁ UT) ((g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY)
have refine_1 : (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ iY ⁻¹ᵁ UT = (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY
Tactic: rw [Scheme.Hom.comp_preimage, ← (g ⁻¹ᵁ UX).ι.image_injective.eq_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ iY ⁻¹ᵁ UT = (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY
have refine_1 : g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT = g ⁻¹ᵁ UX ⊓ UY
Tactic: simp only [Scheme.Hom.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)
have refine_2 : IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) sorry ≫ (f ⁻¹ᵁ US).ι) (resLE iX US UX hUSX ≫ US.ι) f
Tactic: refine .of_bot ?_ ?_ (isPullback_morphismRestrict f US)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
refine_2 : IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ (f ⁻¹ᵁ US).ι) (resLE iX US UX hUSX ≫ US.ι) f
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)
have refine_2₁ : g ∣_ UX ≫ resLE iX US UX hUSX = resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) sorry ≫ f ∣_ US
Tactic: refine .of_bot ?_ ?_ (isPullback_morphismRestrict f US)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
⊢ OpenCover.{u_1, u} (↑U : Scheme)
have refine_1 : ∀ (i : 𝒰.I₀),
  Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
    (Set.range (ι :=
      ↥((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
      ⇑(pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))))
Tactic: refine Cover.copy (𝒰.pullback₁ U.ι) 𝒰.I₀ _ (𝒰.f · ∣_ U) (Equiv.refl _)
    (fun i ↦ IsOpenImmersion.isoOfRangeEq (Opens.ι _) (pullback.snd _ _) ?_) ?_