awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x : Sheaf (J.over T) A
x_1 : (Over.{v, u} X)ᵒᵖ
⊢ Eq (α :=
    x.obj (P := Presheaf.IsSheaf (J.over T)).obj (Opposite.op ((Over.map (f ≫ g ≫ h)).obj (Opposite.unop x_1))) ⟶
      x.obj (P := Presheaf.IsSheaf (J.over T)).obj (Opposite.op ((Over.map ((f ≫ g) ≫ h)).obj (Opposite.unop x_1))))
    (x.obj (P := Presheaf.IsSheaf (J.over T)).map
      (Quiver.Hom.op
        ((Over.mapComp (f ≫ g) h).hom.app (Opposite.unop x_1) ≫
          (Over.map h).map ((Over.mapComp f g).hom.app (Opposite.unop x_1)) ≫
            (Over.mapComp g h).inv.app ((Over.map f).obj (Opposite.unop x_1)) ≫
              (Over.mapComp f (g ≫ h)).inv.app (Opposite.unop x_1))))
    (x.obj (P := Presheaf.IsSheaf (J.over T)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x_1))))
have w : Eq (α := (Over.map ((f ≫ g) ≫ h)).obj (Opposite.unop x_1) ⟶ (Over.map (f ≫ g ≫ h)).obj (Opposite.unop x_1))
  ((Over.mapComp (f ≫ g) h).hom.app (Opposite.unop x_1) ≫
    (Over.map h).map ((Over.mapComp f g).hom.app (Opposite.unop x_1)) ≫
      (Over.mapComp g h).inv.app ((Over.map f).obj (Opposite.unop x_1)) ≫
        (Over.mapComp f (g ≫ h)).inv.app (Opposite.unop x_1))
  ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) sorry).inv.app (Opposite.unop x_1))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
⊢ K.toGrothendieck.over X = (Precoverage.comap (Over.forget X) K).toGrothendieck
have refine_1 : K.toGrothendieck.over X ≤ (Precoverage.comap (Over.forget X) K).toGrothendieck
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
refine_1 : K.toGrothendieck.over X ≤ (Precoverage.comap (Over.forget X) K).toGrothendieck
⊢ K.toGrothendieck.over X = (Precoverage.comap (Over.forget X) K).toGrothendieck
have refine_2 : (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }
hR :
  Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    ((K.toGrothendieck.over X : (a : Over X) → Set (Sieve a)) { left := Y, right := right, hom := s }) R
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Y, right := right, hom := s })
    R
have refine_1 : ∀ (R : Sieve.{v, u} Y)
  (hR :
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
      ((K.toGrothendieck.over X : (a : Over X) → Set (Sieve a)) { left := Y, right := right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
              Sieve { left := Y, right := right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })),
  Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Y, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
            Sieve { left := Y, right := right, hom := s })
        R :
      Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
Tactic: obtain ⟨(R : Sieve Y), rfl⟩ := (Sieve.overEquiv _).symm.surjective R
Cleared hypotheses: R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve.{v, u} Y
hR :
  Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    ((K.toGrothendieck.over X : (a : Over X) → Set (Sieve a)) { left := Y, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
            Sieve { left := Y, right := right, hom := s })
        R :
      Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
⊢ Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Y, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
            Sieve { left := Y, right := right, hom := s })
        R :
      Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
have hR₁ : K.toCoverage.Saturate Y R
Tactic: simp +instances only [GrothendieckTopology.mem_over_iff, Equiv.apply_symm_apply,
      ← Precoverage.toGrothendieck_toCoverage, Coverage.mem_toGrothendieck,
      Over.left] at hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve.{v, u} Y
Z : C
S : Presieve.{v, u} Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Z, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Z, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Z, right := right, hom := s })) →
            Sieve { left := Z, right := right, hom := s })
        (Sieve.generate S) :
      Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s })
have refine_1 : Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
  (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
    { left := Z, right := right, hom := s })
  (Sieve.generate (Presieve.functorPullback (Over.forget X) S))
Tactic: rw [Sieve.overEquiv_symm_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve.{v, u} Y
X_1 : C
s : X_1 ⟶ X
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := X_1, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := X_1, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := X_1, right := right, hom := s }) :
        (a : Sieve (Over.left { left := X_1, right := right, hom := s })) →
          Sieve { left := X_1, right := right, hom := s })
      ⊤)
have refine_1 : Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := X_1, right := right, hom := s }))
  (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
    { left := X_1, right := right, hom := s })
  ⊤
Tactic: rw [Sieve.overEquiv_symm_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y_1 : C
R_1 : Sieve.{v, u} Y_1
Y : C
R S : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_2 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over.{v, u} X
ih :
  ∀ (s : Y ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Y, right := Z.right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
              Sieve { left := Y, right := Z.right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s })
ih' :
  ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_2 ⟶ X),
        Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }) (γ :=
          Set (Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }))
          (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
            { left := Y_2, right := Z.right, hom := s })
          ((Equiv.symm (Sieve.overEquiv { left := Y_2, right := Z.right, hom := s }) :
                (a : Sieve (Over.left { left := Y_2, right := Z.right, hom := s })) →
                  Sieve { left := Y_2, right := Z.right, hom := s })
              (Sieve.pullback f S) :
            Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s })
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg :
  Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
        (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
          Sieve { left := Y, right := Z.right, hom := s })
      R)
    g
