awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_2 : Preregular.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
inst_4 : ∀ (X : C), Projective.{v_1, u_1} X
rw : PreservesFiniteProducts F ↔ IsSheaf (extensiveTopology C) F
rw₁ rw₂ : PreservesFiniteProducts F ↔ PreservesFiniteProducts F
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective, isSheaf_iff_preservesFiniteProducts]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts, CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : PreservesFiniteLimits s
hF : IsSheaf (coherentTopology C) F
rw :
  ∀ (hF : PreservesFiniteProducts F ∧ EqualizerCondition F),
    PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ IsSheaf (coherentTopology C) (F ⋙ s)

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (h := h)] at hF ⊢

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ PreservesFiniteProducts F

Tactic:
have := hF.1
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
this : PreservesFiniteProducts F
⊢ PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)

Tactic:
⟨inferInstance, fun _ _ π _ c hc ↦ ⟨?_⟩⟩

Premises used: inferInstance, Nonempty.intro, And.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
this : PreservesFiniteProducts F
refine :
  (x x_1 : C) →
    (π : x ⟶ x_1) → EffectiveEpi π → (c : PullbackCone π π) → (hc : IsLimit c) → IsLimit (Fork.ofι ((F ⋙ s).map π.op) ⋯)
⊢ PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)

Tactic:
refine ⟨inferInstance, fun _ _ π _ c hc ↦ ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
this : PreservesFiniteProducts F
x x_1 : C
π : x ⟶ x_1
h_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι ((F ⋙ s).map π.op) ⋯)

Tactic:
exact isLimitForkMapOfIsLimit s _ (hF.2 π c hc).some

Premises used: Nonempty.some, And.right, CategoryTheory.Limits.isLimitForkMapOfIsLimit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : ReflectsFiniteLimits s
hF : IsSheaf (coherentTopology C) (F ⋙ s)
rw :
  ∀ (hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)),
    PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ IsSheaf (coherentTopology C) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (h := h)] at hF ⊢

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts (F ⋙ s)

Tactic:
obtain ⟨_, hF₂⟩ := hF
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
left : PreservesFiniteProducts (F ⋙ s)
⊢ EqualizerCondition (F ⋙ s)

Tactic:
obtain ⟨_, hF₂⟩ := hF
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : ReflectsFiniteLimits s
left : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
⟨⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩, fun _ _ π _ c hc ↦ ⟨?_⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Limits.PreservesLimit.mk, And.intro, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : ReflectsFiniteLimits s
left : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
refine_1 :
  ∀ (n : ℕ) {K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ} {c : Cone K} (hc : IsLimit c),
    Nonempty (IsLimit (F.mapCone c))
refine_2 :
  (x x_1 : C) →
    (π : x ⟶ x_1) → EffectiveEpi π → (c : PullbackCone π π) → (hc : IsLimit c) → IsLimit (Fork.ofι (F.map π.op) ⋯)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
refine ⟨⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩, fun _ _ π _ c hc ↦ ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : ReflectsFiniteLimits s
left : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩

Premises used: CategoryTheory.Limits.isLimitOfReflects, CategoryTheory.Functor.comp, Nonempty.intro, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : ReflectsFiniteLimits s
left : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
exact ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst_5 : ReflectsFiniteLimits s
left : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
x x_1 : C
π : x ⟶ x_1
h_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι (F.map π.op) ⋯)

Tactic:
exact isLimitOfIsLimitForkMap s _ (hF₂ π c hc).some

Premises used: CategoryTheory.Limits.isLimitOfIsLimitForkMap, Nonempty.some
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
inst_5 : ∀ (X : C), Projective.{v_1, u_1} X
inst_6 : PreservesFiniteProducts s
hF : IsSheaf (coherentTopology C) F
rw : ∀ (hF : PreservesFiniteProducts F), PreservesFiniteProducts (F ⋙ s)
⊢ IsSheaf (coherentTopology C) (F ⋙ s)

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective] at hF ⊢

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
inst_5 : ∀ (X : C), Projective.{v_1, u_1} X
inst_6 : PreservesFiniteProducts s
hF : PreservesFiniteProducts F
⊢ PreservesFiniteProducts (F ⋙ s)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
inst_5 : ∀ (X : C), Projective.{v_1, u_1} X
inst_6 : ReflectsFiniteProducts s
hF : IsSheaf (coherentTopology C) (F ⋙ s)
rw : ∀ (hF : PreservesFiniteProducts (F ⋙ s)), PreservesFiniteProducts F
⊢ IsSheaf (coherentTopology C) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective] at hF ⊢

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
inst_5 : ∀ (X : C), Projective.{v_1, u_1} X
inst_6 : ReflectsFiniteProducts s
hF : PreservesFiniteProducts (F ⋙ s)
⊢ PreservesFiniteProducts F

