awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i : WalkingPair
⊢ Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init i))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
have left : Function.Injective (α :=
  (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
  (β :=
  (fun (X : Type u) ↦ X)
    ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.left)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init WalkingPair.left))) :
    (a :
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
      (fun (X : Type u) ↦ X)
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.left)))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i : WalkingPair
left :
  Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.left)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init WalkingPair.left))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.left)))
⊢ Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init i))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
have right : Function.Injective (α :=
  (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
  (β :=
  (fun (X : Type u) ↦ X)
    ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.right)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init WalkingPair.right))) :
    (a :
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
      (fun (X : Type u) ↦ X)
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.right)))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i j : WalkingSpan
t : i ⟶ j
⊢ IsOpenImmersion ((span f g).map t).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
have id : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
Tactic: obtain (a | (a | a)) := t
Cleared hypotheses: j, t
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i j : WalkingSpan
t : i ⟶ j
id : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ IsOpenImmersion ((span f g).map t).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
have init : IsOpenImmersion
  ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
Tactic: obtain (a | (a | a)) := t
Cleared hypotheses: i, j, t
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i j : WalkingSpan
t : i ⟶ j
id : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
init :
  IsOpenImmersion
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ IsOpenImmersion ((span f g).map t).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
have init₁ : IsOpenImmersion
  ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
Tactic: obtain (a | (a | a)) := t
Cleared hypotheses: i, j, t
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i : WalkingSpan
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
have id : IsOpenImmersion (MorphismProperty.Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤) (𝟙 ((span f g).obj i))).left
Tactic: simp only [WidePushoutShape.hom_id, CategoryTheory.Functor.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (hypothesis)
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
⊢ CreatesColimit F (MorphismProperty.Over.forget P ⊤ S)
have this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
Tactic: have : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S) :=
    hasColimit_of_created _ (Over.forget S)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
⊢ CreatesColimit F (MorphismProperty.Over.forget P ⊤ S)
have refine : P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom
Tactic: refine createsColimitOfFullyFaithfulOfIso
      { toComma := colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
        prop := ?_ } (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : Scheme.OpenCover.{u_1, u} (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion)
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
⊢ P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom
have rw : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) 𝒰]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
j : J
e : (colimit F).toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) :=
  preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
