Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_1
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} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [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✝¹ : 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 (eqToIso ⋯).op) (Functor.mapIso V.presheaf (eqToIso ⋯).op)
this :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q ((RingHom.fst S T).comp f) → Q ((RingHom.snd S T).comp f) → Q f
⊢ Q
    ((RingHom.fst ↑Γ(U, f ⁻¹ᵁ W) ↑Γ(V, g ⁻¹ᵁ W)).comp
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          ((Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W))).conePointUniqueUpToIso
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))).hom)))

pp: case refine_2
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} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [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✝¹ : 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 (eqToIso ⋯).op) (Functor.mapIso V.presheaf (eqToIso ⋯).op)
this :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q ((RingHom.fst S T).comp f) → Q ((RingHom.snd S T).comp f) → Q f
⊢ Q
    ((RingHom.snd ↑Γ(U, f ⁻¹ᵁ W) ↑Γ(V, g ⁻¹ᵁ W)).comp
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          ((Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W))).conePointUniqueUpToIso
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))).hom)))

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]
    convert! (hf W hW).2
    exact congr(($this).1)

Goal state after:
case refine_2
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} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [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✝¹ : 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 (eqToIso ⋯).op) (Functor.mapIso V.presheaf (eqToIso ⋯).op)
this :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q ((RingHom.fst S T).comp f) → Q ((RingHom.snd S T).comp f) → Q f
⊢ Q
    ((RingHom.snd ↑Γ(U, f ⁻¹ᵁ W) ↑Γ(V, g ⁻¹ᵁ W)).comp
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          ((Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W))).conePointUniqueUpToIso
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))).hom)))