awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
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
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))
⊢ 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

Premises used: CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
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
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:
⟨IsSheafIff.isLimit hP hE le⟩

Premises used: CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.isLimit, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
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
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:
exact ⟨IsSheafIff.isLimit hP hE le⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ ⊤ (Cover.oneHypercover (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ (Cover.oneHypercover (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS)).sieve₀ ≤
    S

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : J.IsGeneratedByOneHypercovers
P : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : GrothendieckTopology.OneHypercover.{w, v, u} J X), Nonempty (IsLimit (E.multifork P))

Tactic:
simpa using GrothendieckTopology.OneHypercoverFamily.isSheaf_iff.{w} ⊤ P
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Z Z' : C
g : Z ⟶ W
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
φ : Z' ⟶ Z
⊢ (φ ≫ g) ≫ p₁ = (φ ≫ h) ≫ E.p₁ j

Tactic:
simpa using φ ≫= fac₁
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Z Z' : C
g : Z ⟶ W
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
φ : Z' ⟶ Z
⊢ (φ ≫ g) ≫ p₂ = (φ ≫ h) ≫ E.p₂ j

Tactic:
simpa using φ ≫= fac₂
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Z Z' : C
g : Z ⟶ W
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
φ : Z' ⟶ Z
⊢ ∃ (j : E.I₁ i₁ i₂) (h : Z' ⟶ E.Y j), (φ ≫ g) ≫ p₁ = h ≫ E.p₁ j ∧ (φ ≫ g) ≫ p₂ = h ≫ E.p₂ j

Tactic:
exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂)
refine_2 : E.sieve₁ (f ≫ p₁) (f ≫ p₂) ≤ Sieve.pullback f (E.sieve₁ p₁ p₂)
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) = E.sieve₁ (f ≫ p₁) (f ≫ p₂)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
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
⊢ (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows g → (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows g

Tactic:
⟨k, u, hu₁, hu₂⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
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
⊢ (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows g → (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows g

Tactic:
⟨k, u, hu₁, hu₂⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂
rw rw₁ : E.p₁ k = E.p₁ k
⊢ CategoryStruct.comp (Y := pullback (E.f i₁) (E.f i₂)) (E.toPullback k) (pullback.fst (E.f i₁) (E.f i₂)) = E.p₁ k

Tactic:
rw [pullback.lift_fst]

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂
rw rw₁ : E.p₂ k = E.p₂ k
⊢ CategoryStruct.comp (Y := pullback (E.f i₁) (E.f i₂)) (E.toPullback k) (pullback.snd (E.f i₁) (E.f i₂)) = E.p₂ k

Tactic:
rw [pullback.lift_snd]

Premises used: CategoryTheory.Limits.pullback.lift_snd
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂
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
⊢ E.sieve₁ p₁ p₂ = Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)

Tactic:
ext Z g
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
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
⊢ (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
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
⊢ (Sieve.pullback (X := pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g

Tactic:
exact ⟨_, h, _, ⟨j⟩, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
Y : C
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac : Eq (α := Z ⟶ pullback (E.f i₁) (E.f i₂)) (h ≫ E.toPullback j) (g ≫ pullback.lift p₁ p₂ w)
⊢ g ≫ p₁ = h ≫ E.p₁ j

Tactic:
simpa using fac.symm =≫ pullback.fst _ _

Premises used: CategoryTheory.Limits.pullback.fst, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
Y : C
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac : Eq (α := Z ⟶ pullback (E.f i₁) (E.f i₂)) (h ≫ E.toPullback j) (g ≫ pullback.lift p₁ p₂ w)
⊢ g ≫ p₂ = h ≫ E.p₂ j

Tactic:
simpa using fac.symm =≫ pullback.snd _ _

Premises used: CategoryTheory.Limits.pullback.snd, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
Y : C
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac : Eq (α := Z ⟶ pullback (E.f i₁) (E.f i₂)) (h ≫ E.toPullback j) (g ≫ pullback.lift p₁ p₂ w)
⊢ (E.sieve₁ p₁ p₂).arrows g

Tactic:
exact ⟨j, h, by simpa using fac.symm =≫ pullback.fst _ _,
      by simpa using fac.symm =≫ pullback.snd _ _⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂)
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₂)) ⋯) (E.sieve₁' i₁ 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₂)))

Tactic:
rw [← Sieve.pullback_id (S := E.sieve₁' i₁ i₂),
    sieve₁_eq_pullback_sieve₁' _ _ _ pullback.condition]

Premises used: CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁', CategoryTheory.Limits.pullback.condition, CategoryTheory.Sieve.pullback_id
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂)
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₂)) ⋯
⊢ 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₂)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i : E.I₁'
⊢ E.Y' i = E.Y (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))

Tactic:
rfl

Premises used: rfl, CategoryTheory.PreOneHypercover.Y'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂
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
⊢ 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))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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₂
⊢ 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:
simp only [← F.map_comp, ← op_comp, E.w]

Premises used: CategoryTheory.op_comp, CategoryTheory.PreOneHypercover.w, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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 : E.I₀
⊢ (E.multifork F).ι i = F.map (E.f i).op

Tactic:
rfl

Premises used: CategoryTheory.Limits.Multifork.ι, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
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
⊢ 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))

Tactic:
simp_rw [← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
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
⊢ 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:
congr 2
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
⊢ ∀ (i : E.I₁'),
    d.inj i ≫
        (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 =
      d.inj i ≫
        (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:
simp [E.w]

Premises used: CategoryTheory.PreOneHypercover.w
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
⊢ (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:
exact Cofan.IsColimit.hom_ext hd _ _ (by simp [E.w])

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
i : E.I₀
⊢ (E.forkOfIsColimit hc hd F).ι ≫ F.map (c.inj i).op = F.map (E.f i).op

Tactic:
simp [forkOfIsColimit, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.PreOneHypercover.forkOfIsColimit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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 :
  IsLimit (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≃
    IsLimit (E.forkOfIsColimit hc hd F)
⊢ IsLimit (E.multifork F) ≃ IsLimit (E.forkOfIsColimit hc hd F)

Tactic:
refine (IsLimit.ofConeEquiv <|
    (E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').symm.trans ?_

Premises used: Equiv.trans, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit, CategoryTheory.Limits.IsLimit.ofConeEquiv, Equiv.symm, CategoryTheory.PreOneHypercover.multicospanIndex
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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)
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)
⊢ IsLimit (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≃
    IsLimit (E.forkOfIsColimit hc hd F)

Tactic:
refine Fork.isLimitEquivOfIsos _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Fork.isLimitEquivOfIsos