awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
            (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
      f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }
⊢ P
    (PreZeroHypercover.f
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
              (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
        PreZeroHypercover.{u_1, u, u + 1} W }
      j)
have refine_2 : P (X :=
  (pullback (X := OverClass.asOver (𝒰.X j) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
      (Hom.asOver (𝒰.f j) S) (Hom.asOver f S)).left)
  (Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f j) S) (Hom.asOver f S)))
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
            (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
      f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }
⊢ P (X :=
    (pullback (X := OverClass.asOver (𝒰.X j) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
        (Hom.asOver (𝒰.f j) S) (Hom.asOver f S)).left)
    (Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f j) S) (Hom.asOver f S)))
have refine_2 : P (X :=
  pullback (X := Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver (𝒰.X j) S)) (Y :=
    Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver W S)) (Z :=
    Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver X S))
    (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S))
    (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S)))
  (pullback.snd (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S))
    (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S)))
Tactic: rw [← Over.forget_map, ← PreservesPullback.iso_hom_snd, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
      f := fun (x : 𝒰.I₀) ↦
        CommaMorphism.left
          (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
            (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) }
⊢ P
    (PreZeroHypercover.f
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
              (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
                X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
        f := fun (x : 𝒰.I₀) ↦
          CommaMorphism.left
            (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
              (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) :
        PreZeroHypercover.{u_1, u, u + 1} W }
      j)
have refine_2 : P (X :=
  (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
      (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X j).asOverProp (P := Q) S sorry) (Z :=
        X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S))).left)
  (Y := W)
  (CategoryTheory.Functor.map (Over.forget S)
      (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
        (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S))) :
    Functor.obj (Over.forget S)
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
          (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X j).asOverProp (P := Q) S sorry) (Z :=
            X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S))) ⟶
      Functor.obj (Over.forget S) (W.asOver S))
Tactic: simp only [← CategoryTheory.Over.forget_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
      f := fun (x : 𝒰.I₀) ↦
        CommaMorphism.left
          (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
            (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) }
⊢ P (X :=
    (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
        (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X j).asOverProp (P := Q) S ⋯) (Z :=
          X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S))).left)
    (Y := W)
    (CategoryTheory.Functor.map (Over.forget S)
        (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
          (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S))) :
      Functor.obj (Over.forget S)
          (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X j).asOverProp (P := Q) S ⋯) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S))) ⟶
        Functor.obj (Over.forget S) (W.asOver S))
have refine_2 : P (X :=
  (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
      (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X j).asOverProp (P := Q) S sorry) (Z :=
        X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S))).left)
  (Y := W)
  (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
      (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S)) :
    Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X j).asOverProp (P := Q) S sorry) (Z :=
          X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S)) ⟶
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (W.asOverProp (P := Q) S hW))
Tactic: rw [MorphismProperty.Comma.toCommaMorphism_eq_hom,
        ← MorphismProperty.Comma.forget_map, ← Functor.comp_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))).left,
      f := fun (x : 𝒰.I₀) ↦
        CommaMorphism.left
          (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
            (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) }
⊢ P
    (PreZeroHypercover.f
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
              (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
                X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))).left,
        f := fun (x : 𝒰.I₀) ↦
          CommaMorphism.left
            (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
              (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) :
        PreZeroHypercover.{u_1, u, u + 1} W }
      j)
have refine_2 : P (X :=
  (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
      (pullback (X := (𝒰.X j).asOverProp (P := Q) S sorry) (Y := W.asOverProp (P := Q) S hW) (Z :=
        X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))).left)
  (Y := W)
  (CategoryTheory.Functor.map (Over.forget S)
      (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
        (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))) :
    Functor.obj (Over.forget S)
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
          (pullback (X := (𝒰.X j).asOverProp (P := Q) S sorry) (Y := W.asOverProp (P := Q) S hW) (Z :=
            X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))) ⟶
      Functor.obj (Over.forget S) (W.asOver S))
Tactic: simp only [← CategoryTheory.Over.forget_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))).left,
      f := fun (x : 𝒰.I₀) ↦
        CommaMorphism.left
          (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
            (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) }
⊢ P (X :=
    (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
        (pullback (X := (𝒰.X j).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
          X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))).left)
    (Y := W)
    (CategoryTheory.Functor.map (Over.forget S)
        (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
          (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))) :
      Functor.obj (Over.forget S)
          (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := (𝒰.X j).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))) ⟶
        Functor.obj (Over.forget S) (W.asOver S))
