awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (pullback f g))) (β :=
      (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (pullback f g))) → (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings Y
have rw : ∀
  (hf :
    ∀ (x : (fun (X : Type u) ↦ X) (F.obj S)),
      ∃ (i : ι),
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
              (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
          x)
  (Y : C) (g : Y ⟶ S) (P : ι → C) (p₁ : (i : ι) → P i ⟶ Y) (p₂ : (i : ι) → P i ⟶ X i)
  (h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)) (x : (fun (X : Type u) ↦ X) (F.obj Y)),
  ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
      x
Tactic: rw [Precoverage.mem_comap_iff, Presieve.map_ofArrows,
      Types.ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf ⊢
Cleared hypotheses: hf, Y, g, P, p₁, p₂, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (pullback f g))) (β :=
      (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (pullback f g))) → (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf :
  ∀ (x : (fun (X : Type u) ↦ X) (F.obj S)),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
            (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
        x
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
⊢ ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
      x
have obtain : ∀ (i : ι)
  (hi :
    Membership.mem (α := (fun (X : Type u) ↦ X) (F.obj S)) (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj S))
          x :
        (fun (X : Type u) ↦ X) (F.obj S))),
  ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
      x
Tactic: obtain ⟨i, hi⟩ := hf (F.map g x)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (pullback f g))) (β :=
      (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (pullback f g))) → (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf :
  ∀ (x : (fun (X : Type u) ↦ X) (F.obj S)),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
            (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
        x
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi :
  Membership.mem (α := (fun (X : Type u) ↦ X) (F.obj S)) (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj S))
        x :
      (fun (X : Type u) ↦ X) (F.obj S))
⊢ ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
      x
have this : HasPullback g (f i)
Tactic: have : HasPullback g (f i) := (h i).hasPullback
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (pullback f g))) (β :=
      (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (pullback f g))) → (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf :
  ∀ (x : (fun (X : Type u) ↦ X) (F.obj S)),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
            (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
        x
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi :
  Membership.mem (α := (fun (X : Type u) ↦ X) (F.obj S)) (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj S))
        x :
      (fun (X : Type u) ↦ X) (F.obj S))
this : HasPullback g (f i)
⊢ ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
      x
have h₁ : Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
  (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
      (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
  x
Tactic: use i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (pullback f g))) (β :=
      (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (pullback f g))) → (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf :
  ∀ (x : (fun (X : Type u) ↦ X) (F.obj S)),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
            (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
        x
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi :
  Membership.mem (α := (fun (X : Type u) ↦ X) (F.obj S)) (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj S))
        x :
      (fun (X : Type u) ↦ X) (F.obj S))
this : HasPullback g (f i)
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
    x
have this₁ : F.map (p₁ i) =
  CategoryStruct.comp (Y := F.obj (pullback g (f i))) (F.map (Iso.hom sorry.isoPullback))
    (CategoryStruct.comp (Y := pullback (F.map g) (F.map (f i))) (pullbackComparison F g (f i))
      (pullback.fst (F.map g) (F.map (f i))))
Tactic: have : F.map (p₁ i) = F.map ((h i).isoPullback.hom) ≫ pullbackComparison F g (f i) ≫
        pullback.fst _ _ := by simp [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (pullback f g))) (β :=
      (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (pullback f g))) → (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf :
  ∀ (x : (fun (X : Type u) ↦ X) (F.obj S)),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
            (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
        x
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi :
  Membership.mem (α := (fun (X : Type u) ↦ X) (F.obj S)) (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj S))
        x :
      (fun (X : Type u) ↦ X) (F.obj S))
this_1 : HasPullback g (f i)
this :
  F.map (p₁ i) =
    CategoryStruct.comp (Y := F.obj (pullback g (f i))) (F.map (Iso.hom ⋯.isoPullback))
      (CategoryStruct.comp (Y := pullback (F.map g) (F.map (f i))) (pullbackComparison F g (f i))
        (pullback.fst (F.map g) (F.map (f i))))
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
    x