Tactic:
⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩⟩⟩⟩

Premises used: CategoryTheory.Limits.isLimitOfReflects, CategoryTheory.Functor.comp, Nonempty.intro, CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Limits.PreservesLimit.mk, CategoryTheory.Limits.PreservesFiniteProducts.mk, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
B : Type u₄
inst_2 : Category.{v₄, u₄} B
s : Functor.{v₃, v₄, u₃, u₄} A B
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
inst_5 : ∀ (X : C), Projective.{v_1, u_1} X
inst_6 : ReflectsFiniteProducts s
hF : PreservesFiniteProducts (F ⋙ s)
⊢ PreservesFiniteProducts F

Tactic:
exact ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
X : C
W : (J.Cover X)ᵒᵖ
refine : (J.diagram P X ⋙ F).obj W ≅ limit (((unop W).index P).multicospan ⋙ F)
⊢ (J.diagram P X ⋙ F).obj W ≅ (J.diagram (P ⋙ F) X).obj W

Tactic:
refine ?_ ≪≫ HasLimit.isoOfNatIso (W.unop.multicospanComp _ _).symm

Premises used: CategoryTheory.Limits.HasLimit.isoOfNatIso, CategoryTheory.GrothendieckTopology.Cover.multicospanComp, CategoryTheory.Iso.symm, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
X : C
W : (J.Cover X)ᵒᵖ
⊢ (J.diagram P X ⋙ F).obj W ≅ limit (((unop W).index P).multicospan ⋙ F)

Tactic:
refine
        (isLimitOfPreserves F (limit.isLimit _)).conePointUniqueUpToIso (limit.isLimit _)

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
X : C
A B : (J.Cover X)ᵒᵖ
f : A ⟶ B
dsimp :
  Eq (α := F.obj (multiequalizer ((unop A).index P)) ⟶ multiequalizer ((unop B).index (P ⋙ F)))
    (CategoryStruct.comp (Y := F.obj (multiequalizer ((unop B).index P)))
      (F.map
        (Multiequalizer.lift ((unop B).index P) (multiequalizer ((unop A).index P))
          (fun (I : (unop B).Arrow) ↦ Multiequalizer.ι ((unop A).index P) (I.map f.unop)) ⋯))
      (CategoryStruct.comp (Y := limit (((unop B).index P).multicospan ⋙ F))
        (Iso.hom
          (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop B).index P).multicospan))
            (limit.isLimit (((unop B).index P).multicospan ⋙ F))))
        (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop B)).symm))))
    (CategoryStruct.comp (Y := multiequalizer ((unop A).index (P ⋙ F)))
      (CategoryStruct.comp (Y := limit (((unop A).index P).multicospan ⋙ F))
        (Iso.hom
          (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan))
            (limit.isLimit (((unop A).index P).multicospan ⋙ F))))
        (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm)))
      (Multiequalizer.lift ((unop B).index (P ⋙ F)) (multiequalizer ((unop A).index (P ⋙ F)))
        (fun (I : (unop B).Arrow) ↦ Multiequalizer.ι ((unop A).index (P ⋙ F)) (I.map f.unop)) ⋯))
⊢ (J.diagram P X ⋙ F).map f ≫
      Iso.hom
        ((fun (W : (J.Cover X)ᵒᵖ) ↦
            (Iso.trans (Y := limit (((unop W).index P).multicospan ⋙ F))
                (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
                  (limit.isLimit (((unop W).index P).multicospan ⋙ F)))
                (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm) :
              (J.diagram P X ⋙ F).obj W ≅ (J.diagram (P ⋙ F) X).obj W))
          B) =
    Iso.hom
        ((fun (W : (J.Cover X)ᵒᵖ) ↦
            (Iso.trans (Y := limit (((unop W).index P).multicospan ⋙ F))
                (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
                  (limit.isLimit (((unop W).index P).multicospan ⋙ F)))
                (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm) :
              (J.diagram P X ⋙ F).obj W ≅ (J.diagram (P ⋙ F) X).obj W))
          A) ≫
      (J.diagram (P ⋙ F) X).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
