awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this_3 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.fst = Scheme.Hom.app f W
⊢ RingHom.comp (RingHom.fst (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          Iso.hom
            (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))) =
    CommRingCat.Hom.hom (Scheme.Hom.app f W)

Tactic:
congr(($this).1)

Premises used: congrArg, id, CommRingCat.Hom.hom'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this_3 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.fst = Scheme.Hom.app f W
⊢ RingHom.comp (RingHom.fst (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          Iso.hom
            (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))) =
    CommRingCat.Hom.hom (Scheme.Hom.app f W)

Tactic:
exact congr(($this).1)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
⊢ Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W

Tactic:
simp [e, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
refine_2 :
  ∀ (this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W),
    Q
      (RingHom.comp (RingHom.snd (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
        (CommRingCat.Hom.hom
          ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
            Iso.hom
              (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
                (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))))
⊢ Q
    (RingHom.comp (RingHom.snd (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          Iso.hom
            (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))))

Tactic:
have : (Limits.coprod.desc f g).app W ≫ e.hom ≫ Limits.prod.snd = g.app W := by
      simp [e, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this_3 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app g W))

Tactic:
(hg W hW).2

Premises used: And.right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this_3 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W
h :
  RingHom.comp (RingHom.snd (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          Iso.hom
            (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))) =
    CommRingCat.Hom.hom (Scheme.Hom.app g W)
⊢ Q
    (RingHom.comp (RingHom.snd (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          Iso.hom
            (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))))

Tactic:
convert! (hg W hW).2

Premises used: And.right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this_3 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W
⊢ RingHom.comp (RingHom.snd (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          Iso.hom
            (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))) =
    CommRingCat.Hom.hom (Scheme.Hom.app g W)

Tactic:
congr(($this).1)

Premises used: congrArg, id, CommRingCat.Hom.hom'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this_3 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W
⊢ RingHom.comp (RingHom.snd (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          Iso.hom
            (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))) =
    CommRingCat.Hom.hom (Scheme.Hom.app g W)

Tactic:
exact congr(($this).1)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ P f

Tactic:
of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) ?_

Premises used: AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
refine : ∀ (i : 𝒰.I₀), P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (𝒰.f i)) : Scheme)) (f ∣_ Scheme.Hom.opensRange (𝒰.f i))
⊢ P f

Tactic:
refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) ?_

Premises used: AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ ∀ (i : 𝒰.I₀), P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (𝒰.f i)) : Scheme)) (f ∣_ Scheme.Hom.opensRange (𝒰.f i))

Tactic:
fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h i)

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ ∀ (i : 𝒰.I₀), P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (𝒰.f i)) : Scheme)) (f ∣_ Scheme.Hom.opensRange (𝒰.f i))

Tactic:
exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h i)

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
UX UY : Scheme
iY : UY ⟶ Y
inst_1 : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
H : P f
⊢ P f'

Tactic:
MorphismProperty.IsLocalAtTarget.of_isPullback (Y.affineCover.add iY) .none h H

Premises used: AlgebraicGeometry.Scheme.Cover.add, CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback, Option.none, AlgebraicGeometry.Scheme.affineCover, Sum.elim
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
U : Y.Opens
⊢ P (f ∣_ U)

Tactic:
of_isPullback (isPullback_morphismRestrict f U).flip hf

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.flip, AlgebraicGeometry.isPullback_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
h :
  ∀ (x : ↥Y),
    x ∈ (↑(iSup (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U))) : Set ↥Y) ↔
      x ∈ (↑⊤ : Set ↥Y)
⊢ IsOpenCover.{u, u} (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
x : ↥Y
⊢ x ∈ (↑(iSup (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U))) : Set ↥Y) ↔
    x ∈ (↑⊤ : Set ↥Y)

Tactic:
simp [← hU]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
refine :
  ∀
    (i :
      (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
          (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).I₀),
    P (X :=
      pullback f
        ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
          i))
      (pullback.snd f
        ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
          i))
⊢ P f

Tactic:
refine (P.iff_of_zeroHypercover_target
    (Y.openCoverOfIsOpenCover (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr fun i ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
i :
  (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U))
      ⋯).I₀
obtain :
  ∀ (i : ι),
    P (X :=
      pullback (Y :=
        (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).X
          (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯))
        f
        ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
          (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯)))
      (pullback.snd f
        ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
          (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯)))
⊢ P (X :=
    pullback f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
        i))
    (pullback.snd f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
        i))

Tactic:
obtain ⟨_, i, rfl⟩ := i

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
i : ι
⊢ P (X :=
    pullback (Y :=
      (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).X
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯))
      f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯)))
    (pullback.snd f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯)))

Tactic:
(P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mp ?_

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, Iff.mp