⊢ IsOpenImmersion (X := (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left) (Y :=
    (colimit F).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CategoryTheory.Functor.map (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (colimit.ι F j) :
      Functor.obj (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (F.obj j) ⟶
        Functor.obj (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (colimit F))
have rw : IsOpenImmersion (X := (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left) (Y :=
  colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
  (CategoryTheory.Functor.map (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (colimit.ι F j) ≫ e.hom :
    (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left ⟶
      colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
Tactic: rw [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _ e.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
j : J
e : (colimit F).toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) :=
  preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
⊢ IsOpenImmersion (X := (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left) (Y :=
    colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
    (CategoryTheory.Functor.map (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (colimit.ι F j) ≫ e.hom :
      (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left ⟶
        colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
have simp : IsOpenImmersion (Y := colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
  (colimit.ι (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) j)
Tactic: simp only [e, CategoryTheory.ι_preservesColimitIso_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (hypothesis)
Goal:
X : Scheme
P_1 : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P_1
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P_1.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P_1) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P_1 ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
P : MorphismProperty Scheme
inst_6 : IsZariskiLocalAtSource P
inst_7 : P.IsStableUnderBaseChange
inst_8 : P.HasOfPostcompProperty P
inst_9 : P.IsMultiplicative
n : ℕ
⊢ HasColimitsOfShape.{0, 0, u, u + 1} (Discrete (Fin n)) (P.CostructuredArrow ⊤ Scheme.Spec S)
have this : (MorphismProperty.commaObj Scheme.Spec (Functor.fromPUnit S) P).IsClosedUnderColimitsOfShape (Discrete (Fin n))
Tactic: have : (MorphismProperty.commaObj Scheme.Spec (.fromPUnit S) P).IsClosedUnderColimitsOfShape
        (Discrete (Fin n)) :=
      IsZariskiLocalAtSource.isClosedUnderColimitsOfShape_discrete _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X : Scheme
M N : X.Modules
f g : M ⟶ N
H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U
⊢ f = g
have h : f.val = g.val
Tactic: apply SheafOfModules.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X : Scheme
M N : X.Modules
f g : M ⟶ N
H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U
⊢ f.val = g.val
have h : ∀ (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) (x : (↑(M.val.obj U) : Type u)),
  Eq (α := (↑(N.val.obj U) : Type u))
    ((ModuleCat.Hom.hom (f.val.app U) : (a : (↑(M.val.obj U) : Type u)) → (↑(N.val.obj U) : Type u)) x :
      (↑(N.val.obj U) : Type u))
    ((ModuleCat.Hom.hom (g.val.app U) : (a : (↑(M.val.obj U) : Type u)) → (↑(N.val.obj U) : Type u)) x :
      (↑(N.val.obj U) : Type u))
Tactic: ext U x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X : Scheme
M N : X.Modules
φ : M ⟶ N
⊢ IsIso φ ↔ ∀ (U : X.Opens), IsIso (app φ U)
have rw : (∀ (X_1 : (TopologicalSpace.Opens ↥X)ᵒᵖ), IsIso (((toPresheaf X).map φ).app X_1)) ↔ ∀ (U : X.Opens), IsIso (app φ U)
Tactic: rw [← isIso_iff_of_reflects_iso _ (toPresheaf X), NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X : Scheme
M N : X.Modules
φ : M ⟶ N
U : X.Opens
inst : IsIso φ
⊢ Hom.app (inv φ) U = inv (Hom.app φ U)
have hom_inv_id : Hom.app φ U ≫ Hom.app (inv φ) U = 𝟙 Γ(M, U)
Tactic: apply IsIso.eq_inv_of_hom_inv_id
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
e₄ : pullback h ⋙ pullback (f ≫ g) ≅ pullback ((f ≫ g) ≫ h) := pullbackComp (f ≫ g) h
⊢ (pullbackComp f (g ≫ h)).inv ≫
      Functor.whiskerRight (pullbackComp g h).inv (pullback f) ≫
        ((pullback h).associator (pullback g) (pullback f)).hom ≫
          (pullback h).whiskerLeft (pullbackComp f g).hom ≫ (pullbackComp (f ≫ g) h).hom =
    eqToHom ⋯
have change : e₁.inv ≫ e₂.inv ≫ ((pullback h).associator (pullback g) (pullback f)).hom ≫ e₃.hom ≫ e₄.hom = eqToHom sorry
Tactic: change e₁.inv ≫ e₂.inv ≫ (Functor.associator _ _ _).hom ≫ e₃.hom ≫ e₄.hom = _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (hypothesis)
Goal:
X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
e₄ : pullback h ⋙ pullback (f ≫ g) ≅ pullback ((f ≫ g) ≫ h) := pullbackComp (f ≫ g) h
⊢ e₁.inv ≫ e₂.inv ≫ ((pullback h).associator (pullback g) (pullback f)).hom ≫ e₃.hom ≫ e₄.hom = eqToHom ⋯
have this : e₃.hom ≫ e₄.hom = ((pullback h).associator (pullback g) (pullback f)).inv ≫ e₂.hom ≫ e₁.hom
Tactic: have : e₃.hom ≫ e₄.hom = (Functor.associator _ _ _).inv ≫ e₂.hom ≫ e₁.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_assoc.{u}
      h.toRingCatSheafHom g.toRingCatSheafHom f.toRingCatSheafHom)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback (𝟙 Y) ⋙ pullback f ≅ pullback (f ≫ 𝟙 Y) := pullbackComp f (𝟙 Y)
e₂ : pullback (𝟙 Y) ⋙ pullback f ≅ 𝟭 Y.Modules ⋙ pullback f := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
e₃ : 𝟭 Y.Modules ⋙ pullback f ≅ pullback f := (pullback f).leftUnitor
⊢ (pullbackComp f (𝟙 Y)).inv ≫ Functor.whiskerRight (pullbackId Y).hom (pullback f) ≫ (pullback f).leftUnitor.hom =
    eqToHom ⋯
have change : e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom sorry
Tactic: change e₁.inv ≫ e₂.hom ≫ e₃.hom = _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback (𝟙 Y) ⋙ pullback f ≅ pullback (f ≫ 𝟙 Y) := pullbackComp f (𝟙 Y)
e₂ : pullback (𝟙 Y) ⋙ pullback f ≅ 𝟭 Y.Modules ⋙ pullback f := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
e₃ : 𝟭 Y.Modules ⋙ pullback f ≅ pullback f := (pullback f).leftUnitor
⊢ e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯
have this : e₁.hom = e₂.hom ≫ e₃.hom
Tactic: have : e₁.hom = e₂.hom ≫ e₃.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_id_comp.{u} f.toRingCatSheafHom)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
⊢ (pullbackComp (𝟙 X) f).inv ≫ (pullback f).whiskerLeft (pullbackId X).hom ≫ (pullback f).rightUnitor.hom = eqToHom ⋯
have change : e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom sorry
Tactic: change e₁.inv ≫ e₂.hom ≫ e₃.hom = _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
⊢ e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯
have this : e₁.hom = e₂.hom ≫ e₃.hom
Tactic: have : e₁.hom = e₂.hom ≫ e₃.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_comp_id.{u} f.toRingCatSheafHom)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ Eq (α :=
    X.ringCatSheaf ⟶
      Functor.obj
        (Functor.sheafPushforwardContinuous (𝟭 X.Opens) RingCat (Opens.grothendieckTopology ↥X)
          (Opens.grothendieckTopology ↥X))
        X.ringCatSheaf)
    (CategoryStruct.comp (Y :=
      Functor.obj
        ((Hom.opensFunctor (𝟙 X)).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
          (Opens.grothendieckTopology ↥X))
        X.ringCatSheaf)
      {
        hom :=
          Functor.whiskerRight
            { app := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) ↦ Iso.inv (Hom.appIso (𝟙 X) (Opposite.unop U)),
              naturality := ⋯ }
            (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              RingCat.carrier)) }
      (NatTrans.app
        (Functor.sheafPushforwardContinuousNatTrans (Iso.hom (NatIso.ofComponents (fun (x : X.Opens) ↦ eqToIso ⋯) ⋯))
          RingCat (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X))
        X.ringCatSheaf))
    (𝟙 X.ringCatSheaf)
have h : ∀ (x : (TopologicalSpace.Opens ↥X)ᵒᵖ),
  NatTrans.app
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y :=
          Functor.obj
            ((Hom.opensFunctor (𝟙 X)).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
              (Opens.grothendieckTopology ↥X))
            X.ringCatSheaf)
          {
            hom :=
              Functor.whiskerRight
                { app := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) ↦ Iso.inv (Hom.appIso (𝟙 X) (Opposite.unop U)),
                  naturality := sorry }
                (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier)) }
          (NatTrans.app
            (Functor.sheafPushforwardContinuousNatTrans
              (Iso.hom (NatIso.ofComponents (fun (x : X.Opens) ↦ eqToIso sorry) sorry)) RingCat (Opens.grothendieckTopology ↥X)
              (Opens.grothendieckTopology ↥X))
            X.ringCatSheaf)))
      x =
    (InducedCategory.Hom.hom (𝟙 X.ringCatSheaf)).app x
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Sheaf (goal)
Goal:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ CategoryStruct.comp (Y := M.presheaf.stalk (f x)) (M.presheaf.germ (f ''ᵁ Opposite.unop (Opposite.op U)) (f x) ⋯)
      (NatTrans.app (Iso.inv (restrictStalkNatIso f x)) M) =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU
have rw : ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
    NatTrans.app (𝟙 (restrictFunctor f ⋙ toPresheaf X ⋙ TopCat.Presheaf.stalkFunctor Ab x)) M =
  ((restrictFunctor f).obj M).presheaf.germ U x hxU
Tactic: rw [← germ_restrictStalkNatIso_hom_app f x M hxU, Category.assoc, ← NatTrans.comp_app,
    Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
⊢ tilde.map (𝟙 M) = 𝟙 (tilde M)
have H : ∀ (p : (Spec R).Opens) (x : (↑Γ(tilde M, p) : Type u)),
  Eq (α := (↑Γ(tilde M, p) : Type u))
    ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (tilde.map (𝟙 M)) p) :
          (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde M, p) : Type u))
        x :
      (↑Γ(tilde M, p) : Type u))
    ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (𝟙 (tilde M)) p) :
          (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde M, p) : Type u))
        x :
      (↑Γ(tilde M, p) : Type u))
Tactic: ext p x