awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
h : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ Eq (α := pullback p ((E.inter F).toPullback k) ⟶ E.X j.1)
    (pullback.fst p ((E.inter F).toPullback k) ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))
    ((pullback.snd p ((E.inter F).toPullback k) ≫ pullback.fst (E.p₁ k.1 ≫ E.f i.1) (F.p₁ k.2 ≫ F.f i.2)) ≫ E.p₂ k.1)
have this : p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) =
  p ≫
    pullback.snd ((E.inter F).f i) ((E.inter F).f j) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              j)))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              j)))
Tactic: have : p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = p ≫ pullback.snd _ _ ≫ pullback.fst _ _ := by
          simp [p]
-- 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
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
h :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun (x : C) (f : x ⟶ W)
          (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    f
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
hab : a ≫ b = f
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f
have h : (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun (x : C) (f : x ⟶ W)
          (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b) →
  ((E.inter F).sieve₁ p₁ p₂).arrows (a ≫ b)
Tactic: subst hab
Cleared hypotheses: f, h, hab
-- 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
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
h :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun (x : C) (f : x ⟶ W)
          (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows (a ≫ b)
have h : (a ≫ e) ≫ E.p₁ (k, l).1 ≫ E.f i.1 = u ≫ F.p₁ (k, l).2 ≫ F.f i.2
Tactic: refine ⟨(k, l), pullback.lift (a ≫ e) u ?_, ?_, ?_⟩
-- 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
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
h_1 :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun (x : C) (f : x ⟶ W)
          (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
h : (a ≫ e) ≫ E.p₁ (k, l).1 ≫ E.f i.1 = u ≫ F.p₁ (k, l).2 ≫ F.f i.2
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows (a ≫ b)
have h₃ : (a ≫ b) ≫ p₁ = pullback.lift (a ≫ e) u sorry ≫ (E.inter F).p₁ (k, l)
Tactic: refine ⟨(k, l), pullback.lift (a ≫ e) u ?_, ?_, ?_⟩
-- 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
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
h_1 :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun (x : C) (f : x ⟶ W)
          (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
h : (a ≫ e) ≫ E.p₁ (k, l).1 ≫ E.f i.1 = u ≫ F.p₁ (k, l).2 ≫ F.f i.2
h₃ : (a ≫ b) ≫ p₁ = pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₁ (k, l)
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows (a ≫ b)
have h₄ : (a ≫ b) ≫ p₂ = pullback.lift (a ≫ e) u sorry ≫ (E.inter F).p₂ (k, l)
Tactic: refine ⟨(k, l), pullback.lift (a ≫ e) u ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
h :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun (x : C) (f : x ⟶ W)
          (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ (a ≫ e) ≫ E.p₁ (k, l).1 ≫ E.f i.1 = u ≫ F.p₁ (k, l).2 ≫ F.f i.2
have u₃ : a ≫ b ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
Tactic: simp only [Category.assoc] at u₁
Cleared hypotheses: u₁
-- 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_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.219515, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
⊢ Eq (α := d.pt ⟶ (E.multicospanIndex P).right k)
    ((fun (a : E.multicospanShape.L) ↦ d.ι (f.s₀ a) ≫ P.map (f.h₀ a).op) (E.multicospanShape.fst k) ≫
      (E.multicospanIndex P).fst k)
    ((fun (a : E.multicospanShape.L) ↦ d.ι (f.s₀ a) ≫ P.map (f.h₀ a).op) (E.multicospanShape.snd k) ≫
      (E.multicospanIndex P).snd k)
have simp : d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
    P.map (Quiver.Hom.op (f.h₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) ≫
      P.map (E.p₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    P.map (Quiver.Hom.op (f.h₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) ≫
      P.map (E.p₂ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op
Tactic: simp only [multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
      multicospanIndex_fst, assoc, multicospanShape_snd, multicospanIndex_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.219515, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
⊢ d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (Quiver.Hom.op (f.h₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) ≫
        P.map (E.p₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (Quiver.Hom.op (f.h₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) ≫
        P.map (E.p₂ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op
have heq : Eq (α := d.pt ⟶ (F.multicospanIndex P).right (f.s₁' k))
  (d.ι (F.multicospanShape.fst (f.s₁' k)) ≫ (F.multicospanIndex P).fst (f.s₁' k))
  (d.ι (F.multicospanShape.snd (f.s₁' k)) ≫ (F.multicospanIndex P).snd (f.s₁' k))
Tactic: have heq := d.condition (f.s₁' k)
-- 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_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.219515, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
⊢ d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (Quiver.Hom.op (f.h₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) ≫
        P.map (E.p₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (Quiver.Hom.op (f.h₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) ≫
        P.map (E.p₂ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op
have rw : d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
    P.map
      (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    P.map
      (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
Tactic: rw [← Functor.map_comp, ← op_comp, ← Hom.w₁₁, ← Functor.map_comp, ← op_comp, ← Hom.w₁₂]
-- 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_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.219515, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
⊢ d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
have rw : CategoryStruct.comp (Y := P.obj (op (F.X (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))))
    (d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))
    (P.map
      ((F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op)) =
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    P.map
      (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
Tactic: rw [op_comp, Functor.map_comp, reassoc_of% heq, op_comp, Functor.map_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_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.219515, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
rw :
  CategoryStruct.comp (Y := P.obj (op (F.X (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))))
      (d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))
      (P.map
        ((F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
          (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op)) =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
⊢ d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
have rw₁ : d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
    P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
      P.map (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    P.map
      (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
Tactic: rw [op_comp, Functor.map_comp, reassoc_of% heq, op_comp, Functor.map_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_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.219515, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
rw :
  CategoryStruct.comp (Y := P.obj (op (F.X (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))))
      (d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))
      (P.map
        ((F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
          (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op)) =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
rw₁ :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
        P.map (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
⊢ d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
have rw₂ : d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
      P.map (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    P.map
      (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
Tactic: rw [op_comp, Functor.map_comp, reassoc_of% heq, op_comp, Functor.map_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
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (E.multicospanIndex P)
⊢ (id E).mapMultiforkOfIsLimit P hc d = Multifork.IsLimit.lift hc d.ι ⋯
have apply : ∀ (a : E.multicospanShape.L), (id E).mapMultiforkOfIsLimit P hc d ≫ c.ι a = Multifork.IsLimit.lift hc d.ι sorry ≫ c.ι a
Tactic: apply Multifork.IsLimit.hom_ext hc
-- 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 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{u_2, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
g : F.Hom G
t : Multifork (G.multicospanIndex P)
hd : IsLimit d
⊢ (f.comp g).mapMultiforkOfIsLimit P hc t = g.mapMultiforkOfIsLimit P hd t ≫ f.mapMultiforkOfIsLimit P hc d
have apply : ∀ (a : E.multicospanShape.L),
  (f.comp g).mapMultiforkOfIsLimit P hc t ≫ c.ι a =
    (g.mapMultiforkOfIsLimit P hd t ≫ f.mapMultiforkOfIsLimit P hc d) ≫ c.ι a
Tactic: apply Multifork.IsLimit.hom_ext hc
-- 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' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
i'' j'' : E.I₀
hii'' : i' = i''
hjj'' : j' = j''
k : E.I₁ i j
⊢ Eq (α := E.I₁ i'' j'')
    ((congrIndexOneOfEq hii'' hjj'' : (a : E.I₁ i' j') → E.I₁ i'' j'')
        ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k) :
      E.I₁ i'' j'')
    ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i'' j'') k : E.I₁ i'' j'')
have subst : ∀ (hii'' : i = i'') (hjj'' : j = j''),
  Eq (α := E.I₁ i'' j'')
    ((congrIndexOneOfEq hii'' hjj'' : (a : E.I₁ i j) → E.I₁ i'' j'')
        ((congrIndexOneOfEq sorry sorry : (a : E.I₁ i j) → E.I₁ i j) k) :
      E.I₁ i'' j'')
    ((congrIndexOneOfEq sorry sorry : (a : E.I₁ i j) → E.I₁ i'' j'') k : E.I₁ i'' j'')
Tactic: subst hii' hjj'
Cleared hypotheses: i', j', hii', hjj', hii'', hjj''