awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
⊢ U.ι ''ᵁ (↑U : Scheme).basicOpen r =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r)
have refine : X.basicOpen (U := X.ofRestrict sorry ''ᵁ ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X.restrict sorry, ⊤)) (Y := Γ(X, X.ofRestrict sorry ''ᵁ ⊤))
          (Iso.inv (Hom.appIso (X.ofRestrict sorry) ⊤)) :
        (a : (↑Γ(X.restrict sorry, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict sorry ''ᵁ ⊤) : Type u))
      r) =
  X.basicOpen (U := U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
      r)
Tactic: refine (Scheme.image_basicOpen (X.ofRestrict U.isOpenEmbedding) r).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
⊢ X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r)
have rw : X.basicOpen (U := X.ofRestrict sorry ''ᵁ ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X.restrict sorry, ⊤)) (Y := Γ(X, X.ofRestrict sorry ''ᵁ ⊤))
          (Iso.inv (Hom.appIso (X.ofRestrict sorry) ⊤)) :
        (a : (↑Γ(X.restrict sorry, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict sorry ''ᵁ ⊤) : Type u))
      r) =
  X.basicOpen (U := sorry.functor.obj ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, sorry.functor.obj ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
            (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
          r :
        (↑Γ(X, U) : Type u)))
Tactic: rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.isOpenEmbedding_obj_top).op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
⊢ X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := ⋯.functor.obj ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, ⋯.functor.obj ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
              (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
            r :
          (↑Γ(X, U) : Type u)))
have rw : X.basicOpen (U := X.ofRestrict sorry ''ᵁ ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X.restrict sorry, ⊤)) (Y := Γ(X, X.ofRestrict sorry ''ᵁ ⊤))
          (Iso.inv (Hom.appIso (X.ofRestrict sorry) ⊤)) :
        (a : (↑Γ(X.restrict sorry, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict sorry ''ᵁ ⊤) : Type u))
      r) =
  X.basicOpen (U := sorry.functor.obj ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (𝟙 (op (sorry.functor.obj ⊤)))) :
        (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, sorry.functor.obj ⊤) : Type u))
      r)
Tactic: rw [← CommRingCat.comp_apply, ← CategoryTheory.Functor.map_comp, ← op_comp, eqToHom_trans,
    eqToHom_refl, op_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
⊢ X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := ⋯.functor.obj ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤)))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, ⋯.functor.obj ⊤) : Type u))
        r)
have e_f : Iso.inv (Hom.appIso (X.ofRestrict sorry) ⊤) = X.presheaf.map (𝟙 (op (sorry.functor.obj ⊤)))
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
⊢ U.ι ''ᵁ (↑U : Scheme).basicOpen r = X.basicOpen r
have rw : X.basicOpen (U := U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
      r) =
  X.basicOpen r
Tactic: rw [Scheme.Opens.ι_image_basicOpen', Scheme.basicOpen_res_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
rw :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r) =
    X.basicOpen r
⊢ U.ι ''ᵁ (↑U : Scheme).basicOpen r = X.basicOpen r
have rw₁ : X.basicOpen r = X.basicOpen r
Tactic: rw [Scheme.Opens.ι_image_basicOpen', Scheme.basicOpen_res_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
          r) =
    X.basicOpen r
have simp : U.ι ''ᵁ
    (↑U : Scheme).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) U.topIso.inv :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
        r) =
  X.basicOpen r
Tactic: simp only [Scheme.Opens.toScheme_presheaf_obj]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
          r) =
    X.basicOpen r
have rw : X.basicOpen (U := U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
          r :
        (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))) =
  X.basicOpen r
Tactic: rw [ι_image_basicOpen', basicOpen_res_eq, topIso_inv, basicOpen_res_eq X]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
rw :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) U.topIso.inv :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
            r :
          (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))) =
    X.basicOpen r
⊢ U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
          r) =
    X.basicOpen r
have rw₁ : X.basicOpen (U := U.ι ''ᵁ ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) U.topIso.inv :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
      r) =
  X.basicOpen r
Tactic: rw [ι_image_basicOpen', basicOpen_res_eq, topIso_inv, basicOpen_res_eq X]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
rw :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) U.topIso.inv :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
            r :
          (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))) =
    X.basicOpen r
rw₁ :
  X.basicOpen (U := U.ι ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) U.topIso.inv :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen r
⊢ U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
          r) =
    X.basicOpen r
have rw₂ : X.basicOpen (U := U.ι ''ᵁ ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
      r) =
  X.basicOpen r
Tactic: rw [ι_image_basicOpen', basicOpen_res_eq, topIso_inv, basicOpen_res_eq X]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
rw :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) U.topIso.inv :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
            r :
          (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))) =
    X.basicOpen r
rw₁ :
  X.basicOpen (U := U.ι ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) U.topIso.inv :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen r
rw₂ :
  X.basicOpen (U := U.ι ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen r
⊢ U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
          r) =
    X.basicOpen r
