awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P = @IsAffineHom ⊓ P'
have rw : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Tactic: rw [HasAffineProperty.eq_targetAffineLocally (P := P),
    targetAffineLocally_affineAnd_eq_affineLocally,
    HasRingHomProperty.eq_affineLocally (P := P')]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
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
R S : CommRingCat
f : R ⟶ S
⊢ P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
have this : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
Tactic: have := RingHom.toMorphismProperty_respectsIso_iff.mp hQi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
have rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))) ↔ Q (CommRingCat.Hom.hom f)
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := P), affineAnd, and_iff_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))) ↔ Q (CommRingCat.Hom.hom f)
⊢ P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
have rw₁ : IsAffine.{u} (Spec S)
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := P), affineAnd, and_iff_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hP' : HasAffineProperty P' (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
⊢ P ≤ P'
have rw : targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ≤
  targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')
Tactic: rw [HasAffineProperty.eq_targetAffineLocally (P := P),
    HasAffineProperty.eq_targetAffineLocally (P := P')]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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 : P f
hg : P g
⊢ P (X := U ⨿ V) (Limits.coprod.desc f g)
have have : ∀ (this : IsAffineHom f), P (X := U ⨿ V) (Limits.coprod.desc f g)
Tactic: have := HasAffineProperty.affineAnd_le_isAffineHom P hP f hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
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 : P f
hg : P g
this : IsAffineHom f
⊢ P (X := U ⨿ V) (Limits.coprod.desc f g)
have this₁ : IsAffineHom g
Tactic: have := HasAffineProperty.affineAnd_le_isAffineHom P hP g hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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 : P f
hg : P g
this_1 : IsAffineHom f
this : IsAffineHom g
⊢ P (X := U ⨿ V) (Limits.coprod.desc f g)
have rw : ∀ (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 : IsAffineHom f) (this : IsAffineHom g) (U_1 : X.Opens),
  IsAffineOpen U_1 →
    IsAffineOpen (X := U ⨿ V) (Limits.coprod.desc f g ⁻¹ᵁ U_1) ∧
      Q (S := (↑Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ U_1) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app (Limits.coprod.desc f g) U_1))
Tactic: rw [HasAffineProperty.eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi] at hf hg ⊢
Cleared hypotheses: hf, hg, this_1, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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 : IsAffineHom g
⊢ ∀ (U_1 : X.Opens),
    IsAffineOpen U_1 →
      IsAffineOpen (X := U ⨿ V) (Limits.coprod.desc f g ⁻¹ᵁ U_1) ∧
        Q (S := (↑Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ U_1) : Type u))
          (CommRingCat.Hom.hom (Scheme.Hom.app (Limits.coprod.desc f g) U_1))
have refine : ∀ (W : X.Opens) (hW : IsAffineOpen W),
  Q (S := (↑Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app (Limits.coprod.desc f g) W))
Tactic: refine fun W hW ↦ ⟨hW.preimage _, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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 : 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 ⋯)))
⊢ Q (S := (↑Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app (Limits.coprod.desc f g) W))
have rw : Q
  (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: rw [← hQi.cancel_right_isIso _ e.hom,
    ← CommRingCat.hom_comp, ← hQi.cancel_right_isIso _
    ((Limits.limit.isLimit _).conePointUniqueUpToIso (CommRingCat.prodFanIsLimit _ _)).hom,
    ← CommRingCat.hom_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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 : 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 ⋯)))
⊢ Q
    (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)))))
have have : ∀
  (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),
  Q
    (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 {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S × T) :
      Q (.comp (.fst _ _) f) → Q (.comp (.snd _ _) f) → Q f :=
    hQ (.comp (.fst _ _) f) (.comp (.snd _ _) f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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
⊢ Q
    (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)))))
have refine_1 : Q
  (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))))))
Tactic: refine this _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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_1 :
  Q
    (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))))))
⊢ Q
    (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)))))
have refine_2 : 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: refine this _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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
⊢ Q
    (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))))))
have refine_1 : ∀ (this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.fst = Scheme.Hom.app f W),
  Q
    (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))))))
Tactic: have : (Limits.coprod.desc f g).app W ≫ e.hom ≫ Limits.prod.fst = f.app W := by
      simp [e, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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
⊢ Q
    (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))))))
have h : 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: convert! (hf W hW).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
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
⊢ 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))))))
have 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))))))
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]