awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H₁ :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
R : Sieve.{v, u} X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ {Y_2 : C} (f : Y_2 ⟶ Y), ∃ (Z : C) (g : Z ⟶ Y_2), S.arrows (g ≫ f)} (Sieve.pullback f R)
Y : C
f : Y ⟶ X
⊢ ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)
have rcases : ∀ (Z : C) (g : Z ⟶ Y) (H₃ : S.arrows (g ≫ f)), ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)
Tactic: rcases H₁ f with ⟨Z, g, H₃⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H₁ :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
R : Sieve.{v, u} X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ {Y_2 : C} (f : Y_2 ⟶ Y), ∃ (Z : C) (g : Z ⟶ Y_2), S.arrows (g ≫ f)} (Sieve.pullback f R)
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
⊢ ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)
have rcases : ∀ (W : C) (h : W ⟶ Z) (H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)), ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)
Tactic: rcases H₂ H₃ (𝟙 Z) with ⟨W, h, H₄⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
hro : RightOreCondition.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y), S.arrows f}
    (Sieve.pullback h S)
have rcases : ∀ (W : C) (g : W ⟶ Y) (k : W ⟶ Z) (comm : g ≫ h = k ≫ f),
  Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y), S.arrows f}
    (Sieve.pullback h S)
Tactic: rcases hro h f with ⟨W, g, k, comm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
hro : RightOreCondition.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y), S.arrows f}
    (Sieve.pullback h S)
have refine : (Sieve.pullback h S).arrows g
Tactic: refine ⟨_, g, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
hro : RightOreCondition.{v, u} C
X : C
S : Sieve.{v, u} X
Y : C
f : Y ⟶ X
hf : S.arrows f
R : Sieve.{v, u} X
h :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y), S.arrows f}
        (Sieve.pullback f R)
⊢ Membership.mem (γ := Set (Sieve.{v, u} X)) {S : Sieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X), S.arrows f} R
have rcases : ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g),
  Membership.mem (γ := Set (Sieve.{v, u} X)) {S : Sieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X), S.arrows f} R
Tactic: rcases h hf with ⟨Z, g, hg⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (↑S : Sieve X).arrows e2
left :
  Sieve.arrows
    ((fun (Y : C) (f : Y ⟶ X) (hf : (↑S : Sieve X).arrows f) ↦
        ((↑(T { Y := Y, f := f, hf := hf : S.Arrow }) : Sieve.{v, u} { Y := Y, f := f, hf := hf : S.Arrow }.Y) :
          Sieve.{v, u} { Y := Y, f := f, hf := hf : S.Arrow }.Y))
      Z e2 h1)
    e1
h3 : e1 ≫ e2 = f
⊢ (↑S : Sieve X).arrows f
have rw : (↑S : Sieve X).arrows (e1 ≫ e2)
Tactic: rw [← h3]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S_1 R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
S : J.Cover X
P : Functor.{v, v₁, u, u₁} Cᵒᵖ D
I : S.shape.R
⊢ Eq (α := P.obj (Opposite.op X) ⟶ (S.index P).right I)
    ((fun (I : S.shape.L) ↦ P.map I.f.op) (S.shape.fst I) ≫ (S.index P).fst I)
    ((fun (I : S.shape.L) ↦ P.map I.f.op) (S.shape.snd I) ≫ (S.index P).snd I)
have dsimp : P.map I.fst.f.op ≫ P.map I.r.g₁.op = P.map I.snd.f.op ≫ P.map I.r.g₂.op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S_1 R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
S : J.Cover X
P : Functor.{v, v₁, u, u₁} Cᵒᵖ D
inst_2 : Limits.HasMultiequalizer (S.index P)
I : S.shape.R
⊢ Eq (α := P.obj (Opposite.op X) ⟶ (S.index P).right I)
    ((fun (I : S.shape.L) ↦ P.map I.f.op) (S.shape.fst I) ≫ (S.index P).fst I)
    ((fun (I : S.shape.L) ↦ P.map I.f.op) (S.shape.snd I) ≫ (S.index P).snd I)
