mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right ≫ F₃.map (Under.Hom.right φ)) =
    curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right)

Tactic:
← f.naturality φ.right,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ (F₁ ⊗ F₂).map (Under.Hom.right φ) ≫ f.app k₂.right) =
    curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (expComparison F A).natTrans
⊢ IsIso (frobeniusMorphism F h A).natTrans

Tactic:
← frobeniusMorphism_mate F h

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i :
  IsIso
    ((conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (frobeniusMorphism F h A).natTrans)
⊢ IsIso (frobeniusMorphism F h A).natTrans
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso (expComparison F A).natTrans

Tactic:
← frobeniusMorphism_mate F h

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso
    ((conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (frobeniusMorphism F h A).natTrans)
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ prod.fst = prod.snd

Tactic:
simp [← cancel_epi (diag A)]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
f₃ : X₃✝ ⟶ Y₃✝
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁✝ Y₂✝ Y₃✝).hom = (α_ X₁✝ X₂✝ X₃✝).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)

Tactic:
by
      apply Functor.Faithful.map_injective (F := ι C V D)
      simp only [Functor.map_comp, ι_map_associator_hom_eq_associator_hom,
        ι_map_tensorHom_hom_eq_tensorHom]
      exact DayConvolution.associator_naturality
        ((ι C V D).map f₁) ((ι C V D).map f₂) ((ι C V D).map f₃)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : R ∈ K.coverings X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
⊢ P X

Tactic:
rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR
    obtain ⟨𝒰, rfl⟩ := hR
    rw [H 𝒰]
    intro i
    exact h ⟨i⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
⊢ Hom.right (f ≫ π f) - Hom.right 0 = biprod.inr ≫ (cokernel f).hom

Tactic:
simp [π]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ ∑ x, ∑ j, (f i✝ j ≫ g j x) ≫ h x j✝ = ∑ x, f i✝ x ≫ ∑ j, g x j ≫ h j j✝

Tactic:
comp_sum,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ ∑ x, ∑ j, (f i✝ j ≫ g j x) ≫ h x j✝ = ∑ x, ∑ j, f i✝ x ≫ g x j ≫ h j j✝
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
f : Arrow J
hf : f ∈ (MorphismProperty.ofHoms fun x ↦ 𝟙 j).toSet
⊢ ∃ a, (fun x ↦ ⟨Arrow.mk (𝟙 j), ⋯⟩) a = ⟨f, hf⟩

Tactic:
refine ⟨⟨⟩, ?_⟩

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
f : Arrow J
hf : f ∈ (MorphismProperty.ofHoms fun x ↦ 𝟙 j).toSet
⊢ (fun x ↦ ⟨Arrow.mk (𝟙 j), ⋯⟩) PUnit.unit = ⟨f, hf⟩
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
this :
  ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → ↑(transfiniteIterate (φ Y m) j A)),
    HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
K : Type w
f : K → ↑(⋃ j, transfiniteIterate (φ Y m) j A)
hK : HasCardinalLT K κ₁
⊢ ∃ j, ∀ (k : K), f k ≤ j

Tactic:
have (k : K) : ∃ (j : κ₁.ord.ToType), (f k).val ∈ transfiniteIterate (φ Y m) j A := by
      simpa only [Set.mem_iUnion] using (f k).prop

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
this✝ :
  ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → ↑(transfiniteIterate (φ Y m) j A)),
    HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
K : Type w
f : K → ↑(⋃ j, transfiniteIterate (φ Y m) j A)
hK : HasCardinalLT K κ₁
this : ∀ (k : K), ∃ j, ↑(f k) ∈ transfiniteIterate (φ Y m) j A
⊢ ∃ j, ∀ (k : K), f k ≤ j
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
simp only [coherentTopology, Presieve.isSheaf_coverage] at hP

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C}, ∀ R ∈ (coherentCoverage C).coverings X, Presieve.IsSheafFor P R
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C}, ∀ R ∈ (coherentCoverage C).coverings X, Presieve.IsSheafFor P R
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
apply hP

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C}, ∀ R ∈ (coherentCoverage C).coverings X, Presieve.IsSheafFor P R
⊢ Presieve.ofArrows X π ∈ (coherentCoverage C).coverings B
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ ∀ {X : C}, ∀ R ∈ (coherentCoverage C).coverings X, Presieve.IsSheafFor P R

Tactic:
rintro B S ⟨α, _, X, π, rfl, hS⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
B : C
α : Type
w✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
hS : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ EffectiveEpi (π' ≫ π)

Tactic:
rw [effectiveEpi_iff_effectiveEpiFamily, ← Sieve.effectiveEpimorphic_family]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π).EffectiveEpimorphic
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Tactic:
rw [Presieve.isSheaf_iff_preservesFiniteProducts] at h

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : PreservesFiniteProducts (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))