have h₁ : Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
  (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := F.obj (pullback g (f i))) (F.map (Iso.hom sorry.isoPullback))
            (CategoryStruct.comp (Y := pullback (F.map g) (F.map (f i))) (pullbackComparison F g (f i))
              (pullback.fst (F.map g) (F.map (f i)))))) :
      (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
  x
Tactic: rwa [this, types_comp, types_comp, Function.comp_assoc, Set.range_comp,
      Function.Surjective.range_eq <| (H _ _).comp (surjective_of_epi _), Set.image_univ,
      Types.range_pullbackFst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
⊢ Types.jointlySurjectivePrecoverage.IsStableUnderBaseChange
have rw : (Precoverage.comap (𝟭 (Type u_2)) Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange
Tactic: rw [← Precoverage.comap_id Types.jointlySurjectivePrecoverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
⊢ (Precoverage.comap (𝟭 (Type u_2)) Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange
have H : ∀ {X Y S : Type u_2} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
  Function.Surjective (α := (fun (X : Type u_2) ↦ X) (Functor.obj (𝟭 (Type u_2)) (pullback f g))) (β :=
    (fun (X : Type u_2) ↦ X)
      (pullback (X := Functor.obj (𝟭 (Type u_2)) X) (Functor.map (𝟭 (Type u_2)) f) (Functor.map (𝟭 (Type u_2)) g)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison (𝟭 (Type u_2)) f g)) :
      (a : (fun (X : Type u_2) ↦ X) ((𝟭 (Type u_2)).obj (pullback f g))) →
        (fun (X : Type u_2) ↦ X) (pullback ((𝟭 (Type u_2)).map f) ((𝟭 (Type u_2)).map g)))
Tactic: apply isStableUnderBaseChange_comap_jointlySurjectivePrecoverage
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W))
a b : K
f : a ⟶ b
⊢ Functor.map (Functor.obj (Functor.const K) E.pt) f ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i =
    (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F ⋙ Functor.obj (evaluation Cᵒᵖ D) (op i.Y)).map f
have dsimp : 𝟙 E.pt ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i =
  (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F.map f).app (op i.Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W))
a b : K
f : a ⟶ b
⊢ 𝟙 E.pt ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i =
    (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F.map f).app (op i.Y)
have rw : (E.π.app a ≫ (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W)).map f) ≫
    Multiequalizer.ι (W.index (F.obj b)) i =
  E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)
Tactic: rw [Category.id_comp, Category.assoc, ← E.w f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W))
a b : K
f : a ⟶ b
⊢ (E.π.app a ≫ (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W)).map f) ≫
      Multiequalizer.ι (W.index (F.obj b)) i =
    E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)
have dsimp : CategoryStruct.comp (Y := multiequalizer (W.index (F.obj b)))
    (E.π.app a ≫
      Multiequalizer.lift (W.index (F.obj b)) (multiequalizer (W.index (F.obj a)))
        (fun (x : W.Arrow) ↦ Multiequalizer.ι (W.index (F.obj a)) x ≫ (F.map f).app (op x.Y)) sorry)
    (Multiequalizer.ι (W.index (F.obj b)) i) =
  E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)
Tactic: dsimp [diagramNatTrans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
⊢ liftToDiagramLimitObjAux F E ((unop W).shape.fst i) ≫ ((unop W).index (limit F)).fst i =
    liftToDiagramLimitObjAux F E ((unop W).shape.snd i) ≫ ((unop W).index (limit F)).snd i
have dsimp : liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op =
  liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
⊢ liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op =
    liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op
have w : ∀ (k : K),
  (liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op) ≫ NatTrans.app (limit.π F k) (op i.r.Z) =
    (liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op) ≫ NatTrans.app (limit.π F k) (op i.r.Z)
Tactic: ext k
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
k : K
⊢ (liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op) ≫ NatTrans.app (limit.π F k) (op i.r.Z) =
    (liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op) ≫ NatTrans.app (limit.π F k) (op i.r.Z)
have w : E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.fst ≫ (F.obj k).map i.r.g₁.op =
  E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.snd ≫ (F.obj k).map i.r.g₂.op
Tactic: simp only [Category.assoc, NatTrans.naturality, liftToDiagramLimitObjAux_fac_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
k : K
⊢ E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.fst ≫ (F.obj k).map i.r.g₁.op =
    E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.snd ≫ (F.obj k).map i.r.g₂.op
have w : E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) ((unop W).shape.snd i) ≫ ((unop W).index (F.obj k)).snd i =
  E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.snd ≫ (F.obj k).map i.r.g₂.op
Tactic: erw [Multiequalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
k : K
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
        (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F)))
      (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
      (NatTrans.app
          (Cone.π (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F)))
          k :
        Functor.obj.{s, t, s, w}
            (Functor.obj (Functor.const K)
              (Cone.pt (F := F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
                (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F))))
            k ⟶
          (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W).obj k) =
    E.π.app k
have dsimp : CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit F)))
    (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
    (Multiequalizer.lift ((unop W).index (F.obj k)) (multiequalizer ((unop W).index (limit F)))
        (fun (x : (unop W).Arrow) ↦ Multiequalizer.ι ((unop W).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
        sorry :
      multiequalizer ((unop W).index (limit F)) ⟶ multiequalizer ((unop W).index (F.obj k))) =
  E.π.app k
Tactic: dsimp [diagramNatTrans]