awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ P.diagonal f
have i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
Tactic: have i1 : ∀ i, IsAffine (𝒱.X i) := fun i => by dsimp [𝒱]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
⊢ P.diagonal f
have apply : ∀ (i : 𝒱.toPreZeroHypercover.1),
  Q (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.diagonal f) 𝒱).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒱 (pullback.diagonal f) i :
      (Precoverage.ZeroHypercover.pullback₁ (pullback.diagonal f) 𝒱).X i ⟶ 𝒱.X i)
Tactic: apply of_openCover 𝒱
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U V : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsAffine U
inst_2 : IsOpenImmersion g
iV : V ⟶ X
f' : V ⟶ U
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
⊢ Q.diagonal f'
have rw : Q.diagonal (X := pullback f g) (pullback.snd f g)
Tactic: rw [← Q.diagonal.cancel_left_of_respectsIso h.isoPullback.inv,
    h.isoPullback_inv_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U_1 V_1 : Scheme
f : X ⟶ Y
g : U_1 ⟶ Y
inst_1 : IsAffine U_1
inst_2 : IsOpenImmersion g
iV : V_1 ⟶ X
f' : V_1 ⟶ U_1
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
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 (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
    (pullback.mapDesc f₁ f₂ (pullback.snd f g))
have rw : Q (X :=
  pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
    (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
      sorry sorry))
  (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
  (CategoryStruct.comp (Y := pullback f₁ f₂)
      (Iso.hom (pullbackDiagonalMapIso f g f₁ f₂) :
        pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
            (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 sorry sorry) ⟶
          pullback f₁ f₂)
      (pullback.mapDesc f₁ f₂ (pullback.snd f g) :
        pullback f₁ f₂ ⟶ pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) :
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
        (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 sorry sorry) ⟶
      pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
Tactic: rw [← Q.cancel_left_of_respectsIso (pullbackDiagonalMapIso f _ f₁ f₂).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
⊢ Q.diagonal f ↔ P.diagonal f
have refine : ∀ (hf : Q.diagonal f), P.diagonal f
Tactic: refine ⟨fun hf ↦ ?_, diagonal_of_diagonal_of_isPullback P .of_id_fst⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
hf : Q.diagonal f
⊢ P.diagonal f
have hf₁ : Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
Tactic: rw [← Q.diagonal.cancel_left_of_respectsIso
    (pullback.fst (f := f) (g := 𝟙 Y)), pullback.condition, Category.comp_id] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
hf : Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion) X.affineCover (inv (pullback.fst f (𝟙 Y)))
i : 𝒰.I₀
⊢ IsAffine.{u} (𝒰.X i)
have dsimp : IsAffine.{u}
  (X.affineCover.X
    (Sigma.snd (β := fun (i : PUnit.{u + 1}) ↦ X.affineCover.I₀)
      ((Equiv.trans (Equiv.symm (Equiv.punitProd X.affineCover.I₀))
            (Equiv.symm (Equiv.sigmaEquivProd PUnit.{u + 1} X.affineCover.I₀)) :
          (a : X.affineCover.I₀) → (_ : PUnit.{u + 1}) × X.affineCover.I₀)
        i)))
Tactic: dsimp [𝒰]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
hf : Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion) X.affineCover (inv (pullback.fst f (𝟙 Y)))
⊢ P.diagonal f
have this₁ : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
Tactic: have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
⊢ Q.diagonal f
have rw : (targetAffineLocally Q).diagonal f
Tactic: rw [HasAffineProperty.diagonal_iff (targetAffineLocally Q)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i : 𝒱.I₀
⊢ IsAffine.{u} (𝒱.X i)
have dsimp : IsAffine.{u} (pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f))
Tactic: dsimp [𝒱]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (hypothesis)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
⊢ (targetAffineLocally Q).diagonal f
have i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
Tactic: have i1 : ∀ i, IsAffine (𝒱.X i) := fun i => by dsimp [𝒱]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
⊢ (targetAffineLocally Q).diagonal f
have refine : ∀ (i : 𝒱.toPreZeroHypercover.1),
  Q (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.diagonal f) 𝒱).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒱 (pullback.diagonal f) i :
      (Precoverage.ZeroHypercover.pullback₁ (pullback.diagonal f) 𝒱).X i ⟶ 𝒱.X i)
Tactic: refine HasAffineProperty.of_openCover (P := targetAffineLocally Q) 𝒱 fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ Q (X :=
    pullback (Y := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))
    (pullback.snd (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))
have have : ∀
  (this :
    IsPullback (P := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
      pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
      (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
      (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) sorry sorry)),
  Q (X :=
    pullback (Y := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) sorry sorry))
    (pullback.snd (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) sorry sorry))
