awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ Eq (α := Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G)
    ((let __Equiv :
            Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0 ≃
              (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G) :=
            Ext.homEquiv₀;
          { toEquiv := __Equiv, map_add' := ⋯ } :
          (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) G 0) →
            (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ G)
        ((map f 0 : (a : F.H 0) → G.H 0) x) :
      Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G)
    ((let __Equiv :
              Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) F 0 ≃
                (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ F) :=
              Ext.homEquiv₀;
            { toEquiv := __Equiv, map_add' := ⋯ } :
            (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) F 0) →
              (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ F)
          x ≫
        f :
      Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G)
have a : Eq.{w' + 1} (α := Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
  (Ext.mk₀
      ((let __Equiv :
            Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0 ≃
              (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G) :=
            Ext.homEquiv₀;
          { toEquiv := __Equiv, map_add' := sorry } :
          (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) G 0) →
            (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ G)
        ((map f 0 : (a : F.H 0) → G.H 0) x)) :
    Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
  (Ext.mk₀
      ((let __Equiv :
              Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) F 0 ≃
                (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ F) :=
              Ext.homEquiv₀;
            { toEquiv := __Equiv, map_add' := sorry } :
            (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) F 0) →
              (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ F)
          x ≫
        f) :
    Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
Tactic: apply (Ext.mk₀_bijective _ G).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ Eq.{w' + 1} (α := Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
    (Ext.mk₀
        ((let __Equiv :
              Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0 ≃
                (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G) :=
              Ext.homEquiv₀;
            { toEquiv := __Equiv, map_add' := ⋯ } :
            (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) G 0) →
              (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ G)
          ((map f 0 : (a : F.H 0) → G.H 0) x)) :
      Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
    (Ext.mk₀
        ((let __Equiv :
                Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) F 0 ≃
                  (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ F) :=
                Ext.homEquiv₀;
              { toEquiv := __Equiv, map_add' := ⋯ } :
              (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) F 0) →
                (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ F)
            x ≫
          f) :
      Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
have a : (map f 0 : (a : F.H 0) → G.H 0) x = Ext.comp x (Ext.mk₀ f) sorry
Tactic: simp only [AddEquiv.coe_mk, Ext.mk₀_homEquiv₀_apply, Ext.mk₀_homEquiv₀_apply, ← Ext.mk₀_comp_mk₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal.{v, u} T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ Eq (α := (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (X := F.obj (P := Presheaf.IsSheaf J).obj (op T)) (f.hom.app (op T)) :
          (a : (↑(F.obj.obj (op T)) : Type w)) → (↑(G.obj.obj (op T)) : Type w))
        ((equiv₀ F hT : (a : F.H 0) → (↑(F.obj.obj (op T)) : Type w)) x :
          (↑(F.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w)) :
      (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
    ((equiv₀ G hT : (a : G.H 0) → (↑(G.obj.obj (op T)) : Type w)) ((map f 0 : (a : F.H 0) → G.H 0) x) :
      (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [equiv₀, AddEquiv.trans_apply, addEquiv₀_map f x]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal.{v, u} T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : (↑(F.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w)
⊢ Eq (α := G.H 0)
    ((map f 0 : (a : F.H 0) → G.H 0)
        ((AddEquiv.symm (equiv₀ F hT) : (a : (↑(F.obj.obj (op T)) : Type w)) → F.H 0) x : F.H 0) :
      G.H 0)
    ((AddEquiv.symm (equiv₀ G hT) : (a : (↑(G.obj.obj (op T)) : Type w)) → G.H 0)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (X := F.obj (P := Presheaf.IsSheaf J).obj (op T)) (f.hom.app (op T)) :
            (a : (↑(F.obj.obj (op T)) : Type w)) → (↑(G.obj.obj (op T)) : Type w))
          x) :
      G.H 0)
have a : Eq.{w + 1} (α := (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
  ((equiv₀ G hT : (a : G.H 0) → (↑(G.obj.obj (op T)) : Type w))
      ((map f 0 : (a : F.H 0) → G.H 0)
        ((AddEquiv.symm (equiv₀ F hT) : (a : (↑(F.obj.obj (op T)) : Type w)) → F.H 0) x : F.H 0)) :
    (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
  ((equiv₀ G hT : (a : G.H 0) → (↑(G.obj.obj (op T)) : Type w))
      ((AddEquiv.symm (equiv₀ G hT) : (a : (↑(G.obj.obj (op T)) : Type w)) → G.H 0)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (X := F.obj (P := Presheaf.IsSheaf J).obj (op T)) (f.hom.app (op T)) :
            (a : (↑(F.obj.obj (op T)) : Type w)) → (↑(G.obj.obj (op T)) : Type w))
          x)) :
    (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
Tactic: apply (H.equiv₀ G hT).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
h : Limits.IsZero F
n : ℕ
⊢ Subsingleton.{w' + 1} (↑((functorH J n).obj F) : Type w')
have h₁ : Limits.IsZero ((functorH J n).obj F)
Tactic: apply AddCommGrpCat.subsingleton_of_isZero
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
x : (↑(F.H' n S.X₂ ⊞ F.H' n S.X₃) : Type w)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have obtain : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨⟨x₂, x₃⟩, rfl⟩ :=
    (AddCommGrpCat.biprodIsoProd _ _).addCommGroupIsoToAddEquiv.symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
      Iso.hom
        ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) =
    Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝
have hf : ∀ (x : (↑((S.sequence F n₀ n₁ h).obj ⟨0, sorry⟩) : Type w)),
  Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 1 _proof_450✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
              Iso.hom
                ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨0, sorry⟩) : Type w)) →
            (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 1 _proof_450✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 1 _proof_450✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).map' 0 1 homMk₁._proof_4 _proof_450✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨0, sorry⟩) : Type w)) →
            (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 1 _proof_450✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 1 _proof_450✝) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
      Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)) =
    Iso.hom
        ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝
have hf : ∀ (x : (↑((S.sequence F n₀ n₁ h).obj ⟨1, sorry⟩) : Type w)),
  Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, sorry⟩) : Type w)) →
            (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom
                ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).map' 1 2 _proof_246✝ _proof_451✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, sorry⟩) : Type w)) →
            (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)
⊢ Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom
                ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
have hf : Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
  ((AddCommGrpCat.Hom.hom
          (Iso.hom
              ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
            (Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).map' 1 2 _proof_246✝ _proof_451✝) :
        (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, sorry⟩) : Type w)) →
          (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
      x :
    (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
  ((AddCommGrpCat.Hom.hom
          ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
            Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝))) :
        (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, sorry⟩) : Type w)) →
          (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
      x :
    (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 2 _proof_451✝) : Type w))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map
        (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁)
          (S.fromBiprod F n₁))
        (S.toBiprod F n₀) 2 3 ⋯ ≫
      𝟙
        (Precomp.obj
          (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁)
            (S.fromBiprod F n₁))
          (F.H' n₀ S.X₄) 3) =
    𝟙
        (Precomp.obj
          (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁)
            (S.fromBiprod F n₁))
          (F.H' n₀ S.X₄) 2) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)
have rw : Precomp.map
    (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁))
    (S.toBiprod F n₀) 2 3 sorry =
  (Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).map (homOfLE sorry)
Tactic: rw [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
      Iso.hom
        ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) =
    Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝
have hf : ∀ (x : (↑((S.sequence F n₀ n₁ h).obj ⟨3, sorry⟩) : Type w)),
  Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 4 _proof_453✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
              Iso.hom
                ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨3, sorry⟩) : Type w)) →
            (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 4 _proof_453✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 4 _proof_453✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).map' 3 4 _proof_364✝ _proof_453✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨3, sorry⟩) : Type w)) →
            (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 4 _proof_453✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 4 _proof_453✝) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
      Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝)) =
    Iso.hom
        ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 4 5 _proof_453✝ _proof_454✝
have hf : ∀ (x : (↑((S.sequence F n₀ n₁ h).obj ⟨4, sorry⟩) : Type w)),
  Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, sorry⟩) : Type w)) →
            (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom
                ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).map' 4 5 _proof_453✝ _proof_454✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, sorry⟩) : Type w)) →
            (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)
⊢ Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom
                ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 4 5 _proof_453✝ _proof_454✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
have hf : Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
  ((AddCommGrpCat.Hom.hom
          (Iso.hom
              ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫
                AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
            (Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).map' 4 5 _proof_453✝ _proof_454✝) :
        (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, sorry⟩) : Type w)) →
          (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
      x :
    (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
  ((AddCommGrpCat.Hom.hom
          ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
            Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝))) :
        (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, sorry⟩) : Type w)) →
          (↑((Ext.contravariantSequence sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
      x :
    (↑((Ext.contravariantSequence (S := S.shortComplex) sorry F n₀ n₁ sorry).obj' 5 _proof_454✝) : Type w))
Tactic: symm