X : C
A B : (J.Cover X)ᵒᵖ
f : A ⟶ B
g : (unop B).shape.L
⊢ Eq (α := F.obj (multiequalizer ((unop A).index P)) ⟶ ((unop B).index (P ⋙ F)).left g)
    (CategoryStruct.comp (Y := multiequalizer ((unop B).index (P ⋙ F)))
      (CategoryStruct.comp (Y := F.obj (multiequalizer ((unop B).index P)))
        (F.map
          (Multiequalizer.lift ((unop B).index P) (multiequalizer ((unop A).index P))
            (fun (I : (unop B).Arrow) ↦ Multiequalizer.ι ((unop A).index P) (I.map f.unop)) ⋯))
        (CategoryStruct.comp (Y := limit (((unop B).index P).multicospan ⋙ F))
          (Iso.hom
            (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop B).index P).multicospan))
              (limit.isLimit (((unop B).index P).multicospan ⋙ F))))
          (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop B)).symm))))
      (Multiequalizer.ι ((unop B).index (P ⋙ F)) g))
    (CategoryStruct.comp (Y := multiequalizer ((unop B).index (P ⋙ F)))
      (CategoryStruct.comp (Y := multiequalizer ((unop A).index (P ⋙ F)))
        (CategoryStruct.comp (Y := limit (((unop A).index P).multicospan ⋙ F))
          (Iso.hom
            (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan))
              (limit.isLimit (((unop A).index P).multicospan ⋙ F))))
          (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm)))
        (Multiequalizer.lift ((unop B).index (P ⋙ F)) (multiequalizer ((unop A).index (P ⋙ F)))
          (fun (I : (unop B).Arrow) ↦ Multiequalizer.ι ((unop A).index (P ⋙ F)) (I.map f.unop)) ⋯))
      (Multiequalizer.ι ((unop B).index (P ⋙ F)) g))

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).Arrow
delta :
  Eq (α := (J.diagram P X ⋙ F).obj W ⟶ ((unop W).index (P ⋙ F)).left i)
    (CategoryStruct.comp (Y := (J.diagram (P ⋙ F) X).obj W)
        (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (W : (J.Cover X)ᵒᵖ) ↦
                  Iso.trans (Y := limit (((unop W).index P).multicospan ⋙ F))
                    (IsLimit.conePointUniqueUpToIso
                      (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
                      (limit.isLimit (((unop W).index P).multicospan ⋙ F)))
                    (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm))
                ⋯))
            W :
          (J.diagram P X ⋙ F).obj W ⟶ (J.diagram (P ⋙ F) X).obj W)
        (Multiequalizer.ι ((unop W).index (P ⋙ F)) i :
          multiequalizer ((unop W).index (P ⋙ F)) ⟶ ((unop W).index (P ⋙ F)).left i) :
      (J.diagram P X ⋙ F).obj W ⟶ ((unop W).index (P ⋙ F)).left i)
    (F.map (Multiequalizer.ι ((unop W).index P) i) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (((unop W).index P).left i))
⊢ Eq (α := (J.diagram P X ⋙ F).obj W ⟶ ((unop W).index (P ⋙ F)).left i)
    (CategoryStruct.comp (Y := (J.diagram (P ⋙ F) X).obj W)
        (NatTrans.app (Iso.hom (J.diagramCompIso F P X)) W : (J.diagram P X ⋙ F).obj W ⟶ (J.diagram (P ⋙ F) X).obj W)
        (Multiequalizer.ι ((unop W).index (P ⋙ F)) i :
          multiequalizer ((unop W).index (P ⋙ F)) ⟶ ((unop W).index (P ⋙ F)).left i) :
      (J.diagram P X ⋙ F).obj W ⟶ ((unop W).index (P ⋙ F)).left i)
    (F.map (Multiequalizer.ι ((unop W).index P) i) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (((unop W).index P).left i))

Tactic:
delta diagramCompIso

Premises used: CategoryTheory.GrothendieckTopology.diagramCompIso