Tactic: have : IsPullback (pullback.fst _ _ ≫ 𝒰.f _) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)
      (pullback.diagonal f) (pullback.map _ _ _ _ (𝒰.f _) (𝒰.f _) (𝟙 Y) (by simp) (by simp)) :=
    .of_iso (pullback_fst_map_snd_isPullback f (𝟙 _) (𝒰.f i.1 ≫ pullback.lift (𝟙 _) f)
      (𝒰.f i.2 ≫ pullback.lift (𝟙 _) f)) (asIso (pullback.map _ _ _ _ (𝟙 _) (𝟙 _)
      (pullback.fst _ _) (by simp) (by simp))) (.refl _) (pullback.congrHom (by simp) (by simp))
      (.refl _) (by simp) (by cat_disch) (by simp) (by cat_disch)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
this :
  IsPullback (P := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
    pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
    (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
    (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)
⊢ Q (X :=
    pullback (Y := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))
    (pullback.snd (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))
have rw : Q (X := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
  pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)
Tactic: rw [← Q.cancel_left_of_respectsIso this.isoPullback.hom, IsPullback.isoPullback_hom_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
⊢ Q.diagonal f
have refine : (targetAffineLocally Q).diagonal f
Tactic: refine (diagonal_iff (targetAffineLocally Q)).mpr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (hypothesis)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun (f : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)) ↦ Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⋯
⊢ (targetAffineLocally Q).diagonal f
have this : ∀ (i : 𝒰.I₀), IsAffine.{u_1} (𝒰.X i)
Tactic: have (i : _) : IsAffine (𝒰.X i) := (isAffineOpen_top Y).basicOpen i.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun (f : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)) ↦ Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine.{u_1} (𝒰.X i)
⊢ (targetAffineLocally Q).diagonal f
have refine : ∀ (i : 𝒰.toPreZeroHypercover.1),
  Q.diagonal (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
Tactic: refine diagonal_of_openCover_diagonal (targetAffineLocally Q) f 𝒰 ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
⊢ P.diagonal = targetAffineLocally Q.diagonal
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y), P.diagonal f ↔ targetAffineLocally Q.diagonal f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ P.diagonal f ↔ targetAffineLocally Q.diagonal f
have h : P.diagonal f → targetAffineLocally Q.diagonal f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
h : P.diagonal f → targetAffineLocally Q.diagonal f
⊢ P.diagonal f ↔ targetAffineLocally Q.diagonal f
have h₁ : targetAffineLocally Q.diagonal f → P.diagonal f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
⊢ IsZariskiLocalAtSource.{u_1} P.diagonal
have refine_1 : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) (hf : P.diagonal f), P.diagonal (U.ι ≫ f)
Tactic: refine IsZariskiLocalAtSource.mk' (fun {X Y} f U hf ↦ ?_) (fun {X Y} f {ι} U hU hf ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
refine_1 : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) (hf : P.diagonal f), P.diagonal (U.ι ≫ f)
⊢ IsZariskiLocalAtSource.{u_1} P.diagonal
have refine_2 : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) {ι : Type u_1} (U : ι → X.Opens) (hU : iSup U = ⊤)
  (hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)), P.diagonal f
Tactic: refine IsZariskiLocalAtSource.mk' (fun {X Y} f U hf ↦ ?_) (fun {X Y} f {ι} U hU hf ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P.diagonal (U.ι ≫ f)
have refine_1 : P (Y := pullback.diagonalObj (U.ι ≫ f)) (pullback.diagonal (U.ι ≫ f))
Tactic: change P _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (Y := pullback.diagonalObj (U.ι ≫ f)) (pullback.diagonal (U.ι ≫ f))
have refine_1 : P (pullback.diagonal (U.ι ≫ f) ≫ g f U)
Tactic: apply P.of_postcomp (W' := @IsOpenImmersion) (pullback.diagonal (U.ι ≫ f)) (g f U) inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (pullback.diagonal (U.ι ≫ f) ≫ g f U)
have refine_1 : P (Y := pullback f f) (U.ι ≫ pullback.diagonal f)
Tactic: rw [← pullback.comp_diagonal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (Y := pullback f f) (U.ι ≫ pullback.diagonal f)
have refine_1 : P (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: apply IsZariskiLocalAtSource.comp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
⊢ P.diagonal f
have refine_2 : P (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: change P _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
⊢ P (Y := pullback.diagonalObj f) (pullback.diagonal f)
have refine_2 : ∀ (i : ι), P (Y := pullback.diagonalObj f) ((U i).ι ≫ pullback.diagonal f)
Tactic: refine IsZariskiLocalAtSource.of_iSup_eq_top U hU fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
i : ι
⊢ P (Y := pullback.diagonalObj f) ((U i).ι ≫ pullback.diagonal f)
have refine_2 : P (Y := pullback.diagonalObj f)
  (CategoryStruct.comp (Y := pullback.diagonalObj ((U i).ι ≫ f)) (pullback.diagonal ((U i).ι ≫ f))
    (pullback.map ((U i).ι ≫ f) ((U i).ι ≫ f) f f (U i).ι (U i).ι (𝟙 Y) sorry sorry))
Tactic: rw [pullback.comp_diagonal]