awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
rw₅ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))).op
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₆ : Scheme.Hom.app f V =
  Scheme.Hom.app f V ≫
    Y.presheaf.map
      (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom sorry : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
          ((Opens.map f.base).map (eqToHom sorry))).op
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
rw₅ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))).op
rw₆ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (eqToHom ⋯))).op
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₇ : Scheme.Hom.app f V =
  Scheme.Hom.app f V ≫
    Y.presheaf.map
      (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom sorry : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
          (eqToHom sorry)).op
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
rw₅ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))).op
rw₆ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (eqToHom ⋯))).op
rw₇ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            (eqToHom ⋯)).op
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₈ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom sorry))
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
rw₅ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))).op
rw₆ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (eqToHom ⋯))).op
rw₇ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            (eqToHom ⋯)).op
rw₈ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₉ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom sorry)
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
rw₅ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))).op
rw₆ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (eqToHom ⋯))).op
rw₇ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            (eqToHom ⋯)).op
rw₈ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₉ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom ⋯)
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₁₀ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (𝟙 (op ((Opens.map f.base).obj V)))
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
rw₅ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))).op
rw₆ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (eqToHom ⋯))).op
rw₇ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            (eqToHom ⋯)).op
rw₈ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₉ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom ⋯)
rw₁₀ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (𝟙 (op ((Opens.map f.base).obj V)))
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₁₁ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ 𝟙 Γ(Y, f ⁻¹ᵁ V)
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
rw₅ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))).op
rw₆ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (eqToHom ⋯))).op
rw₇ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            (eqToHom ⋯)).op
rw₈ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₉ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom ⋯)
rw₁₀ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (𝟙 (op ((Opens.map f.base).obj V)))
rw₁₁ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ 𝟙 Γ(Y, f ⁻¹ᵁ V)
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₁₂ : Scheme.Hom.app f V = Scheme.Hom.app f V
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst : IsOpenImmersion iU
inst_1 : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
⊢ IsPullback g iU iV f
have h : g = e.inv ≫ pullback.fst iV f
Tactic: convert!
    (IsPullback.of_horiz_isIso
          (show CommSq e.inv iU (pullback.snd iV f) (𝟙 X) from ⟨by simp [e]⟩)).paste_horiz
      (IsPullback.of_hasPullback iV f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
H : IsOpenImmersion f_1
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
U : Y.Opens
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ (Scheme.Hom.opensRange f ⊓ U)
have rw : f ⁻¹ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ f ⁻¹ᵁ U
Tactic: rw [← f.image_preimage_eq_opensRange_inf, f.preimage_image_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
H : IsOpenImmersion f_1
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
U : Y.Opens
rw : f ⁻¹ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ f ⁻¹ᵁ U
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ (Scheme.Hom.opensRange f ⊓ U)
have rw₁ : f ⁻¹ᵁ U ≤ f ⁻¹ᵁ U
Tactic: rw [← f.image_preimage_eq_opensRange_inf, f.preimage_image_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, Scheme.Hom.opensRange f ⊓ U)) (Scheme.Hom.app f U ≫ Iso.hom (ΓIso f U))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have rw : Eq (α := Γ(Y, U) ⟶ Γ(Y, Scheme.Hom.opensRange f ⊓ U))
  (CategoryStruct.comp (Y := Y.presheaf.obj (op (Scheme.Hom.opensRange f ⊓ U)))
      (Y.presheaf.map (Quiver.Hom.op (homOfLE sorry))) (Iso.inv (ΓIso f U)) ≫
    Iso.hom (ΓIso f U))
  (Y.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [← map_ΓIso_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsIso f
have rw : IsOpenImmersion f ∧ Epi f.base
Tactic: rw [isIso_iff_isOpenImmersion_and_epi_base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsOpenImmersion f ∧ Epi f.base
have refine : Epi f.base
Tactic: refine ⟨inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Epi f.base
have rw : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ
Tactic: rw [TopCat.epi_iff_surjective, ← Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsOpenImmersion.RespectsIso
have hP : MorphismProperty.isomorphisms Scheme ≤ IsOpenImmersion
Tactic: apply MorphismProperty.respectsIso_of_isStableUnderComposition
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f
have hP : ∀ (hf : IsIso f), IsOpenImmersion f
Tactic: (hf : IsIso f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ f ''ᵁ X.basicOpen r =
    Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r)
have e : f ⁻¹ᵁ
    Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r) =
  X.basicOpen (U := f ⁻¹ᵁ f ''ᵁ U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(Y, f ''ᵁ U)) (Hom.app f (f ''ᵁ U)) :
        (a : (↑Γ(Y, f ''ᵁ U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r :
        (↑Γ(Y, f ''ᵁ U) : Type u)))
Tactic: have e := Scheme.preimage_basicOpen f ((f.appIso U).inv r)