awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
rw : K.W (G.op.whiskerLeft f) ↔ MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f
⊢ K.W (G.op.whiskerLeft f) ↔ J.W f

Tactic:
rw [← W_inverseImage_whiskeringLeft J K G]

Premises used: CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
⊢ K.W (G.op.whiskerLeft f) ↔ MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : J.W f
⊢ K.W (G.op.whiskerLeft f)

Tactic:
rw [← J.W_whiskerLeft_iff (G := G) (K := K)] at hf

Premises used: CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
⊢ K.W (whiskerRight (G.op.whiskerLeft f) F)

Tactic:
have := K.W_of_preservesSheafification F (whiskerLeft G.op f) hf
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W (whiskerRight (G.op.whiskerLeft f) F)
⊢ K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)

Tactic:
rw [whiskerRight_left] at this

Premises used: CategoryTheory.Functor.whiskerRight_left
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
⊢ K.W (G.op.whiskerLeft (whiskerRight f F))

Tactic:
haveI := K.W.of_postcomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_inv _) <|
      K.W.of_precomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_hom _) this
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this_1 : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
this : K.W (G.op.whiskerLeft (whiskerRight f F))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : J.W (whiskerRight f F)), MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f
⊢ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f

Tactic:
rwa [K.W_whiskerLeft_iff (G := G) (J := J) (f := whiskerRight f F)] at this

Premises used: CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff, CategoryTheory.Functor.whiskerRight
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_7 : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst_8 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_9 : ConcreteCategory.{u_2, v₃, u₃, u_1} A FA (CC := CA)
inst_10 : WEqualsLocallyBijective.{u_2, v₃, v₂, u₃, u₂, u_1} K A (FA := FA) (CA := CA)
hG : CoverPreserving K J G
X Y : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : X ⟶ Y
rw :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₁ :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₂ :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
      Presheaf.IsLocallySurjective K (FA := FA) (CA := CA) (G.op.whiskerLeft f)
rw₃ rw₄ :
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
      Presheaf.IsLocallySurjective K (FA := FA) (CA := CA) (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
      Presheaf.IsLocallySurjective K (FA := FA) (CA := CA) (G.op.whiskerLeft f)
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f

Tactic:
rw [← W_whiskerLeft_iff J K G f, ← Presheaf.isLocallyInjective_whisker_iff K J G f hG,
      ← Presheaf.isLocallySurjective_whisker_iff K J G f hG, W_iff_isLocallyBijective]

Premises used: CategoryTheory.Presheaf.isLocallyInjective_whisker_iff, CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff, CategoryTheory.Presheaf.isLocallySurjective_whisker_iff, CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
FA : A → A → Type u_1
CA : A → Type u_2
inst_2 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_2, v₃, u₃, u_1} A FA (CC := CA)
inst_4 : EssentiallySmall.{w, v₁, u₁} C
inst_5 :
  ∀ (X : Cᵒᵖ),
    HasLimitsOfShape
      (StructuredArrow.{w, v₁, w, u₁} (C := (SmallModel.{w, v₁, u₁} C)ᵒᵖ) X
        (Functor.op (Equivalence.inverse (equivSmallModel C))))
      A
inst_6 :
  WEqualsLocallyBijective.{u_2, v₃, w, u₃, w, u_1} (C := SmallModel.{w, v₁, u₁} C)
    (inducedTopology (Equivalence.inverse (equivSmallModel C)) J) A (FA := FA) (CA := CA)
⊢ WEqualsLocallyBijective.{u_2, v₃, v₁, u₃, u₁, u_1} J A (FA := FA) (CA := CA)

Tactic:
WEqualsLocallyBijective.transport J ((equivSmallModel C).inverse.inducedTopology J)
    (equivSmallModel C).inverse (IsDenseSubsite.coverPreserving _ _ _)

