awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
i : 𝒰.I₀
hf : P f
⊢ P (X := pullback f (𝒰.f i)) (pullback.fst f (𝒰.f i) ≫ f)

Tactic:
IsZariskiLocalAtSource.comp hf _

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
i : 𝒰.I₀
hf : P f
⊢ P (X := pullback f (𝒰.f i)) (pullback.fst f (𝒰.f i) ≫ f)

Tactic:
exact IsZariskiLocalAtSource.comp hf _

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
rw : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀), P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)
⊢ P f

Tactic:
rw [P.iff_of_zeroHypercover_source (𝒰.pullback₁ f)]

Premises used: CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source, CategoryTheory.Precoverage.ZeroHypercover.pullback₁
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
rw :
  P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i ≫ 𝒰.f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ Y)
⊢ P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)

Tactic:
rw [← Scheme.Cover.pullbackHom_map]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i ≫ 𝒰.f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ Y)

Tactic:
P.comp_mem _ _ (h i) (of_isOpenImmersion _)

Premises used: CategoryTheory.MorphismProperty.comp_mem, AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i ≫ 𝒰.f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ Y)

Tactic:
exact P.comp_mem _ _ (h i) (of_isOpenImmersion _)

Premises used: CategoryTheory.MorphismProperty.comp_mem, AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X : Scheme
ι : Type v
inst_1 : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
hf : ∀ (i : ι), P (f i)
rw :
  ∀
    (i :
      PreZeroHypercover.I₀ (S := colimit (Discrete.functor Y))
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)) :
          PreZeroHypercover.{v, u, u + 1} (colimit (Discrete.functor Y)))),
    P (X :=
      PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y))) i)
      (CategoryStruct.comp (Y := colimit (Discrete.functor Y))
          (PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
              i :
            PreZeroHypercover.X
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
                i ⟶
              colimit (Discrete.functor Y))
          (Sigma.desc f : ∐ Y ⟶ X) :
        PreZeroHypercover.X
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
            i ⟶
          X)
⊢ P (X := ∐ Y) (Sigma.desc f)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Scheme.IsLocallyDirected.openCover _)]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.openCover, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X : Scheme
ι : Type v
inst_1 : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
hf : ∀ (i : ι), P (f i)
i :
  PreZeroHypercover.I₀ (S := colimit (Discrete.functor Y))
    (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)) :
      PreZeroHypercover.{v, u, u + 1} (colimit (Discrete.functor Y)))
⊢ P (X :=
    PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y))) i)
    (CategoryStruct.comp (Y := colimit (Discrete.functor Y))
        (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
            i :
          PreZeroHypercover.X
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
              i ⟶
            colimit (Discrete.functor Y))
        (Sigma.desc f : ∐ Y ⟶ X) :
      PreZeroHypercover.X
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y))) i ⟶
        X)

Tactic:
simp [hf]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X : Scheme
ι : Type v
inst_1 : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
hf : ∀ (i : ι), P (f i)
⊢ ∀
    (i :
      PreZeroHypercover.I₀ (S := colimit (Discrete.functor Y))
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)) :
          PreZeroHypercover.{v, u, u + 1} (colimit (Discrete.functor Y)))),
    P (X :=
      PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y))) i)
      (CategoryStruct.comp (Y := colimit (Discrete.functor Y))
          (PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
              i :
            PreZeroHypercover.X
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
                i ⟶
              colimit (Discrete.functor Y))
          (Sigma.desc f : ∐ Y ⟶ X) :
        PreZeroHypercover.X
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
            i ⟶
          X)

Tactic:
exact fun i ↦ by simp [hf]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
hf : P f
⊢ P (Scheme.Hom.resLE f U V e)

Tactic:
IsZariskiLocalAtSource.comp (IsZariskiLocalAtTarget.restrict hf U) _

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.IsZariskiLocalAtSource.comp, AlgebraicGeometry.Scheme.Hom.resLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
hf : P f
x : ↥X
⊢ ⊤ ≤ f ⁻¹ᵁ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
refine :
  ∀
    (hf :
      ∀ (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)),
    P f
⊢ P f ↔ ∀ (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)

Tactic:
refine ⟨fun hf x ↦ ⟨⊤, ⊤, trivial, by simp, resLE _ hf⟩, fun hf ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
hf : ∀ (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
choose :
  ∀ (U : (x : ↥X) → Y.Opens) (V : (x : ↥X) → X.Opens) (hxU : ∀ (x : ↥X), x ∈ (V x).carrier)
    (e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x) (hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)), P f
⊢ P f

Tactic:
choose U V hxU e hf using hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
rw : ∀ (i : ↥X), P ((V i).ι ≫ f)
rw₁ : Eq.{u + 1} (α := X.Opens) (⨆ (x : ↥X), V x) ⊤
⊢ P f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (fun x : X ↦ V x) (P := P)]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
rw : P (Scheme.Hom.resLE f (U x) (V x) ⋯ ≫ (U x).ι)
⊢ P ((V x).ι ≫ f)

Tactic:
rw [← Scheme.Hom.resLE_comp_ι _ (e x)]

Premises used: AlgebraicGeometry.Scheme.Hom.resLE_comp_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ P (Scheme.Hom.resLE f (U x) (V x) ⋯ ≫ (U x).ι)

Tactic:
MorphismProperty.RespectsRight.postcomp (Q := @IsOpenImmersion) _ inferInstance _ (hf x)

Premises used: inferInstance, CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
rw : LE.le.{u} (α := X.Opens) ⊤ (⨆ (x : ↥X), V x)
⊢ Eq.{u + 1} (α := X.Opens) (⨆ (x : ↥X), V x) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
simp : ∃ (i : ↥X), x ∈ V i
⊢ Membership.mem (γ := Opens ↥X) (⨆ (x : ↥X), V x) x

