awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
inst_2 : H.IsGenerating
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
m : F.pt ⟶ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).pt
hm :
  ∀ (i : (Cover.shape (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)).L),
    m ≫ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).ι i =
      F.ι i
⊢ m =
    (fun
          (F :
            Multifork
              (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)) ↦
        lift (H := H) hP hE le F)
      F
have apply : ∀ ⦃Y : C⦄ (f : Y ⟶ X),
  S.arrows f →
    m ≫ P.map f.op =
      (fun
              (F :
                Multifork
                  (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S sorry)
                    P)) ↦
            lift (H := H) hP hE le F)
          F ≫
        P.map f.op
Tactic: apply hom_ext H P hP S (J.superset_covering le E.mem₀)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
inst_2 : H.IsGenerating
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
m : F.pt ⟶ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).pt
hm :
  ∀ (i : (Cover.shape (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)).L),
    m ≫ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).ι i =
      F.ι i
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ m ≫ P.map f.op =
    (fun
            (F :
              Multifork
                (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)
                  P)) ↦
          lift (H := H) hP hE le F)
        F ≫
      P.map f.op
have rw : m ≫ P.map f.op = F.ι { Y := Y, f := f, hf := hf }
Tactic: rw [fac _ _ _ _ _ hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
⊢ Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
have mp : Presheaf.IsSheaf J P → ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
mp : Presheaf.IsSheaf J P → ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
⊢ Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
have mpr : (∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
⊢ Presheaf.IsSheaf J P
have mpr : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
Tactic: rw [Presheaf.isSheaf_iff_multifork]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Nonempty
    (IsLimit
      (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS) P))
have mpr : ∀ (E : OneHypercover.{w, v, u} J X) (hE : H E) (le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S),
  Nonempty
    (IsLimit
      (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS) P))
