-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
lemma isLocalAtTarget [P.IsMultiplicative]
    (hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f) :
    IsLocalAtTarget P where
  iff_of_openCover' {X Y} f 𝒰

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Scheme.Cover.pullbackCover 𝒰 f).J
⊢ P (Scheme.Cover.pullbackHom 𝒰 f i ≫ 𝒰.map i) ↔ P (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
constructor

Result:
case mp
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Scheme.Cover.pullbackCover 𝒰 f).J
⊢ P (Scheme.Cover.pullbackHom 𝒰 f i ≫ 𝒰.map i) → P (Scheme.Cover.pullbackHom 𝒰 f i)

case mpr
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Scheme.Cover.pullbackCover 𝒰 f).J
⊢ P (Scheme.Cover.pullbackHom 𝒰 f i) → P (Scheme.Cover.pullbackHom 𝒰 f i ≫ 𝒰.map i)

Proof state:
case mpr
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Scheme.Cover.pullbackCover 𝒰 f).J
⊢ P (Scheme.Cover.pullbackHom 𝒰 f i) → P (Scheme.Cover.pullbackHom 𝒰 f i ≫ 𝒰.map i)

Tactic:
exact fun H ↦ P.comp_mem _ _ H (of_isOpenImmersion _)

Result:
no goals

Proof state:
case mp
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Scheme.Cover.pullbackCover 𝒰 f).J
⊢ P (Scheme.Cover.pullbackHom 𝒰 f i ≫ 𝒰.map i) → P (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
exact hP _ _

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
⊢ P f ↔ ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
refine (iff_of_openCover (𝒰.pullbackCover f)).trans (forall_congr' fun i ↦ ?_)

Result:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Scheme.Cover.pullbackCover 𝒰 f).J
⊢ P ((Scheme.Cover.pullbackCover 𝒰 f).map i ≫ f) ↔ P (Scheme.Cover.pullbackHom 𝒰 f i)

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Scheme.Cover.pullbackCover 𝒰 f).J
⊢ P ((Scheme.Cover.pullbackCover 𝒰 f).map i ≫ f) ↔ P (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
rw [← Scheme.Cover.pullbackHom_map]

Result:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Scheme.Cover.pullbackCover 𝒰 f).J
⊢ P (Scheme.Cover.pullbackHom 𝒰 f i ≫ 𝒰.map i) ↔ P (Scheme.Cover.pullbackHom 𝒰 f i)