Tactic:
simp only [Opens.mem_iSup]

Premises used: TopologicalSpace.Opens.mem_iSup
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x w : ↥X
h : x ∈ V x
⊢ ∃ (i : ↥X), x ∈ V i

Tactic:
use x, hxU x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P Q : AffineTargetMorphismProperty
H h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1) (x_3 : IsAffine x_1), P x_2 ↔ Q x_2
⊢ P = Q

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
x x_1 : Scheme
x_2 : x ⟶ x_1
h : IsAffine x_1
⊢ P x_2 ↔ Q x_2

Tactic:
H _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
x x_1 : Scheme
x_2 : x ⟶ x_1
h : IsAffine x_1
⊢ P x_2 ↔ Q x_2

Tactic:
exact H _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ (∃ (h : IsAffine Y), P f) ↔ P f

Tactic:
simp [*]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsAffine Z
rw : P.toProperty (f ≫ g) ↔ P g
rw₁ : P.toProperty (f ≫ g) ↔ P.toProperty g
rw₂ rw₃ : P.toProperty g ↔ P.toProperty g
⊢ P (f ≫ g) ↔ P g

Tactic:
rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.cancel_left_of_respectsIso]

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.toProperty_apply, AlgebraicGeometry.AffineTargetMorphismProperty.toProperty, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
inst_2 : IsAffine Z
inst_3 : IsAffine Y
rw : P.toProperty (f ≫ g) ↔ P f
rw₁ : P.toProperty (f ≫ g) ↔ P.toProperty f
rw₂ rw₃ : P.toProperty f ↔ P.toProperty f
⊢ P (f ≫ g) ↔ P f

Tactic:
rw [← P.toProperty_apply, ← P.toProperty_apply,
      P.toProperty.cancel_right_of_respectsIso]

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.toProperty_apply, AlgebraicGeometry.AffineTargetMorphismProperty.toProperty, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
rw : P.toProperty f ↔ P f'
rw₁ : P.toProperty f ↔ P.toProperty f'
rw₂ rw₃ : P.toProperty f' ↔ P.toProperty f'
⊢ P f ↔ P f'

Tactic:
rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.arrow_mk_iso_iff e]

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.toProperty_apply, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.AffineTargetMorphismProperty.toProperty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), P.toProperty f → P.toProperty (e.hom ≫ f)
hpostcomp : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y), P.toProperty f → P.toProperty (f ≫ e.hom)
⊢ P.toProperty.RespectsIso

Tactic:
apply MorphismProperty.RespectsIso.mk

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
a : IsAffine Z
h : P f
⊢ P.toProperty (e.hom ≫ f)

Tactic:
⟨a, h₁ e f h⟩

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.toProperty, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
a : IsAffine Z
h : P f
⊢ P.toProperty (e.hom ≫ f)

Tactic:
exact ⟨a, h₁ e f h⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
a : IsAffine Y
h : P f
⊢ P.toProperty (f ≫ e.hom)

Tactic:
⟨.of_isIso e.inv, h₂ e f h⟩

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.AffineTargetMorphismProperty.toProperty, Exists.intro, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
a : IsAffine Y
h : P f
⊢ P.toProperty (f ≫ e.hom)

Tactic:
exact ⟨.of_isIso e.inv, h₂ e f h⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)
⊢ (of P).toProperty.RespectsIso

Tactic:
apply respectsIso_mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X : Scheme
h₁ : ∀ {Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
⊢ ∀ {Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y : Scheme
h₁ : ∀ {Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
⊢ ∀ {Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y Z : Scheme
h₁ : ∀ (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y Z : Scheme
e : X ≅ Y
h₁ : ∀ (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
⊢ ∀ (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
h₁ : ∀ [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
⊢ ∀ [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst_1 : IsAffine Z
⊢ of P f → of P (e.hom ≫ f)

Tactic:
apply MorphismProperty.RespectsIso.precomp

Premises used: CategoryTheory.MorphismProperty.RespectsIso.precomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X : Scheme
h₂ : ∀ {Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)
⊢ ∀ {Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y : Scheme
h₂ : ∀ {Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)
⊢ ∀ {Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y Z : Scheme
h₂ : ∀ (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
h₂ : ∀ (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)
⊢ ∀ (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
h₂ : ∀ [inst : IsAffine Y], of P f → of P (f ≫ e.hom)
⊢ ∀ [inst : IsAffine Y], of P f → of P (f ≫ e.hom)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst_1 : IsAffine Y
⊢ of P f → of P (f ≫ e.hom)

Tactic:
apply MorphismProperty.RespectsIso.postcomp

Premises used: CategoryTheory.MorphismProperty.RespectsIso.postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
H :
  ∀ ⦃X Y S : Scheme.{u_1}⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    P g → P (X := pullback f g) (pullback.fst f g)
Z X Y S : Scheme
_ :
  ∀ [inst : IsAffine S] [inst_1 : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X},
    IsPullback g' f' f g → P g → P g'
⊢ ∀ [inst : IsAffine S] [inst_1 : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X},
    IsPullback g' f' f g → P g → P g'

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
H :
  ∀ ⦃X Y S : Scheme.{u_1}⦄ [inst : IsAffine S] [inst_2 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    P g → P (X := pullback f g) (pullback.fst f g)
Z X Y S : Scheme
inst_1 : IsAffine S
_ : ∀ [inst : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X}, IsPullback g' f' f g → P g → P g'
⊢ ∀ [inst : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X}, IsPullback g' f' f g → P g → P g'

Tactic:
_