⊢ Sieve.pullback g
      ((Equiv.symm
            (Sieve.overEquiv
              { left := Y, right := Z.right, hom := s : Comma.{v, 0, v, u, 0, u} (𝟭 C) (Functor.fromPUnit X) }) :
          (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
            Sieve { left := Y, right := Z.right, hom := s })
        S) ∈
    ((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a)) Z
have refine_1 : Membership.mem (α := Sieve Z) (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a)) Z)
  (((Sieve.overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) (Sieve.pullback (Over.Hom.left g) S) : Sieve Z)
Tactic: rw [← Sieve.overEquiv_symm_pullback]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
⊢ Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Y, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
            Sieve { left := Y, right := right, hom := s })
        R :
      Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
have refine_1 : ∀ (Z : C) (S : Presieve.{v, u} Z) (hS : S ∈ K.toCoverage.coverings Z) (s : Z ⟶ X),
  Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Z, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Z, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Z, right := right, hom := s })) →
            Sieve { left := Z, right := right, hom := s })
        (Sieve.generate S) :
      Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s })
Tactic: induction hR with
    | of Z S hS =>
      rw [Sieve.overEquiv_symm_generate]
      exact .of _ _ (by simpa)
    | top =>
      rw [Sieve.overEquiv_symm_top]
      simp
    | transitive Y R S hR H ih ih' =>
      refine GrothendieckTopology.transitive _ (ih s) _ fun Z g hg ↦ ?_
      obtain rfl : right = Z.right := Subsingleton.elim _ _
      rw [← Sieve.overEquiv_symm_pullback]
      exact ih' hg Z.hom
Cleared hypotheses: s, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
refine_1 :
  ∀ (Z : C) (S : Presieve.{v, u} Z) (hS : S ∈ K.toCoverage.coverings Z) (s : Z ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Z, right := right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Z, right := right, hom := s }) :
            (a : Sieve (Over.left { left := Z, right := right, hom := s })) →
              Sieve { left := Z, right := right, hom := s })
          (Sieve.generate S) :
        Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s })
⊢ Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Y, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
            Sieve { left := Y, right := right, hom := s })
        R :
      Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
have refine_1₁ : ∀ (X_1 : C) (s : X_1 ⟶ X),
  Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := X_1, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := X_1, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := X_1, right := right, hom := s }) :
        (a : Sieve (Over.left { left := X_1, right := right, hom := s })) →
          Sieve { left := X_1, right := right, hom := s })
      ⊤)
Tactic: induction hR with
    | of Z S hS =>
      rw [Sieve.overEquiv_symm_generate]
      exact .of _ _ (by simpa)
    | top =>
      rw [Sieve.overEquiv_symm_top]
      simp
    | transitive Y R S hR H ih ih' =>
      refine GrothendieckTopology.transitive _ (ih s) _ fun Z g hg ↦ ?_
      obtain rfl : right = Z.right := Subsingleton.elim _ _
      rw [← Sieve.overEquiv_symm_pullback]
      exact ih' hg Z.hom