Premises used: CategoryTheory.Functor.inducedTopology, CategoryTheory.Functor.IsDenseSubsite.coverPreserving, CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.transport, CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_8 : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst_9 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_10 : ConcreteCategory.{u_2, v₃, u₃, u_1} A FA (CC := CA)
inst_11 : WEqualsLocallyBijective.{u_2, v₃, v₂, u₃, u₂, u_1} K A (FA := FA) (CA := CA)
inst_12 : EssentiallySmall.{w, v₁, u₁} C
inst_13 :
  ∀ (X : Cᵒᵖ),
    HasLimitsOfShape
      (StructuredArrow.{w, v₁, w, u₁} (C := (SmallModel.{w, v₁, u₁} C)ᵒᵖ) X
        (Functor.op (Equivalence.inverse (equivSmallModel C))))
      A
inst_14 :
  ∀ (X : Cᵒᵖ),
    HasLimitsOfShape
      (StructuredArrow.{w, v₁, w, u₁} (C := (SmallModel.{w, v₁, u₁} C)ᵒᵖ) X
        (Functor.op (Equivalence.inverse (equivSmallModel C))))
      B
inst_15 :
  PreservesSheafification.{w, w, v₃, u₃, v₄, u₄} (C := SmallModel.{w, v₁, u₁} C)
    (inducedTopology (Equivalence.inverse (equivSmallModel C)) J) F
⊢ J.PreservesSheafification F

Tactic:
PreservesSheafification.transport (A := A) J
    ((equivSmallModel C).inverse.inducedTopology J) (equivSmallModel C).inverse B F

Premises used: CategoryTheory.Functor.inducedTopology, CategoryTheory.GrothendieckTopology.PreservesSheafification.transport, CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Finite
Goal:
C : Type u
inst : Category.{v, u} C
X : C
s : Presieve.{v, u} X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (coverings (finite C) X) s ↔ s.uncurry.Finite

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Finite
-- Module: Mathlib.CategoryTheory.Sites.Finite
Goal:
C : Type u
inst : Category.{v, u} C
X : C
ι : Type u_1
inst_1 : Finite ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (coverings (finite C) X) (ofArrows Y f)

Tactic:
simpa using Set.finite_range _

Premises used: Set.finite_range
-- Module: Mathlib.CategoryTheory.Sites.Finite
Goal:
C : Type u
inst : Category.{v, u} C
⊢ ∀ {S T : C} (f : S ⟶ T) [IsIso f],
    Membership.mem (γ := Set (Presieve.{v, u} T)) (coverings (finite C) T) (Presieve.singleton f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Finite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
u : Y ⟶ X
s : Presieve.{v, u} X
hs : Membership.mem (γ := Set (Presieve.{v, u} X)) (Precoverage.coverings (Precoverage.finite C) X) s
⊢ Membership.mem (γ := Set (Presieve.{v, u} Y)) (Precoverage.coverings (Precoverage.finite C) Y) (pullbackArrows u s)

Tactic:
simpa using hs.image _

Premises used: Set.Finite.image
-- Module: Mathlib.CategoryTheory.Sites.Finite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X : C
s : Presieve.{v, u} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v, u} Y
hs : Membership.mem (γ := Set (Presieve.{v, u} X)) (Precoverage.coverings (Precoverage.finite C) X) s
ht :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : s f),
    Membership.mem (γ := Set (Presieve.{v, u} Y)) (Precoverage.coverings (Precoverage.finite C) Y) (t f H)
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (Precoverage.coverings (Precoverage.finite C) X) (s.bind t)

Tactic:
simpa using hs.biUnion' fun _ _ ↦ (ht _ _).image _

Premises used: Set.Finite.biUnion', Set.Finite.image
-- Module: Mathlib.CategoryTheory.Sites.Finite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X : C
ι : Type u_1
inst_2 : Finite ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (Precoverage.coverings (toPrecoverage (finite C)) X) (ofArrows Y f)

Tactic:
Precoverage.ofArrows_mem_finite _ _

Premises used: Set.Mem, CategoryTheory.Precoverage.ofArrows_mem_finite
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasTerminal.{v, u} C
⊢ HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A