have dsimp : P.map I.fst.f.op ≫ P.map I.r.g₁.op = P.map I.snd.f.op ≫ P.map I.r.g₂.op
Tactic: dsimp only [shape, index, Relation.fst, Relation.snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
E F : PreOneHypercover.{w, v, u} S
f g : E.Hom F
H : Homotopy f g
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
⊢ f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d
have refine : ∀ (a : E.multicospanShape.L), f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = g.mapMultiforkOfIsLimit P hc d ≫ c.ι a
Tactic: refine Multifork.IsLimit.hom_ext hc fun a ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
E F : PreOneHypercover.{w, v, u} S
f g : E.Hom F
H : Homotopy f g
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
a : E.multicospanShape.L
⊢ f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = g.mapMultiforkOfIsLimit P hc d ≫ c.ι a
have heq : Eq (α :=
  d.pt ⟶ (F.multicospanIndex P).right (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) (f.s₀ a, g.s₀ a) (H.H a)))
  (d.ι (F.multicospanShape.fst (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) (f.s₀ a, g.s₀ a) (H.H a))) ≫
    (F.multicospanIndex P).fst (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) (f.s₀ a, g.s₀ a) (H.H a)))
  (d.ι (F.multicospanShape.snd (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) (f.s₀ a, g.s₀ a) (H.H a))) ≫
    (F.multicospanIndex P).snd (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) (f.s₀ a, g.s₀ a) (H.H a)))
Tactic: have heq := d.condition ⟨⟨(f.s₀ a), (g.s₀ a)⟩, H.H a⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
⊢ IsLimit (F.multifork G)
have refine_1 : (E : Multifork (F.multicospanIndex G)) → E.pt ⟶ (F.multifork G).pt
Tactic: refine Multifork.IsLimit.mk _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
refine_1 : (E : Multifork (F.multicospanIndex G)) → E.pt ⟶ (F.multifork G).pt
⊢ IsLimit (F.multifork G)
have refine_2 : ∀ (E_1 : Multifork (F.multicospanIndex G)) (i : F.multicospanShape.L),
  Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) sorry ≫
      (F.multifork G).ι i =
    E_1.ι i
Tactic: refine Multifork.IsLimit.mk _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
refine_1 : (E : Multifork (F.multicospanIndex G)) → E.pt ⟶ (F.multifork G).pt
refine_2 :
  ∀ (E_1 : Multifork (F.multicospanIndex G)) (i : F.multicospanShape.L),
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
        (F.multifork G).ι i =
      E_1.ι i
⊢ IsLimit (F.multifork G)
have refine_3 : ∀ (E_1 : Multifork (F.multicospanIndex G)) (m : E_1.pt ⟶ (F.multifork G).pt),
  (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = E_1.ι i) →
    m = Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) sorry
Tactic: refine Multifork.IsLimit.mk _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
⊢ t.pt ⟶ (F.multifork G).pt
have refine_1 : ∀ (b : E.multicospanShape.R),
  Eq (α := t.pt ⟶ (E.multicospanIndex G).right b)
    ((fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) (E.multicospanShape.fst b) ≫
      (E.multicospanIndex G).fst b)
    ((fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) (E.multicospanShape.snd b) ≫
      (E.multicospanIndex G).snd b)
Tactic: refine Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
b : E.multicospanShape.R
⊢ Eq (α := t.pt ⟶ (E.multicospanIndex G).right b)
    ((fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) (E.multicospanShape.fst b) ≫
      (E.multicospanIndex G).fst b)
    ((fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) (E.multicospanShape.snd b) ≫
      (E.multicospanIndex G).snd b)
