awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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 b : 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₃₄)
    (b ≫
      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 b.op)
have 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: obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac
Cleared hypotheses: b, fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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)
⊢ IsLimit (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).pullbackCone
have h : ∀
  (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₃₄) ↦
          (sorry.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)
              sorry :
            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: refine PullbackCone.IsLimit.mk _
      (fun s ↦ F.2.amalgamateOfArrows _ h₂
        (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        (fun W ↦ by
          rintro (_ | _) (_ | _) a b fac
          · obtain rfl : a = b := by simpa only [← cancel_mono sq.f₂₄] using fac
            rfl
          · obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac
            simpa using s.condition =≫ F.obj.map φ.op
          · obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm
            simpa using s.condition.symm =≫ F.obj.map φ.op
          · obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac
            rfl)) (fun _ ↦ ?_) (fun _ ↦ ?_) (fun s m hm₁ hm₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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)
h :
  ∀
    (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
⊢ IsLimit (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).pullbackCone
have h₃ : ∀
  (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₃₄) ↦
          (sorry.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)
              sorry :
            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: refine PullbackCone.IsLimit.mk _
      (fun s ↦ F.2.amalgamateOfArrows _ h₂
        (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        (fun W ↦ by
          rintro (_ | _) (_ | _) a b fac
          · obtain rfl : a = b := by simpa only [← cancel_mono sq.f₂₄] using fac
            rfl
          · obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac
            simpa using s.condition =≫ F.obj.map φ.op
          · obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm
            simpa using s.condition.symm =≫ F.obj.map φ.op
          · obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac
            rfl)) (fun _ ↦ ?_) (fun _ ↦ ?_) (fun s m hm₁ hm₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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
⊢ 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
have 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₃₄) ↦
          (sorry.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)
              sorry :
            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₃₄))))
Tactic: apply F.2.hom_ext_ofArrows _ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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₃₄)))
    (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₃₄))))
have 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)
Tactic: rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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₃₄)))
    (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₃₄))))
have 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)
Tactic: rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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')
⊢ S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)
have have : ∀ (this : IsLimit (S.op.map P).pullbackCone ≃ Function.Bijective (S.op.map P).pullbackCone.toPullbackObj),
  S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)
Tactic: have := (S.toSquare.op.map P).pullbackCone.isLimitEquivBijective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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')
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
h₂ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
⊢ S.toPullbackObj P x = S.toPullbackObj P y
have a : (↑(S.toPullbackObj P x) : P.obj (op S.X₂) × P.obj (op S.X₃)).1 =
  (↑(S.toPullbackObj P y) : P.obj (op S.X₂) × P.obj (op S.X₃)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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')
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
h₂ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
a :
  (↑(S.toPullbackObj P x) : P.obj (op S.X₂) × P.obj (op S.X₃)).1 =
    (↑(S.toPullbackObj P y) : P.obj (op S.X₂) × P.obj (op S.X₃)).1
⊢ S.toPullbackObj P x = S.toPullbackObj P y
have a₁ : (↑(S.toPullbackObj P x) : P.obj (op S.X₂) × P.obj (op S.X₃)).2 =
  (↑(S.toPullbackObj P y) : P.obj (op S.X₂) × P.obj (op S.X₃)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
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
F : Sheaf J A
⊢ S.SheafCondition (F.obj (P := Presheaf.IsSheaf J))
have rw : ∀ (X : Aᵒᵖ), S.SheafCondition (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda X)
Tactic: rw [sheafCondition_iff_comp_coyoneda]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (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
S : J.MayerVietorisSquare
⊢ Mono (X := Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₁ ⋙ AddCommGrpCat.free))
    (CategoryStruct.comp (Y :=
      Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₂ ⋙ AddCommGrpCat.free) ⊞
        Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₃ ⋙ AddCommGrpCat.free))
      (biprod.lift
        (Functor.map (presheafToSheaf J AddCommGrpCat)
          (Functor.whiskerRight (Functor.map yoneda S.f₁₂) AddCommGrpCat.free))
        (-Functor.map (presheafToSheaf J AddCommGrpCat)
            (Functor.whiskerRight (Functor.map yoneda S.f₁₃) AddCommGrpCat.free)))
      biprod.snd)
have simp : Mono (X := Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₁ ⋙ AddCommGrpCat.free))
  (-Functor.map (presheafToSheaf J AddCommGrpCat) (Functor.whiskerRight (Functor.map yoneda S.f₁₃) AddCommGrpCat.free))
Tactic: simp only [biprod.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (hypothesis)
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
S : J.MayerVietorisSquare
⊢ Mono S.shortComplex.f
have this : Mono (S.shortComplex.f ≫ biprod.snd)
Tactic: have : Mono (S.shortComplex.f ≫ biprod.snd) := by
    dsimp
    simp only [biprod.lift_snd]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)
j j' : (Over.{v₁, u₁} (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙
            tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)).obj
        j ⟶
      (Functor.op (Over.forget (unop (op X))) ⋙ G).obj j')
    ((Functor.op (Over.forget (unop (op X))) ⋙
            tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)).map
        φ ≫
      uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)))
    (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
      (Functor.op (Over.forget (unop (op X))) ⋙ G).map φ)
have dsimp : Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op (unop j).left)) M ⟶ G.obj (op (unop j').left))
  ((F.map (Over.Hom.left φ.unop).op ⊗ₘ 𝟙 M) ≫
    uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)))
  (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
    G.map (Over.Hom.left φ.unop).op)
Tactic: dsimp