Tactic: obtain ⟨E, hE, le⟩ := H.exists_oneHypercover S hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) = E.sieve₁ (f ≫ p₁) (f ≫ p₂)
have refine_1 : Sieve.pullback f (E.sieve₁ p₁ p₂) ≤ E.sieve₁ (f ≫ p₁) (f ≫ p₂)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
refine_1 : Sieve.pullback f (E.sieve₁ p₁ p₂) ≤ E.sieve₁ (f ≫ p₁) (f ≫ p₂)
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) = E.sieve₁ (f ≫ p₁) (f ≫ p₂)
have refine_2 : E.sieve₁ (f ≫ p₁) (f ≫ p₂) ≤ Sieve.pullback f (E.sieve₁ p₁ p₂)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
g : Z ⟶ T
⊢ (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows g → (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows g
have refine_1 : ∀ (k : E.I₁ i₁ i₂) (u : Z ⟶ E.Y k) (hu₁ : (g ≫ f) ≫ p₁ = u ≫ E.p₁ k) (hu₂ : (g ≫ f) ≫ p₂ = u ≫ E.p₂ k),
  (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows g
Tactic: ⟨k, u, hu₁, hu₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
g : Z ⟶ T
⊢ (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows g → (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows g
have refine_2 : ∀ (k : E.I₁ i₁ i₂) (u : Z ⟶ E.Y k) (hu₁ : g ≫ f ≫ p₁ = u ≫ E.p₁ k) (hu₂ : g ≫ f ≫ p₂ = u ≫ E.p₂ k),
  (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows g
Tactic: ⟨k, u, hu₁, hu₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
k : E.I₁ i₁ i₂
⊢ CategoryStruct.comp (Y := pullback (E.f i₁) (E.f i₂)) (E.toPullback k) (pullback.fst (E.f i₁) (E.f i₂)) = E.p₁ k
have rw : E.p₁ k = E.p₁ k
Tactic: rw [pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
k : E.I₁ i₁ i₂
⊢ CategoryStruct.comp (Y := pullback (E.f i₁) (E.f i₂)) (E.toPullback k) (pullback.snd (E.f i₁) (E.f i₂)) = E.p₂ k
have rw : E.p₂ k = E.p₂ k
Tactic: rw [pullback.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ E.sieve₁ p₁ p₂ = Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)
have h : ∀ ⦃Z : C⦄ (g : Z ⟶ W),
  (E.sieve₁ p₁ p₂).arrows g ↔
    (Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g
Tactic: ext Z g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
⊢ (E.sieve₁ p₁ p₂).arrows g ↔
    (Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g
have h : (E.sieve₁ p₁ p₂).arrows g →
  (Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
h :
  (E.sieve₁ p₁ p₂).arrows g →
    (Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g
⊢ (E.sieve₁ p₁ p₂).arrows g ↔
    (Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g
have h₁ : (Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g →
  (E.sieve₁ p₁ p₂).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
⊢ Eq (α := Sieve.{v, u} (pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂)
    (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)))
have rw : Sieve.pullback (𝟙 (pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂) =
  Sieve.pullback (X := pullback (E.f i₁) (E.f i₂))
    (pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) sorry) (E.sieve₁' i₁ i₂)
Tactic: rw [← Sieve.pullback_id (S := E.sieve₁' i₁ i₂),
    sieve₁_eq_pullback_sieve₁' _ _ _ pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
⊢ Sieve.pullback (𝟙 (pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂) =
    Sieve.pullback (X := pullback (E.f i₁) (E.f i₂))
      (pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ⋯) (E.sieve₁' i₁ i₂)
have e_h : 𝟙 (pullback (E.f i₁) (E.f i₂)) = pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
i₁ i₂ : E.I₀
j : E.I₁ i₁ i₂
⊢ Eq (α :=
    F.obj (Opposite.op S) ⟶
      (E.multicospanIndex F).right (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i₀ : E.multicospanShape.L) ↦ F.map (E.f i₀).op)
        (E.multicospanShape.fst (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i₁, i₂) j)) ≫
      (E.multicospanIndex F).fst (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i₀ : E.multicospanShape.L) ↦ F.map (E.f i₀).op)
        (E.multicospanShape.snd (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i₁, i₂) j)) ≫
      (E.multicospanIndex F).snd (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i₁, i₂) j))
have dsimp : F.map (E.f i₁).op ≫ F.map (E.p₁ j).op = F.map (E.f i₂).op ≫ F.map (E.p₂ j).op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ F.map (Cofan.IsColimit.desc hc E.f).op ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) =
    F.map (Cofan.IsColimit.desc hc E.f).op ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
have simp_rw : F.map
    ((Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
          E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
        Cofan.IsColimit.desc hc E.f).op =
  F.map
    ((Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
          E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
        Cofan.IsColimit.desc hc E.f).op
Tactic: simp_rw [← Functor.map_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ F.map
      ((Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
          Cofan.IsColimit.desc hc E.f).op =
    F.map
      ((Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
          Cofan.IsColimit.desc hc E.f).op
have e_a : (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
      E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
        c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
    Cofan.IsColimit.desc hc E.f =
  (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
      E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
        c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    Cofan.IsColimit.desc hc E.f
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ IsLimit (E.multifork F) ≃ IsLimit (E.forkOfIsColimit hc hd F)
have refine : IsLimit (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≃
  IsLimit (E.forkOfIsColimit hc hd F)
Tactic: refine (IsLimit.ofConeEquiv <|
    (E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').symm.trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ IsLimit (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≃
    IsLimit (E.forkOfIsColimit hc hd F)
have refine_1 : Iso.hom (Iso.refl c'.pt) ≫
    F.map
      (Quiver.Hom.op
        (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
          E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) =
  (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)
Tactic: refine Fork.isLimitEquivOfIsos _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
refine_1 :
  Iso.hom (Iso.refl c'.pt) ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)
⊢ IsLimit (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≃
    IsLimit (E.forkOfIsColimit hc hd F)
have refine_2 : Iso.hom (Iso.refl c'.pt) ≫
    F.map
      (Quiver.Hom.op
        (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
          E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) =
  (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)
Tactic: refine Fork.isLimitEquivOfIsos _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
refine_1 :
  Iso.hom (Iso.refl c'.pt) ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)
refine_2 :
  Iso.hom (Iso.refl c'.pt) ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)
⊢ IsLimit (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≃
    IsLimit (E.forkOfIsColimit hc hd F)
have refine_3 : Iso.hom (Iso.refl (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)).pt) ≫
    (E.forkOfIsColimit hc hd F).ι =
  Fork.ι (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≫
    Iso.hom (Iso.refl c'.pt)
Tactic: refine Fork.isLimitEquivOfIsos _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_