awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac :
  Eq (α := W ⟶ sq.X₄)
    (a ≫
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
        sq.f₂₄ sq.f₃₄)
    (a ≫
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
        sq.f₂₄ sq.f₃₄)
⊢ Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op W))
    ((fun (j : WalkingPair) ↦
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
              s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd :
            s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ j))))
        WalkingPair.right ≫
      F.obj (P := Presheaf.IsSheaf J).map a.op)
    ((fun (j : WalkingPair) ↦
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
              s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd :
            s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ j))))
        WalkingPair.right ≫
      F.obj (P := Presheaf.IsSheaf J).map a.op)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
⊢ (fun
            (s :
              PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
          (⋯.amalgamateOfArrows
              (fun (k : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                  sq.f₃₄)
              h₂
              (fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
              ⋯ :
            s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
        x ≫
      (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ =
    x.fst

Tactic:
F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.left

Premises used: Quiver.Hom.op, CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.pairFunction, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
⊢ (fun
            (s :
              PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
          (⋯.amalgamateOfArrows
              (fun (k : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                  sq.f₃₄)
              h₂
              (fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
              ⋯ :
            s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
        x ≫
      (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ =
    x.fst

Tactic:
exact F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.left

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
⊢ (fun
            (s :
              PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
          (⋯.amalgamateOfArrows
              (fun (k : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                  sq.f₃₄)
              h₂
              (fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
              ⋯ :
            s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
        x ≫
      (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ =
    x.snd

Tactic:
F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.right

Premises used: Quiver.Hom.op, CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.pairFunction
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
⊢ (fun
            (s :
              PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
          (⋯.amalgamateOfArrows
              (fun (k : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                  sq.f₃₄)
              h₂
              (fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
              ⋯ :
            s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
        x ≫
      (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ =
    x.snd

Tactic:
exact F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.right

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.WalkingPair.right
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
m : s.pt ⟶ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).X₁
hm₁ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ = s.snd
h :
  ∀ (i : WalkingPair),
    Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ i)))
      (m ≫
        F.obj (P := Presheaf.IsSheaf J).map
          (Quiver.Hom.op
            (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) i sq.f₂₄
              sq.f₃₄)))
      (CategoryStruct.comp (Y := F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄))
        ((fun
              (s :
                PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                  (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
            (⋯.amalgamateOfArrows
                (fun (k : WalkingPair) ↦
                  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                    sq.f₃₄)
                h₂
                (fun (j : WalkingPair) ↦
                  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                    s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
                ⋯ :
              s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
          s)
        (F.obj (P := Presheaf.IsSheaf J).map
          (Quiver.Hom.op
            (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) i sq.f₂₄
              sq.f₃₄))))
⊢ m =
    (fun
          (s :
            PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
              (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
        (⋯.amalgamateOfArrows
            (fun (k : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                sq.f₃₄)
            h₂
            (fun (j : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
            ⋯ :
          s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
      s

Tactic:
apply F.2.hom_ext_ofArrows _ h₂

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.IsSheaf.hom_ext_ofArrows
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
m : s.pt ⟶ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).X₁
hm₁ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ = s.snd
h :
  Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ WalkingPair.left)))
    (m ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left
            sq.f₂₄ sq.f₃₄)))
    (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) WalkingPair.left s.fst s.snd)
⊢ Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ WalkingPair.left)))
    (m ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left
            sq.f₂₄ sq.f₃₄)))
    (CategoryStruct.comp (Y := F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄))
      ((fun
            (s :
              PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
          (⋯.amalgamateOfArrows
              (fun (k : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                  sq.f₃₄)
              h₂
              (fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
              ⋯ :
            s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
        s)
      (F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left
            sq.f₂₄ sq.f₃₄))))

Tactic:
rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.left]

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
m : s.pt ⟶ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).X₁
hm₁ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ = s.snd
⊢ Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ WalkingPair.left)))
    (m ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left
            sq.f₂₄ sq.f₃₄)))
    (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) WalkingPair.left s.fst s.snd)

Tactic:
hm₁

Premises used: Quiver.Hom.op, CategoryTheory.Limits.pairFunction
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
m : s.pt ⟶ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).X₁
hm₁ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ = s.snd
⊢ Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ WalkingPair.left)))
    (m ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left
            sq.f₂₄ sq.f₃₄)))
    (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) WalkingPair.left s.fst s.snd)

Tactic:
exact hm₁
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
m : s.pt ⟶ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).X₁
hm₁ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ = s.snd
h :
  Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ WalkingPair.right)))
    (m ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
            sq.f₂₄ sq.f₃₄)))
    (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) WalkingPair.right s.fst s.snd)
⊢ Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ WalkingPair.right)))
    (m ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
            sq.f₂₄ sq.f₃₄)))
    (CategoryStruct.comp (Y := F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄))
      ((fun
            (s :
              PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
          (⋯.amalgamateOfArrows
              (fun (k : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                  sq.f₃₄)
              h₂
              (fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
              ⋯ :
            s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
        s)
      (F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
            sq.f₂₄ sq.f₃₄))))

Tactic:
rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.right]

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.WalkingPair.right
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
m : s.pt ⟶ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).X₁
hm₁ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ = s.snd
⊢ Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ WalkingPair.right)))
    (m ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
            sq.f₂₄ sq.f₃₄)))
    (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) WalkingPair.right s.fst s.snd)

Tactic:
hm₂

Premises used: Quiver.Hom.op, CategoryTheory.Limits.pairFunction
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
m : s.pt ⟶ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).X₁
hm₁ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ = s.snd
⊢ Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ WalkingPair.right)))
    (m ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op
          (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
            sq.f₂₄ sq.f₃₄)))
    (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) WalkingPair.right s.fst s.snd)

Tactic:
exact hm₂
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
inst_2 : HasWeakSheafify J AddCommGrpCat
⊢ (S.map
      (yoneda ⋙
        Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type v) AddCommGrpCat) AddCommGrpCat.free ⋙
          presheafToSheaf J AddCommGrpCat)).IsPushout

Tactic:
(S.isPushout.map (Sheaf.composeAndSheafify J AddCommGrpCat.free)).of_iso
    ((Square.mapFunctor.mapIso
      (presheafToSheafCompComposeAndSheafifyIso J AddCommGrpCat.free)).app
        (S.map yoneda))

Premises used: AddCommGrpCat.free, CategoryTheory.Square.IsPushout.of_iso, CategoryTheory.presheafToSheafCompComposeAndSheafifyIso, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout, CategoryTheory.Square.mapFunctor, CategoryTheory.yoneda, CategoryTheory.Square.map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare, CategoryTheory.Sheaf.composeAndSheafify, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Square.IsPushout.map
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst_2 : Category.{v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ S.SheafCondition P ↔ ∀ (X : Aᵒᵖ), S.SheafCondition (P ⋙ Functor.obj coyoneda X)

Tactic:
Square.isPullback_iff_map_coyoneda_isPullback (S.op.map P)

Premises used: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition, CategoryTheory.Square.op, Quiver.Hom.op, CategoryTheory.Square.map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare, CategoryTheory.Square.isPullback_iff_map_coyoneda_isPullback
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
have :
  ∀ (this : IsLimit (S.op.map P).pullbackCone ≃ Function.Bijective (S.op.map P).pullbackCone.toPullbackObj),
    S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)
⊢ S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

Tactic:
have := (S.toSquare.op.map P).pullbackCone.isLimitEquivBijective