have refine_2 : P (X :=
  (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
      (pullback (X := (𝒰.X j).asOverProp (P := Q) S sorry) (Y := W.asOverProp (P := Q) S hW) (Z :=
        X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))).left)
  (Y := W)
  (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
      (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S)) :
    Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (pullback (X := (𝒰.X j).asOverProp (P := Q) S sorry) (Y := W.asOverProp (P := Q) S hW) (Z :=
          X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S)) ⟶
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (W.asOverProp (P := Q) S hW))
Tactic: rw [MorphismProperty.Comma.toCommaMorphism_eq_hom,
        ← MorphismProperty.Comma.forget_map, ← Functor.comp_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
inst_2 : P.IsStableUnderComposition
X_1 : Scheme
𝒰_1 : Cover (precoverage P) X_1
𝒱_1 : (x : 𝒰_1.I₀) → Cover.{?u.103208, u} (precoverage P) (𝒰_1.X x)
inst_3 : X_1.Over S
inst_4 : Cover.Over S (P := P) 𝒰_1
inst_5 : (x : 𝒰_1.I₀) → Cover.Over S (P := P) (𝒱_1 x)
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
𝒱 : (x : 𝒰.I₀) → Cover.{u_2, u} (precoverage P) (𝒰.X x)
inst_6 : X.Over S
inst_7 : Cover.Over S (P := P) 𝒰
inst_8 : (x : 𝒰.I₀) → Cover.Over S (P := P) (𝒱 x)
x : (Precoverage.ZeroHypercover.bind 𝒰 𝒱).I₀
i : 𝒰.I₀
j : PreZeroHypercover.I₀.{u_2, u, u + 1} (C := Scheme) (S := 𝒰.X i) ((fun (i : 𝒰.I₀) ↦ (𝒱 i).toPreZeroHypercover) i)
⊢ (Precoverage.ZeroHypercover.bind 𝒰 𝒱).f
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀.{u_2, u, u + 1} (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦ (𝒱 i).toPreZeroHypercover) i))
          i j) ≫
      X ↘ S =
    (Precoverage.ZeroHypercover.bind 𝒰 𝒱).X
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀.{u_2, u, u + 1} (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦ (𝒱 i).toPreZeroHypercover) i))
          i j) ↘
      S
have simp : (𝒱 i).X j ↘ S = (𝒱 i).X j ↘ S
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)
have obtain : ∀ (Us : Set (TopologicalSpace.Opens ↥S)) (hUs : Us ⊆ S.affineOpens) (hUf : Us.Finite) (hUc : U = sSup Us),
  IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)
Tactic: obtain ⟨Us, hUs, hUf, hUc⟩ := S.isBasis_affineOpens.exists_finite_of_isCompact hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
Us : Set (TopologicalSpace.Opens ↥S)
hUs : Us ⊆ S.affineOpens
hUf : Us.Finite
hUc : U = sSup Us
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)
have refine : ∀ t ∈ SetLike.coe '' Us, IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) t
Tactic: refine .of_biUnion_eq_of_finite (SetLike.coe '' Us) (by simp_all) (hUf.image _) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
⊢ ∃ (n : ℕ) (f : Fin n → 𝒰.I₀) (V : (i : Fin n) → (𝒰.X (f i)).Opens),
    (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ (i : Fin n), ⇑(𝒰.f (f i)) '' (↑(V i) : Set ↥(𝒰.X (f i))) = (↑U : Set ↥S)
have obtain : ∀ (n : ℕ) (a : Fin n → 𝒰.I₀) (V : (i : Fin n) → TopologicalSpace.Opens ↥(𝒰.X (a i)))
  (ha : ∀ (i : Fin n), Membership.mem (γ := Set (TopologicalSpace.Opens ↥(𝒰.X (a i)))) (𝒰.X (a i)).affineOpens (V i))
  (heq : ⋃ (i : Fin n), ⇑(𝒰.f (a i)) '' (↑(V i) : Set ↥(𝒰.X (a i))) = (↑U : Set ↥S)),
  ∃ (n : ℕ) (f : Fin n → 𝒰.I₀) (V : (i : Fin n) → (𝒰.X (f i)).Opens),
    (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ (i : Fin n), ⇑(𝒰.f (f i)) '' (↑(V i) : Set ↥(𝒰.X (f i))) = (↑U : Set ↥S)
Tactic: obtain ⟨n, a, V, ha, heq⟩ := (isCompactOpenCovered_of_isCompact 𝒰 hU).exists_mem_of_isBasis
    (fun i ↦ (𝒰.X i).isBasis_affineOpens) (fun _ _ h ↦ h.isCompact)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
𝒱 : PreZeroHypercover.{w', u, u + 1} S
f : 𝒱.Hom 𝒰
inst : QuasiCompactCover 𝒱
⊢ QuasiCompactCover 𝒰
have refine : ∀ {U : S.Opens} (hU : IsAffineOpen U),
  IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)
Tactic: refine ⟨fun {U} hU ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
⊢ QuasiCompactCover (PreZeroHypercover.pullback₁ f 𝒰)
have refine : ∀ {U' : T.Opens} (hU' : IsAffineOpen U'),
  IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
Tactic: refine ⟨fun {U'} hU' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
have inr : ∀
  (this :
    ∀ {U' : T.Opens} (hU' : IsAffineOpen U')
      (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
      IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
        ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
        (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T))
  (h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
  IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
Tactic: wlog h : ∃ (U : S.Opens), IsAffineOpen U ∧ f '' U' ⊆ U generalizing U'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
inr :
  ∀
    (this :
      ∀ {U' : T.Opens} (hU' : IsAffineOpen U')
        (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
        IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
          ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
          (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T))
    (h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
have wlog : ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
  IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
Tactic: wlog h : ∃ (U : S.Opens), IsAffineOpen U ∧ f '' U' ⊆ U generalizing U'
Cleared hypotheses: U', hU'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
this :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
have inr : ∀ (x : ↥T) (hxU : x ∈ (↑U' : Set ↥T)),
  ∃ t ⊆ (↑U' : Set ↥T),
    x ∈ t ∧
      IsOpen t ∧
        IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
          ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
          (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t
Tactic: refine .of_isCompact_of_forall_exists_isCompactOpenCovered hU'.isCompact fun x hxU ↦ ?_