Cleared hypotheses: s, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
⊢ (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X
have refine_2 : Precoverage.comap (Over.forget X) K ≤ (K.toGrothendieck.over X).toPrecoverage
Tactic: rw [Precoverage.toGrothendieck_le_iff_le_toPrecoverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
Y : Over.{v, u} X
R : Presieve Y
hR : R ∈ (Precoverage.comap (Over.forget X) K).coverings Y
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y
have hR₁ : Membership.mem (γ := Set (Presieve.{v, u} (Functor.obj (Over.forget X) Y)))
  (K.coverings (Functor.obj (Over.forget X) Y)) (Presieve.map (Over.forget X) R)
Tactic: rw [Precoverage.mem_comap_iff] at hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
Y : Over.{v, u} X
R : Presieve Y
hR :
  Membership.mem (γ := Set (Presieve.{v, u} (Functor.obj (Over.forget X) Y)))
    (K.coverings (Functor.obj (Over.forget X) Y)) (Presieve.map (Over.forget X) R)
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y
have refine_2 : Membership.mem (α := Sieve.{v, u} Y.left) (γ := Set (Sieve.{v, u} Y.left))
  ((K.toGrothendieck : (a : C) → Set (Sieve a)) Y.left)
  (Sieve.generate (Presieve.map (Over.forget X) R) : Sieve.{v, u} (Functor.obj (Over.forget X) Y))
Tactic: rw [GrothendieckTopology.mem_toPrecoverage_iff, GrothendieckTopology.mem_over_iff,
      Sieve.overEquiv, Equiv.coe_fn_mk, ← Sieve.generate_map_eq_functorPushforward]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
X Y : C
f_1 : X ⟶ Y
S T : (J.Cover Y)ᵒᵖ
f : S ⟶ T
I : (unop ((J.pullback f_1).op.obj T)).shape.L
⊢ CategoryStruct.comp (Y := multiequalizer ((unop ((J.pullback f_1).op.obj T)).index P))
      ((J.diagram P Y).map f ≫
        Multiequalizer.lift ((unop ((J.pullback f_1).op.obj T)).index P) ((J.diagram P Y).obj T)
          (fun (I : (unop ((J.pullback f_1).op.obj T)).shape.L) ↦
            Multiequalizer.ι ((unop T).index P) (Cover.Arrow.base I))
          ⋯)
      (Multiequalizer.ι ((unop ((J.pullback f_1).op.obj T)).index P) I) =
    (Multiequalizer.lift ((unop ((J.pullback f_1).op.obj S)).index P) ((J.diagram P Y).obj S)
          (fun (I : (unop ((J.pullback f_1).op.obj S)).shape.L) ↦
            Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I))
          ⋯ ≫
        ((J.pullback f_1).op ⋙ J.diagram P X).map f) ≫
      Multiequalizer.ι ((unop ((J.pullback f_1).op.obj T)).index P) I
have simp : Eq (α := multiequalizer ((unop S).index P) ⟶ P.obj (op I.Y))
  (Multiequalizer.ι ((unop S).index P) ((Cover.Arrow.base I).map f.unop) :
    multiequalizer ((unop S).index P) ⟶ ((unop S).index P).left ((Cover.Arrow.base I).map f.unop))
  (Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I ((J.pullback f_1).map f.unop)).base)
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P_1 P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ Eq (α := (J.diagram P X).obj W ⟶ ((unop W).index Q).right i)
    ((Multiequalizer.ι ((unop W).index P) ((unop W).shape.fst i) ≫ η.app (op ((unop W).shape.fst i).Y)) ≫
      ((unop W).index Q).fst i)
    ((Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ η.app (op ((unop W).shape.snd i).Y)) ≫
      ((unop W).index Q).snd i)
have erw : Eq (α := (J.diagram P X).obj W ⟶ ((unop W).index Q).right i)
  (Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ ((unop W).index P).snd i ≫ η.app (op i.r.Z))
  (Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ P.map i.r.g₂.op ≫ η.app (op i.r.Z))
Tactic: erw [Category.assoc, Category.assoc, ← η.naturality, ← η.naturality,
        Multiequalizer.condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
⊢ J.diagramNatTrans (𝟙 P) X = 𝟙 (J.diagram P X)
have w : ∀ (x : (J.Cover X)ᵒᵖ), NatTrans.app (J.diagramNatTrans (𝟙 P) X) x = NatTrans.app (𝟙 (J.diagram P X)) x
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
x : (J.Cover X)ᵒᵖ
⊢ NatTrans.app (J.diagramNatTrans (𝟙 P) X) x = NatTrans.app (𝟙 (J.diagram P X)) x
have w : ∀ (i : (unop x).shape.L),
  NatTrans.app (J.diagramNatTrans (𝟙 P) X) x ≫ Multiequalizer.ι ((unop x).index P) i =
    NatTrans.app (𝟙 (J.diagram P X)) x ≫ Multiequalizer.ι ((unop x).index P) i
Tactic: refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : Preadditive.{w', w} D
X : C
P Q : Functor.{v, w', u, w} Cᵒᵖ D
⊢ Eq (α := J.diagram P X ⟶ J.diagram Q X) (J.diagramNatTrans 0 X) 0
have w : ∀ (x : (J.Cover X)ᵒᵖ),
  Eq.{w' + 1} (α := (J.diagram P X).obj x ⟶ (J.diagram Q X).obj x) (NatTrans.app (J.diagramNatTrans 0 X) x)
    (NatTrans.app 0 x)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : Preadditive.{w', w} D
X : C
P Q : Functor.{v, w', u, w} Cᵒᵖ D
x : (J.Cover X)ᵒᵖ
⊢ Eq.{w' + 1} (α := (J.diagram P X).obj x ⟶ (J.diagram Q X).obj x) (NatTrans.app (J.diagramNatTrans 0 X) x)
    (NatTrans.app 0 x)
have w : ∀ (i : (unop x).shape.L),
  Eq (α := (J.diagram P X).obj x ⟶ ((unop x).index Q).left i)
    (NatTrans.app (J.diagramNatTrans 0 X) x ≫ Multiequalizer.ι ((unop x).index Q) i)
    (CategoryStruct.comp (Y := multiequalizer ((unop x).index Q))
      (NatTrans.app 0 x : (J.diagram P X).obj x ⟶ (J.diagram Q X).obj x) (Multiequalizer.ι ((unop x).index Q) i))
Tactic: refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
⊢ Eq (α := J.diagram P X ⟶ J.diagram R X) (J.diagramNatTrans (η ≫ γ) X) (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X)
have w : ∀ (x : (J.Cover X)ᵒᵖ),
  Eq (α := (J.diagram P X).obj x ⟶ (J.diagram R X).obj x) (NatTrans.app (J.diagramNatTrans (η ≫ γ) X) x)
    (NatTrans.app (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X) x)
Tactic: ext : 2