awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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
⊢ (Sieve.pullback h S).arrows g

Tactic:
simp [comm, hf]
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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)
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
⊢ 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⟩
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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)
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:
⟨_, _, hg⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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)
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:
exact ⟨_, _, hg⟩
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
J : GrothendieckTopology.{v, u} C
S : J.Cover X
⊢ (↑S : Sieve X) ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
S.2

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
J : GrothendieckTopology.{v, u} C
S T : J.Cover X
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), (↑S : Sieve X).arrows f ↔ (↑T : Sieve X).arrows f
⊢ S = T

Tactic:
Subtype.ext <| Sieve.ext h

Premises used: CategoryTheory.Sieve.ext, CategoryTheory.GrothendieckTopology.Cover, Subtype.ext
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
x : J.Cover X
x_1 : C
x_2 : x_1 ⟶ X
h : (↑x : Sieve X).arrows x_2
⊢ (↑(Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) ⊤ ⋯) : Sieve X).arrows x_2

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y_1 : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
x x_1 : J.Cover X
h1 : x ≤ x_1
h2 : x_1 ≤ x
Y : C
f : Y ⟶ X
⊢ (↑x : Sieve X).arrows f → (↑x_1 : Sieve X).arrows f

Tactic:
apply h1
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y_1 : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
x x_1 : J.Cover X
h1 : x ≤ x_1
h2 : x_1 ≤ x
Y : C
f : Y ⟶ X
⊢ (↑x_1 : Sieve X).arrows f → (↑x : Sieve X).arrows f

Tactic:
apply h2
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S_1 R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S : J.Cover X
I₁ I₂ : (S.pullback f).Arrow
r : I₁.Relation I₂
⊢ r.g₁ ≫ I₁.base.f = r.g₂ ≫ I₂.base.f

Tactic:
simp [r.w_assoc]

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w_assoc
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
Z : C
f : Y ⟶ X
g : Z ⟶ Y
S : J.Cover X
⊢ (↑(S.pullback f) : Sieve Y).arrows g ↔ (↑S : Sieve X).arrows (g ≫ f)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y_1 : C
S_1 R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑(S.pullback (𝟙 X)) : Sieve X).arrows f ↔ (↑S : Sieve X).arrows f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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 Y_2 Z : C
S : J.Cover X
f_1 : Z ⟶ Y_2
g : Y_2 ⟶ X
Y : C
f : Y ⟶ Z
⊢ (↑(S.pullback (f_1 ≫ g)) : Sieve Z).arrows f ↔ (↑((S.pullback g).pullback f_1) : Sieve Z).arrows f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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
rw : (↑S : Sieve X).arrows (e1 ≫ e2)
⊢ (↑S : Sieve X).arrows f

Tactic:
rw [← h3]
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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
x : (↑S : Sieve X).arrows e2
⊢ (↑S : Sieve X).arrows (e1 ≫ e2)

Tactic:
apply Sieve.downward_closed

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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 e2

Tactic:
h1
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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 e2

Tactic:
exact h1
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
I : (S.bind T).Arrow
⊢ (↑S : Sieve X).arrows I.fromMiddleHom

Tactic:
I.hf.choose_spec.choose_spec.choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom, Exists.choose, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
I : (S.bind T).Arrow
⊢ Sieve.arrows (↑(T I.fromMiddle) : Sieve I.fromMiddle.Y) I.toMiddleHom

Tactic:
I.hf.choose_spec.choose_spec.choose_spec.choose_spec.1

Premises used: Exists.choose_spec, CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddle, CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, And.left, CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
I : (S.bind T).Arrow
⊢ I.toMiddleHom ≫ I.fromMiddleHom = I.f

Tactic:
I.hf.choose_spec.choose_spec.choose_spec.choose_spec.2

Premises used: Exists.choose_spec, CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, And.right, CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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
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
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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
⊢ 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:
simp only [← P.map_comp, ← op_comp, I.r.w]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.GrothendieckTopology.Cover.Relation.r, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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
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
⊢ 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)

Tactic:
dsimp only [shape, index, Relation.fst, Relation.snd]

Premises used: CategoryTheory.GrothendieckTopology.Cover.shape, CategoryTheory.GrothendieckTopology.Cover.index, CategoryTheory.GrothendieckTopology.Cover.Relation.fst, CategoryTheory.GrothendieckTopology.Cover.Relation.snd
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
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
⊢ 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:
simp only [← P.map_comp, ← op_comp, I.r.w]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.GrothendieckTopology.Cover.Relation.r, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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

Tactic:
Multifork.IsLimit.hom_ext hc fun a ↦ ?_

Premises used: CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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)
refine : ∀ (a : E.multicospanShape.L), f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = g.mapMultiforkOfIsLimit P hc d ≫ c.ι a
⊢ f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d

Tactic:
refine Multifork.IsLimit.hom_ext hc fun a ↦ ?_

Premises used: CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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
⊢ 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⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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
heq : d.ι (f.s₀ a) ≫ P.map (F.p₁ (H.H a)).op = d.ι (g.s₀ a) ≫ P.map (F.p₂ (H.H a)).op
⊢ f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = g.mapMultiforkOfIsLimit P hc d ≫ c.ι a

Tactic:
simp [-Homotopy.wl, -Homotopy.wr, ← H.wl, ← H.wr, reassoc_of% heq]

Premises used: CategoryTheory.PreOneHypercover.Homotopy.wl, CategoryTheory.PreOneHypercover.Homotopy.wr
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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
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) ⋯
⊢ IsLimit (F.multifork G)

Tactic:
refine Multifork.IsLimit.mk _ ?_ ?_ ?_

Premises used: CategoryTheory.Limits.Multifork.IsLimit.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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)
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)
⊢ t.pt ⟶ (F.multifork G).pt

Tactic:
refine Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ?_

Premises used: CategoryTheory.PreZeroHypercover.Hom.h₀, Quiver.Hom.op, CategoryTheory.PreOneHypercover.Hom.toHom, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Multifork.ι, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Limits.Multifork.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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
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
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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
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
⊢ (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:
simp only [Category.assoc, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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
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
⊢ 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:
rw [← f.w₁₁, ← f.w₁₂]

Premises used: CategoryTheory.PreOneHypercover.Hom.w₁₁, CategoryTheory.PreOneHypercover.Hom.w₁₂
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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
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
⊢ 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:
simp only [op_comp, Functor.map_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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.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:
t.condition_assoc ⟨(f.s₀ b.1.1, f.s₀ b.1.2), f.s₁ b.2⟩ _

Premises used: CategoryTheory.PreOneHypercover.Hom.s₁, Prod.mk, Sigma.fst, CategoryTheory.PreOneHypercover.Hom.toHom, Prod.fst, Sigma.mk, CategoryTheory.PreZeroHypercover.Hom.s₀, Sigma.snd, Prod.snd, CategoryTheory.Limits.Multifork.condition_assoc