have refine_1 : (t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      G.map (Quiver.Hom.op (f.h₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))) ≫
    G.map (E.p₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
  (t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      G.map (Quiver.Hom.op (f.h₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))) ≫
    G.map (E.p₂ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
b : E.multicospanShape.R
⊢ (t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
        G.map (Quiver.Hom.op (f.h₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))) ≫
      G.map (E.p₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    (t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
        G.map (Quiver.Hom.op (f.h₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))) ≫
      G.map (E.p₂ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op
have refine_1 : t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
    G.map
      (E.p₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          f.h₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1).op =
  t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    G.map
      (E.p₂ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          f.h₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2).op
Tactic: simp only [Category.assoc, ← Functor.map_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
b : E.multicospanShape.R
⊢ t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      G.map
        (E.p₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            f.h₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1).op =
    t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      G.map
        (E.p₂ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            f.h₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2).op
have refine_1 : t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
    G.map
      (f.h₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          F.p₁ (f.s₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
  t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    G.map
      (f.h₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
          F.p₂ (f.s₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
Tactic: rw [← f.w₁₁, ← f.w₁₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
b : E.multicospanShape.R
⊢ t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      G.map
        (f.h₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₁ (f.s₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      G.map
        (f.h₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
have refine_1 : t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
    G.map (F.p₁ (f.s₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
      G.map (f.h₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
  t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    G.map (F.p₂ (f.s₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
      G.map (f.h₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op
Tactic: simp only [op_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
⊢ Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (F.multifork G).ι i =
    t.ι i
have refine_2 : Multifork.IsLimit.lift hE (fun (a : E.I₀) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) sorry ≫ G.map (F.f i).op = t.ι i
Tactic: simp only [multicospanIndex_left, multicospanShape_L, multifork_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
⊢ Multifork.IsLimit.lift hE (fun (a : E.I₀) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map (F.f i).op = t.ι i
have h1 : hgf.a i ≫ F.p₁ (hgf.H i) = (g.comp f).h₀ i
Tactic: have h1 := hgf.wl i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = (g.comp f).h₀ i
⊢ Multifork.IsLimit.lift hE (fun (a : E.I₀) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map (F.f i).op = t.ι i
have h2 : Eq (α :=
  t.pt ⟶
    (F.multicospanIndex G).right
      (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i) (hgf.H i)))
  (t.ι
      (F.multicospanShape.fst
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i) (hgf.H i))) ≫
    (F.multicospanIndex G).fst
      (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i) (hgf.H i)))
  (t.ι
      (F.multicospanShape.snd
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i) (hgf.H i))) ≫
    (F.multicospanIndex G).snd
      (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i) (hgf.H i)))
Tactic: have h2 := t.condition ⟨⟨_, _⟩, hgf.H i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ Multifork.IsLimit.lift hE (fun (a : E.I₀) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map (F.f i).op = t.ι i
have refine_2 : t.ι i ≫ G.map ((Hom.id F).h₀ i).op = t.ι i
Tactic: rw [← g.w₀, op_comp, Functor.map_comp, ← E.multifork_ι, Multifork.IsLimit.fac_assoc,
      Category.assoc, ← Functor.map_comp, ← op_comp, ← h1, op_comp, Functor.map_comp,
      reassoc_of% h2, ← Functor.map_comp, ← op_comp, hgf.wr i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
⊢ m = Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯
have refine_3 : ∀ (i : E.multicospanShape.L),
  m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) sorry ≫
      (E.multifork G).ι i
Tactic: refine Multifork.IsLimit.hom_ext hE fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
⊢ m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι i
have refine_3 : m ≫ (E.multifork G).ι i = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
Tactic: rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
refine_3 : m ≫ (E.multifork G).ι i = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
⊢ m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι i
have refine_3₁ : m ≫ G.map (E.f i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
Tactic: rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
refine_3 : m ≫ (E.multifork G).ι i = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₁ : m ≫ G.map (E.f i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
⊢ m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι i
have refine_3₂ : m ≫ G.map (f.h₀ i ≫ F.f (f.s₀ i)).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
Tactic: rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]