have rw₃ : X.basicOpen r = X.basicOpen r
Tactic: rw [ι_image_basicOpen', basicOpen_res_eq, topIso_inv, basicOpen_res_eq X]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
V : (↑U : Scheme).Opens
r : (↑Γ((↑U : Scheme), V) : Type u)
x : ↥U
⊢ x ∈ (↑U : Scheme).basicOpen r ↔ (↑x : ↥X) ∈ X.basicOpen r
have rw : Membership.mem (γ := (↑U : Scheme).Opens)
    ((↑U : Scheme).basicOpen (U := U.ι ⁻¹ᵁ U.ι ''ᵁ V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V))
            ((↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
          (a : (↑Γ((↑U : Scheme), V) : Type u)) → (↑Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V) : Type u))
        r))
    x ↔
  (↑x : ↥X) ∈ X.basicOpen r
Tactic: rw [← U.toScheme.basicOpen_res_eq _ (eqToHom (U.ι.preimage_image_eq V)).op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
⊢ X.homOfLE ⋯ = 𝟙 (↑U : Scheme)
have rw : X.homOfLE sorry ≫ U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
Tactic: rw [← cancel_mono U.ι, Scheme.homOfLE_ι, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
rw : X.homOfLE ⋯ ≫ U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
⊢ X.homOfLE ⋯ = 𝟙 (↑U : Scheme)
have rw₁ : U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
Tactic: rw [← cancel_mono U.ι, Scheme.homOfLE_ι, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
rw : X.homOfLE ⋯ ≫ U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
rw₁ : U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
⊢ X.homOfLE ⋯ = 𝟙 (↑U : Scheme)
have rw₂ : U.ι = U.ι
Tactic: rw [← cancel_mono U.ι, Scheme.homOfLE_ι, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯
have rw : (X.homOfLE e₁ ≫ X.homOfLE e₂) ≫ W.ι = X.homOfLE sorry ≫ W.ι
Tactic: rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
rw : (X.homOfLE e₁ ≫ X.homOfLE e₂) ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯
have rw₁ : X.homOfLE e₁ ≫ X.homOfLE e₂ ≫ W.ι = X.homOfLE sorry ≫ W.ι
Tactic: rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
rw : (X.homOfLE e₁ ≫ X.homOfLE e₂) ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
rw₁ : X.homOfLE e₁ ≫ X.homOfLE e₂ ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯
have rw₂ : X.homOfLE e₁ ≫ V.ι = X.homOfLE sorry ≫ W.ι
Tactic: rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
rw : (X.homOfLE e₁ ≫ X.homOfLE e₂) ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
rw₁ : X.homOfLE e₁ ≫ X.homOfLE e₂ ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
rw₂ : X.homOfLE e₁ ≫ V.ι = X.homOfLE ⋯ ≫ W.ι
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯
have rw₃ : U.ι = X.homOfLE sorry ≫ W.ι
Tactic: rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
rw : (X.homOfLE e₁ ≫ X.homOfLE e₂) ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
rw₁ : X.homOfLE e₁ ≫ X.homOfLE e₂ ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
rw₂ : X.homOfLE e₁ ≫ V.ι = X.homOfLE ⋯ ≫ W.ι
rw₃ : U.ι = X.homOfLE ⋯ ≫ W.ι
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯
have rw₄ : U.ι = U.ι
Tactic: rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ (X.homOfLE e).base = CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e)
have w : ∀ (a : ↥(↑U : Scheme)),
  Eq (α := ↥(↑V : Scheme)) ((X.homOfLE e) a : ↥(↑V : Scheme))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
              (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
                Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                  Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
            C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
          (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
        a :
      ↥(↑V : Scheme))
Tactic: ext a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↥(↑U : Scheme)
⊢ Eq (α := ↥(↑V : Scheme)) ((X.homOfLE e) a : ↥(↑V : Scheme))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
              (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
                Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                  Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
            C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
          (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
        a :
      ↥(↑V : Scheme))
have w : Eq.{u + 1} (α := ↥X) (↑((X.homOfLE e) a) : ↥X)
  (↑(((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
              (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
                Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                  Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
            C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
          (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
        a) :
    ↥X)
Tactic: refine Subtype.ext ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥X
hx : x ∈ U
⊢ (X.homOfLE e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) = Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯
have rw : ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
          (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
          (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
            Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
              Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
        C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
      (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
    (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) =
  Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x sorry
Tactic: rw [homOfLE_base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
⊢ (↑((X.homOfLE e) x) : ↥X) = (↑x : ↥X)
have rw : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) (↑x : ↥X) sorry) : ↥X) = (↑x : ↥X)
Tactic: rw [Scheme.homOfLE_apply']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
x : ↥X
⊢ x ∈ (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X)
have h : x ∈ (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X) → x ∈ (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
x : ↥X
h : x ∈ (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X) → x ∈ (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X)
⊢ x ∈ (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X)
have h₁ : x ∈ (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X) → x ∈ (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (hypothesis)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
have e₁ : Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
  (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
  (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: have e₁ := Scheme.Hom.congr_app (X.homOfLE_ι e) (V.ι ''ᵁ W)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (hypothesis)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
have this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
Tactic: have : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W := W.map_functor_eq (U := V)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (hypothesis)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
have e₂ : (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
  Hom.app (X.homOfLE e) W ≫
    (↑U : Scheme).presheaf.map
      ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op
Tactic: have e₂ := (X.homOfLE e).naturality (eqToIso this).hom.op