-- Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
theorem HasAffineProperty.diagonal_of_diagonal_of_isPullback
    (P) {Q} [HasAffineProperty P Q]
    {X Y U V : Scheme.{u}} {f : X ⟶ Y} {g : U ⟶ Y}
    [IsAffine U] [IsOpenImmersion g]
    {iV : V ⟶ X} {f' : V ⟶ U} (h : IsPullback iV f' f g) (H : P.diagonal f) :
    Q.diagonal f'

Proof state:
case h.e'_3.h
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
e_1✝ :
  pullback (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯) =
    pullback (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯)
e_2✝ :
  pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) = pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)
⊢ (pullbackDiagonalMapIso f g f₁ f₂).hom ≫ pullback.mapDesc f₁ f₂ (pullback.snd f g) =
    pullback.snd (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯)

Tactic:
apply pullback.hom_ext <;> simp

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U V : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝¹ : IsAffine U
inst✝ : IsOpenImmersion g
iV : V ⟶ X
f' : V ⟶ U
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q.diagonal (pullback.snd f g)

Tactic:
rintro U V f₁ f₂ hU hV hf₁ hf₂

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ Q (pullback.mapDesc f₁ f₂ (pullback.snd f g))

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U V : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝¹ : IsAffine U
inst✝ : IsOpenImmersion g
iV : V ⟶ X
f' : V ⟶ U
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q.diagonal f'

Tactic:
rw [← Q.diagonal.cancel_left_of_respectsIso h.isoPullback.inv,
  h.isoPullback_inv_snd]

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U V : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝¹ : IsAffine U
inst✝ : IsOpenImmersion g
iV : V ⟶ X
f' : V ⟶ U
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q.diagonal (pullback.snd f g)

Proof state:
case convert_1
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsAffine (pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))

Tactic:
infer_instance

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U V : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝¹ : IsAffine U
inst✝ : IsOpenImmersion g
iV : V ⟶ X
f' : V ⟶ U
h : IsPullback iV f' f g
H : P.diagonal f
⊢ Q.diagonal f'

Tactic:
letI := isLocal_affineProperty P

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U V : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝¹ : IsAffine U
inst✝ : IsOpenImmersion g
iV : V ⟶ X
f' : V ⟶ U
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q.diagonal f'

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ Q (pullback.mapDesc f₁ f₂ (pullback.snd f g))

Tactic:
rw [← Q.cancel_left_of_respectsIso (pullbackDiagonalMapIso f _ f₁ f₂).hom]

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ Q ((pullbackDiagonalMapIso f g f₁ f₂).hom ≫ pullback.mapDesc f₁ f₂ (pullback.snd f g))

Proof state:
case convert_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsOpenImmersion
    (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g
      ⋯ ⋯)

Tactic:
infer_instance

Result:
no goals