awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
have rw : (pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
Tactic: rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
rw : (pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
⊢ ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
have rw₁ : (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f U.ι ≫ f = (f ⁻¹ᵁ U).ι ≫ f
Tactic: rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
rw : (pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
rw₁ : (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f U.ι ≫ f = (f ⁻¹ᵁ U).ι ≫ f
⊢ ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
have rw₂ : (f ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ U).ι ≫ f
Tactic: rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f
have H : (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ≫ U.ι
Tactic: apply IsOpenImmersion.isPullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
H : (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ≫ U.ι
⊢ IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f
have H' : f ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (f ⁻¹ᵁ U).ι
Tactic: apply IsOpenImmersion.isPullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)
have refine_1 : V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V
Tactic: refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
refine_1 : V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)
have refine_2 : W.ι ''ᵁ W.ι ⁻¹ᵁ U = U
Tactic: refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
refine_1 : V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V
refine_2 : W.ι ''ᵁ W.ι ⁻¹ᵁ U = U
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)
have refine_3 : X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq sorry).hom =
  CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
    (Iso.hom
        (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
          (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq sorry)) :
      (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
    (X.homOfLE sorry : (↑(U ⊓ V) : Scheme) ⟶ (↑U : Scheme))
Tactic: refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
refine_1 : V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V
refine_2 : W.ι ''ᵁ W.ι ⁻¹ᵁ U = U
refine_3 :
  X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑U : Scheme))
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)
have refine_4 : (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑V : Scheme)) =
  CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
    (Iso.hom
        (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
          (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq sorry)) :
      (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
    (X.homOfLE sorry : (↑(U ⊓ V) : Scheme) ⟶ (↑V : Scheme))
Tactic: refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
refine_1 : V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V
refine_2 : W.ι ''ᵁ W.ι ⁻¹ᵁ U = U
refine_3 :
  X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑U : Scheme))
refine_4 :
  (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑V : Scheme)) =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑V : Scheme))
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)
have refine_5 : (W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑W : Scheme)) =
  (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq sorry).hom ≫ X.homOfLE hU
Tactic: refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
refine_1 : V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V
refine_2 : W.ι ''ᵁ W.ι ⁻¹ᵁ U = U
refine_3 :
  X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑U : Scheme))
refine_4 :
  (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑V : Scheme)) =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑V : Scheme))
refine_5 :
  (W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑W : Scheme)) =
    (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)