Tactic:
refine ⟨(IsLimit.equivIsoLimit (ForkOfι.ext ?_ _ h)) ?_⟩

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ P.map (F.map π).op ≫ (F.op ⋙ P).map c.fst.op = P.map (F.map π).op ≫ (F.op ⋙ P).map c.snd.op

case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ IsLimit (Fork.ofι (P.map (F.map π).op) ?refine_1)
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h : Presheaf.imageSieve f x ∈ (extensiveTopology C) X
⊢ ∃ a, (ConcreteCategory.hom (f.app (op X))) a = x

Tactic:
mem_sieves_iff_contains_colimit_cofan

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h :
  ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
⊢ ∃ a, (ConcreteCategory.hom (f.app (op X))) a = x
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : PreservesFiniteLimits s
hF : IsSheaf (coherentTopology C) F
⊢ IsSheaf (coherentTopology C) (F ⋙ s)

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

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : IsSheaf (coherentTopology C) (F ⋙ s)
⊢ IsSheaf (coherentTopology C) F

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

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj.obj (op X)
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).hom.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op n)).obj.map φ.op)) y

Tactic:
have := hF n
  rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff] at this
  exact this X y

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
h : Presheaf.IsLocallySurjective (coherentTopology C) f
U✝ : C
y : ToType (G.obj (op U✝))
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝

Tactic:
by
    replace h := h.1 y
    rw [coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily] at h
    obtain ⟨α, _, Z, π, h, h'⟩ := h
    rw [mem_sieves_iff_hasEffectiveEpi]
    let x : (a : α) → (F.obj ⟨Z a⟩) := fun a ↦ (h' a).choose
    let i' : ((a : α) → (F.obj ⟨Z a⟩)) ≅ (F.obj ⟨∐ Z⟩) := (Types.productIso _).symm ≪≫
      (PreservesProduct.iso F _).symm ≪≫ F.mapIso (opCoproductIsoProduct _).symm
    refine ⟨∐ Z, Sigma.desc π, inferInstance, i'.hom x, ?_⟩
    have := preservesLimitsOfShape_of_equiv (Discrete.opposite α).symm G
    apply Concrete.isLimit_ext _ (isLimitOfPreserves G (coproductIsCoproduct Z).op)
    intro ⟨⟨a⟩⟩
    simp only [Functor.comp_obj, Functor.op_obj, Discrete.functor_obj_eq_as, Functor.mapCone_pt,
      Cocone.op_pt, Cofan.mk_pt, Functor.const_obj_obj, Functor.mapCone_π_app, Cocone.op_π,
      NatTrans.op_app, Cofan.mk_ι_app, Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom,
      Functor.mapIso_inv, comp_apply, ← f.naturality_apply (Sigma.ι Z a).op, i']
    have : f.app ⟨Z a⟩ (x a) = G.map (π a).op y := (h' a).choose_spec
    convert! this
    · rw [← Functor.map_comp_apply, opCoproductIsoProduct_inv_comp_ι, ← piComparison_comp_π]
      change ((PreservesProduct.iso F _).hom ≫ _) _ = _
      have := Types.productIso_hom_comp_eval (fun a ↦ F.obj (op (Z a))) a
      rw [← Iso.eq_inv_comp] at this
      simp only [types_comp_apply, Iso.inv_hom_id_apply]
      simp [← comp_apply]
    · simp only [← Functor.map_comp_apply, ← op_comp, Sigma.ι_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : WalkingParallelPair ⥤ D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
⊢ IsLimit (Fork.ofι (P.map π.op) ⋯) ≃ IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)

Tactic:
let H := parallelPair fst.op snd.op

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : WalkingParallelPair ⥤ D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
⊢ IsLimit (Fork.ofι (P.map π.op) ⋯) ≃ IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ SingleEqualizerCondition P π ↔ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op))

Tactic:
constructor
  · intro h
    exact ⟨isLimit_forkOfι_equiv _ _ _ (pullbackIsPullback π π) (h _ (pullbackIsPullback π π)).some⟩
  · intro ⟨h⟩
    exact fun c hc ↦ ⟨(isLimit_forkOfι_equiv _ _ _ hc).symm h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f (𝒰.f i))
⊢ 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst f (𝒰.f i)) ⋯ ≫ f = 𝟙 Y

Tactic:
· exact 𝒰.hom_ext fun i ↦ by simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
h : Z ⟶ X
w : f ≫ g = h
α : (presheafHom F G).obj (op X)
⊢ ((ConcreteCategory.hom ((presheafHom F G).map g.op)) α).app (op (Over.mk f)) = α.app (op (Over.mk h))

Tactic:
subst w
  rfl

Goal state after: