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 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) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw₂ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₂ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw₃ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₂ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₃ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw₄ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.fst f g ≫ f
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₂ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₃ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g
rw₄ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.fst f g ≫ f
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw₅ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ (f ⁻¹ᵁ Scheme.Hom.opensRange g).ι ≫ f = pullback.fst f g ≫ f
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₂ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₃ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g
rw₄ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.fst f g ≫ f
rw₅ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ (f ⁻¹ᵁ Scheme.Hom.opensRange g).ι ≫ f = pullback.fst f g ≫ f
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw₆ : t ≫ pullback.fst f V.ι ≫ f = pullback.fst f g ≫ f
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₂ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₃ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g
rw₄ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.fst f g ≫ f
rw₅ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ (f ⁻¹ᵁ Scheme.Hom.opensRange g).ι ≫ f = pullback.fst f g ≫ f
rw₆ : t ≫ pullback.fst f V.ι ≫ f = pullback.fst f g ≫ f
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw₇ : Eq (α := pullback f g ⟶ Y) ((pullback.fst f g ≫ 𝟙 X) ≫ f) (pullback.fst f g ≫ f)
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₂ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₃ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g
rw₄ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.fst f g ≫ f
rw₅ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ (f ⁻¹ᵁ Scheme.Hom.opensRange g).ι ≫ f = pullback.fst f g ≫ f
rw₆ : t ≫ pullback.fst f V.ι ≫ f = pullback.fst f g ≫ f
rw₇ : Eq (α := pullback f g ⟶ Y) ((pullback.fst f g ≫ 𝟙 X) ≫ f) (pullback.fst f g ≫ f)
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
have rw₈ : Eq (α := pullback f g ⟶ Y) (pullback.fst f g ≫ f) (pullback.fst f g ≫ f)
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
-- 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 V : Y.Opens
e : U = V
⊢ Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ V)
have subst : Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ U)
Tactic: subst e
Cleared hypotheses: V, e
-- 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
⊢ Arrow.mk (f ∣_ U ∣_ V) ≅ Arrow.mk (X := (↑(f ⁻¹ᵁ U.ι ''ᵁ V) : Scheme)) (f ∣_ U.ι ''ᵁ V)
have refine_1 : (f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V = f ⁻¹ᵁ U.ι ''ᵁ V
Tactic: refine Arrow.isoMk' _ _ ((Scheme.Opens.ι _).isoImage _ ≪≫ Scheme.isoOfEq _ ?_)
    ((Scheme.Opens.ι _).isoImage _) ?_
-- 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_1 : (f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V = f ⁻¹ᵁ U.ι ''ᵁ V
⊢ Arrow.mk (f ∣_ U ∣_ V) ≅ Arrow.mk (X := (↑(f ⁻¹ᵁ U.ι ''ᵁ V) : Scheme)) (f ∣_ U.ι ''ᵁ V)
have refine_2 : (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq sorry).hom ≫ f ∣_ U.ι ''ᵁ V =
  f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)
Tactic: refine Arrow.isoMk' _ _ ((Scheme.Opens.ι _).isoImage _ ≪≫ Scheme.isoOfEq _ ?_)
    ((Scheme.Opens.ι _).isoImage _) ?_
-- 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
⊢ (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 : ((Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq sorry).hom ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
  (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
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).ι
⊢ (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₁ : ((Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq sorry).hom) ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
  (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
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).ι
⊢ (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₂ : (Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq sorry).hom) ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
  (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
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).ι
⊢ (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₃ : Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq sorry).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
  (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
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).ι
⊢ (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₄ : Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq sorry).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
  f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
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).ι
⊢ (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₅ : Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq sorry).hom ≫ (f ⁻¹ᵁ U.ι ''ᵁ V).ι ≫ f =
  f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
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).ι
⊢ (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₆ : 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).ι
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).ι
⊢ (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 ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
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_ι]