have refine_6 : X.homOfLE hV ≫ Iso.hom (Iso.refl (↑W : Scheme)) = Iso.hom (Iso.refl (↑V : Scheme)) ≫ X.homOfLE hV
Tactic: refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V
have refine_1 : V.ι ''ᵁ (Opens.map V.ι.base).obj U = U ⊓ V
Tactic: rw [← TopologicalSpace.Opens.map_comp_obj, ← Scheme.Hom.comp_base, Scheme.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
⊢ 𝟙 X ∣_ U = 𝟙 (↑(𝟙 X ⁻¹ᵁ U) : Scheme)
have rw : (𝟙 X ⁻¹ᵁ U).ι = U.ι
Tactic: rw [← cancel_mono U.ι, morphismRestrict_ι, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.snd (f ≫ g) (Scheme.Opens.ι U) =
    (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
have rw : (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
    CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
      (Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
      (pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U)) =
  (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
    (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
Tactic: rw [← pullbackRightPullbackFstIso_inv_snd_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        (Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U)) =
    (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
have simp_rw : CategoryStruct.comp (Y := pullback g (Scheme.Opens.ι U))
    (CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
      ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
      (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))))
    (pullback.snd g (Scheme.Opens.ι U)) =
  ((Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv) ≫
    pullback.snd g (Scheme.Opens.ι U)
Tactic: simp_rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ CategoryStruct.comp (Y := pullback g (Scheme.Opens.ι U))
      (CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))))
      (pullback.snd g (Scheme.Opens.ι U)) =
    ((Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.snd g (Scheme.Opens.ι U)
have e_a : CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
    ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
    (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) =
  (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
    (pullbackRestrictIsoRestrict g U).inv
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
      ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
      (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) =
    (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv
have e_a : CategoryStruct.comp (Y := pullback g (Scheme.Opens.ι U))
    (CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
      ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
      (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))))
    (pullback.fst g (Scheme.Opens.ι U)) =
  ((Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv) ≫
    pullback.fst g (Scheme.Opens.ι U)
Tactic: rw [← cancel_mono (pullback.fst _ _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ CategoryStruct.comp (Y := pullback g (Scheme.Opens.ι U))
      (CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))))
      (pullback.fst g (Scheme.Opens.ι U)) =
    ((Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.fst g (Scheme.Opens.ι U)
have e_a : (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
    CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
      (Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
      (pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U)) =
  CategoryStruct.comp (Y := pullback f (g ⁻¹ᵁ U).ι) (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)))
    (pullback.snd f (g ⁻¹ᵁ U).ι ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.fst g (Scheme.Opens.ι U))
Tactic: simp_rw [Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        (Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U)) =
    CategoryStruct.comp (Y := pullback f (g ⁻¹ᵁ U).ι) (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)))
      (pullback.snd f (g ⁻¹ᵁ U).ι ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.fst g (Scheme.Opens.ι U))
have e_a : ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f
Tactic: rw [pullbackRestrictIsoRestrict_inv_fst, pullbackRightPullbackFstIso_inv_snd_fst, ←
    pullback.condition, pullbackRestrictIsoRestrict_inv_fst_assoc,
    pullbackRestrictIsoRestrict_inv_fst_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have obtain : ∀ (V : (↑U : Scheme).Opens),
  Eq (α := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⟶ Γ((↑(f ⁻¹ᵁ U) : Scheme), (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V))
    (Hom.app (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V))
    (Hom.app f (U.ι ''ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: obtain ⟨V, rfl⟩ : ∃ V', U.ι ⁻¹ᵁ U.ι ''ᵁ V' = V := ⟨_, U.ι.preimage_image_eq V⟩
Cleared hypotheses: V
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
W : (↑(f ⁻¹ᵁ U) : Scheme).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
have rw : Scheme.Hom.app (f ∣_ U) V ≫ (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
  Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) sorry
Tactic: rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map,
    Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
W : (↑(f ⁻¹ᵁ U) : Scheme).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
rw :
  Scheme.Hom.app (f ∣_ U) V ≫ (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
have rw₁ : Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) sorry ≫ (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
  Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) sorry
Tactic: rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map,
    Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
W : (↑(f ⁻¹ᵁ U) : Scheme).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
rw :
  Scheme.Hom.app (f ∣_ U) V ≫ (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
rw₁ :
  Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯ ≫
      (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
have rw₂ : Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) sorry ≫
    X.presheaf.map ((Scheme.Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (homOfLE e).op.unop).op =
  Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) sorry
Tactic: rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map,
    Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
W : (↑(f ⁻¹ᵁ U) : Scheme).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
rw :
  Scheme.Hom.app (f ∣_ U) V ≫ (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
rw₁ :
  Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯ ≫
      (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
rw₂ :
  Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯ ≫
      X.presheaf.map ((Scheme.Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (homOfLE e).op.unop).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
have rw₃ : Eq (α := Γ((↑U : Scheme), V) ⟶ Γ((↑(f ⁻¹ᵁ U) : Scheme), W))
  (Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ unop (op W)) sorry : Γ(Y, U.ι ''ᵁ V) ⟶ Γ(X, (f ⁻¹ᵁ U).ι ''ᵁ unop (op W)))
  (Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) sorry : Γ(Y, U.ι ''ᵁ V) ⟶ Γ(X, (f ⁻¹ᵁ U).ι ''ᵁ W))
Tactic: rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map,
    Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
have rw : f = 𝟙 X ≫ f
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
rw : f = 𝟙 X ≫ f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
have rw₁ : f = f
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
⊢ g ≫ 𝟙 Y = e.hom ≫ V.ι
have rw : g = e.hom ≫ V.ι
Tactic: rw [Category.comp_id, IsOpenImmersion.isoOfRangeEq_hom_fac]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
rw : g = e.hom ≫ V.ι
⊢ g ≫ 𝟙 Y = e.hom ≫ V.ι
have rw₁ : g = g
Tactic: rw [Category.comp_id, IsOpenImmersion.isoOfRangeEq_hom_fac]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g) ≅
    Arrow.mk (X := pullback f g) (pullback.snd f g)
have symm : Arrow.mk (X := pullback f g) (pullback.snd f g) ≅
  Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ Arrow.mk (X := pullback f g) (pullback.snd f g) ≅
    Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)
have refine : (asIso t ≪≫ pullbackRestrictIsoRestrict f V).hom ≫
    (Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)).hom =
  (Arrow.mk (X := pullback f g) (pullback.snd f g)).hom ≫ e.hom
Tactic: refine Arrow.isoMk (asIso t ≪≫ pullbackRestrictIsoRestrict f V) e ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (asIso t ≪≫ pullbackRestrictIsoRestrict f V).hom ≫
      (Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (X := pullback f g) (pullback.snd f g)).hom ≫ e.hom
have rw : (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫
        (Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)).hom) ≫
      e.inv) ≫
    g =
  (Arrow.mk (X := pullback f g) (pullback.snd f g)).hom ≫ g
Tactic: rw [Iso.trans_hom, asIso_hom, ← Iso.comp_inv_eq, ← cancel_mono g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫
          (Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)).hom) ≫
        e.inv) ≫
      g =
    (Arrow.mk (X := pullback f g) (pullback.snd f g)).hom ≫ g
have dsimp : (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
Tactic: dsimp