-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem iff_of_isAffine [IsAffine Y] : P f ↔ Q f

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
this : ∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).1), Q ((Scheme.coverOfIsIso (𝟙 Y)).pullbackHom f i)) ↔ Q f

Tactic:
trans Q (pullback.snd f (𝟙 _))

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
this : ∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).1), Q ((Scheme.coverOfIsIso (𝟙 Y)).pullbackHom f i)) ↔ Q (pullback.snd f (𝟙 Y))

P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
this : ∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)
⊢ Q (pullback.snd f (𝟙 Y)) ↔ Q f

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f ↔ Q f

Tactic:
haveI : ∀ i, IsAffine (Scheme.Cover.obj
    (Scheme.coverOfIsIso (P := @IsOpenImmersion) (𝟙 Y)) i) := fun i => by
  dsimp; infer_instance

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
this : ∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)
⊢ P f ↔ Q f

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
this : ∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)
⊢ P f ↔ Q f

Tactic:
rw [iff_of_openCover (P := P) (Scheme.coverOfIsIso.{0} (𝟙 Y))]

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
this : ∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).1), Q ((Scheme.coverOfIsIso (𝟙 Y)).pullbackHom f i)) ↔ Q f

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
i : (Scheme.coverOfIsIso (𝟙 Y)).J
⊢ IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)

Tactic:
dsimp

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
i : (Scheme.coverOfIsIso (𝟙 Y)).J
⊢ IsAffine Y

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
i : (Scheme.coverOfIsIso (𝟙 Y)).J
⊢ IsAffine Y

Tactic:
infer_instance

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
this : ∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)
⊢ Q (pullback.snd f (𝟙 Y)) ↔ Q f

Tactic:
rw [← Category.comp_id (pullback.snd _ _), ← pullback.condition,
  Q.cancel_left_of_respectsIso]

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ P f ↔ Q f

Tactic:
letI := isLocal_affineProperty P

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f ↔ Q f

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
this : ∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.coverOfIsIso (𝟙 Y)).obj i)
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).1), Q ((Scheme.coverOfIsIso (𝟙 Y)).pullbackHom f i)) ↔ Q (pullback.snd f (𝟙 Y))

Tactic:
exact ⟨fun H => H PUnit.unit, fun H _ => H⟩

Result:
no goals