Tactic:
⟨_, ⟨constantSheafAdj J A terminalIsTerminal⟩⟩

Premises used: Nonempty.intro, CategoryTheory.constantSheafAdj, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasLimitsOfShape.{v, u, v₂, u₂} Cᵒᵖ A
⊢ HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A

Tactic:
⟨sheafToPresheaf J A ⋙ lim, ⟨constLimAdj.comp (sheafificationAdjunction J A)⟩⟩

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.lim, CategoryTheory.sheafificationAdjunction, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Limits.constLimAdj, CategoryTheory.Adjunction.comp, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
X' X : A
F : Sheaf.{v, v₂, u, u₂} J A
f : X' ⟶ X
g : Functor.obj (Functor.const Cᵒᵖ) X ⟶ F.obj (P := Presheaf.IsSheaf J)
⊢ Eq.{v₂ + 1} (α := X' ⟶ Functor.obj (Γ J A) F)
    ((ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj X' ⟶ F.obj) → X' ⟶ (Γ J A).obj F)
        (Functor.map (Functor.const Cᵒᵖ) f ≫ g) :
      X' ⟶ Functor.obj (Γ J A) F)
    (f ≫ (ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj X ⟶ F.obj) → X ⟶ (Γ J A).obj F) g : X' ⟶ Functor.obj (Γ J A) F)

Tactic:
(congrArg _ ((sheafificationAdjunction J A).homEquiv_naturality_left_symm _ _)).trans
    ((constantSheafΓAdj J A).homEquiv_naturality_left _ _)

Premises used: congrArg, CategoryTheory.sheafificationAdjunction, CategoryTheory.constantSheafΓAdj, CategoryTheory.Adjunction.homEquiv_naturality_left_symm, CategoryTheory.Adjunction.homEquiv_naturality_left, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
X' X : A
F : Sheaf.{v, v₂, u, u₂} J A
f : X' ⟶ X
g : X ⟶ Functor.obj (Γ J A) F
⊢ Eq (α := Functor.obj (Functor.const Cᵒᵖ) X' ⟶ F.obj (P := Presheaf.IsSheaf J))
    ((Equiv.symm ΓHomEquiv : (a : X' ⟶ (Γ J A).obj F) → (Functor.const Cᵒᵖ).obj X' ⟶ F.obj) (f ≫ g) :
      Functor.obj (Functor.const Cᵒᵖ) X' ⟶ F.obj (P := Presheaf.IsSheaf J))
    (Functor.map (Functor.const Cᵒᵖ) f ≫
        (Equiv.symm ΓHomEquiv : (a : X ⟶ (Γ J A).obj F) → (Functor.const Cᵒᵖ).obj X ⟶ F.obj) g :
      Functor.obj (Functor.const Cᵒᵖ) X' ⟶ F.obj (P := Presheaf.IsSheaf J))

Tactic:
(congrArg _ ((constantSheafΓAdj J A).homEquiv_naturality_left_symm _ _)).trans
    ((sheafificationAdjunction J A).homEquiv_naturality_left _ _)

Premises used: CategoryTheory.NatTrans.vcomp, congrArg, CategoryTheory.sheafificationAdjunction, CategoryTheory.constantSheafΓAdj, CategoryTheory.Adjunction.homEquiv_naturality_left_symm, CategoryTheory.Adjunction.homEquiv_naturality_left, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
X : A
F F' : Sheaf.{v, v₂, u, u₂} J A
f : Functor.obj (Functor.const Cᵒᵖ) X ⟶ F.obj (P := Presheaf.IsSheaf J)
g : F ⟶ F'
⊢ Eq.{v₂ + 1} (α := X ⟶ Functor.obj (Γ J A) F')
    ((ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj X ⟶ F'.obj) → X ⟶ (Γ J A).obj F') (f ≫ g.hom) :
      X ⟶ Functor.obj (Γ J A) F')
    ((ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj X ⟶ F.obj) → X ⟶ (Γ J A).obj F) f ≫ Functor.map (Γ J A) g :
      X ⟶ Functor.obj (Γ J A) F')

Tactic:
(congrArg _ ((sheafificationAdjunction J A).homEquiv_naturality_right_symm _ _)).trans
    ((constantSheafΓAdj J A).homEquiv_naturality_right _ _)

Premises used: congrArg, CategoryTheory.sheafificationAdjunction, CategoryTheory.constantSheafΓAdj, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_right, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
X : A
F F' : Sheaf.{v, v₂, u, u₂} J A
f : X ⟶ Functor.obj (Γ J A) F
g : F ⟶ F'
⊢ Eq (α := Functor.obj (Functor.const Cᵒᵖ) X ⟶ F'.obj (P := Presheaf.IsSheaf J))
    ((Equiv.symm ΓHomEquiv : (a : X ⟶ (Γ J A).obj F') → (Functor.const Cᵒᵖ).obj X ⟶ F'.obj)
        (f ≫ Functor.map (Γ J A) g) :
      Functor.obj (Functor.const Cᵒᵖ) X ⟶ F'.obj (P := Presheaf.IsSheaf J))
    ((Equiv.symm ΓHomEquiv : (a : X ⟶ (Γ J A).obj F) → (Functor.const Cᵒᵖ).obj X ⟶ F.obj) f ≫ g.hom :
      Functor.obj (Functor.const Cᵒᵖ) X ⟶ F'.obj (P := Presheaf.IsSheaf J))

Tactic:
(congrArg _ ((constantSheafΓAdj J A).homEquiv_naturality_right_symm _ _)).trans
    ((sheafificationAdjunction J A).homEquiv_naturality_right _ _)

Premises used: CategoryTheory.NatTrans.vcomp, congrArg, CategoryTheory.sheafificationAdjunction, CategoryTheory.constantSheafΓAdj, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_right, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
j : Cᵒᵖ
suffices :
  Functor.map (Functor.const Cᵒᵖ)
        ((ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj c.pt ⟶ F.obj) → c.pt ⟶ (Γ J A).obj F) c.π) ≫
      F.coneΓ.π =
    c.π
⊢ (ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj c.pt ⟶ F.obj) → c.pt ⟶ (Γ J A).obj F) c.π ≫ F.coneΓ.π.app j = c.π.app j

Tactic:
suffices h : ((Functor.const Cᵒᵖ).map (ΓHomEquiv c.π)) ≫ F.coneΓ.π = c.π from congr_app h j
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
j : Cᵒᵖ
⊢ Functor.map (Functor.const Cᵒᵖ)
        ((ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj c.pt ⟶ F.obj) → c.pt ⟶ (Γ J A).obj F) c.π) ≫
      F.coneΓ.π =
    c.π

Tactic:
simp [coneΓ, ← ΓHomEquiv_naturality_left_symm]

Premises used: CategoryTheory.Sheaf.ΓHomEquiv_naturality_left_symm, CategoryTheory.Sheaf.coneΓ
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
w : ∀ (j : Cᵒᵖ), (Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π).app j = c.π.app j
⊢ Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π = c.π

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
j : Cᵒᵖ
⊢ (Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π).app j = c.π.app j

Tactic:
hf j
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
j : Cᵒᵖ
⊢ (Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π).app j = c.π.app j

Tactic:
exact hf j
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
⊢ Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π = c.π

Tactic:
replace hf : ((Functor.const Cᵒᵖ).map f) ≫ F.coneΓ.π = c.π := by ext j; exact hf j
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
f : c.pt ⟶ F.coneΓ.pt
hf : Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π = c.π
⊢ f = (ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj c.pt ⟶ F.obj) → c.pt ⟶ (Γ J A).obj F) c.π

Tactic:
simpa [coneΓ, ← ΓHomEquiv_naturality_left_symm, Equiv.symm_apply_eq] using hf

Premises used: CategoryTheory.Sheaf.ΓHomEquiv_naturality_left_symm, Equiv.symm_apply_eq, CategoryTheory.Sheaf.coneΓ