mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
⊢ ∀ ⦃f : V ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
      (coherentCoverage C).Saturate V
        (Sieve.pullback f
          (Sieve.generate
            (Presieve.ofArrows
              (fun x ↦
                match x with
                | ⟨a, b⟩ => Y_n a b)
              fun x ↦
              match x with
              | ⟨a, b⟩ => π_n a b ≫ π a)))

Tactic:
f

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
⊢ (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
    (coherentCoverage C).Saturate V
      (Sieve.pullback f
        (Sieve.generate
          (Presieve.ofArrows
            (fun x ↦
              match x with
              | ⟨a, b⟩ => Y_n a b)
            fun x ↦
            match x with
            | ⟨a, b⟩ => π_n a b ≫ π a)))
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 : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
⊢ Presieve.ofArrows (fun x ↦ Y) (fun x ↦ π) g → ∃ W_1 i e, S.arrows e ∧ i ≫ e = g

Tactic:
f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun x ↦ Y) (fun x ↦ π) g
⊢ ∃ W_1 i e, S.arrows e ∧ i ≫ e = g
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case a
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 π'
V : C
⊢ ∀ ⦃f : V ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π)).arrows f →
      (regularCoverage C).Saturate V (Sieve.pullback f (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)))

Tactic:
f

Goal state after:
case a
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 π'
V : C
f : V ⟶ X
⊢ (Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π)).arrows f →
    (regularCoverage C).Saturate V (Sieve.pullback f (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)))
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.of.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Tactic:
have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using! h'
        exact ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ P.map π.op ≫ P.map (pullback.fst π π).op = P.map π.op ≫ P.map (pullback.snd π π).op

Tactic:
simp only [← Functor.map_comp, ← op_comp, pullback.condition]

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

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
hF :
  ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).coverings X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Y X : C
⊢ ∀ (π : Y ⟶ X) [EffectiveEpi π], SingleEqualizerCondition F π

Tactic:
f

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
hF :
  ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).coverings X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Y X : C
f : Y ⟶ X
⊢ ∀ [EffectiveEpi f], SingleEqualizerCondition F f
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M : ↑(F.obj { as := op S }).obj
i₁ i₂ i₃ : ι
⊢ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M) ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).r.toFunctor.map
          ((F.map (f i₂).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M))) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M) ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.1 ((F.map (f i₃).op.toLoc).l.toFunctor.obj M)))

Tactic:
rw [← Functor.map_comp, ← Functor.map_comp, Adj.unit_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)
hom_self : ∀ (i : ι), pullHom' hom (f i) (𝟙 (X i)) (𝟙 (X i)) ⋯ ⋯ = 𝟙 ((F.map (𝟙 (X i)).op.toLoc).toFunctor.obj (obj i))
Y : C
q : Y ⟶ S
i : ι
g : Y ⟶ X i
hg : g ≫ f i = q
⊢ pullHom' hom q g g hg hg = 𝟙 ((F.map g.op.toLoc).toFunctor.obj (obj i))

Tactic:
simp [← pullHom_pullHom' hom g (f i) q (𝟙 (X i)) (𝟙 (X i)) g g hg, hom_self, pullHom]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
⊢ pullback.snd (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫ F.p₂ p.snd =
    ((cylinderHom f g).comp g).h₀ p

Tactic:
by
    have : g.h₀ p.fst = pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) (by simp) ≫
        pullback.snd (F.f _) (F.f _) := by simp
    dsimp only [cylinder_X, Hom.comp_s₀, cylinder_I₀, Function.comp_apply, cylinderHom_s₀,
      Hom.comp_h₀, cylinderHom_h₀]
    nth_rw 3 [this]
    rw [pullback.condition_assoc]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
q' : Y ⟶ S
f₁' : Y ⟶ X (α j₁)
f₂' : Y ⟶ X (α j₂)
hf₁ : autoParam (f₁ ≫ f' j₁ = q) pullFunctorObjHom_eq._auto_1
hf₂ : autoParam (f₂ ≫ f' j₂ = q) pullFunctorObjHom_eq._auto_3
hq' : autoParam (q ≫ p = q') pullFunctorObjHom_eq._auto_5
hf₁' : autoParam (f₁ ≫ p' j₁ = f₁') pullFunctorObjHom_eq._auto_7
hf₂' : autoParam (f₂ ≫ p' j₂ = f₂') pullFunctorObjHom_eq._auto_9
⊢ f₂' ≫ f (α j₂) = q ≫ p

Tactic:
← hf₂',

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
q' : Y ⟶ S
f₁' : Y ⟶ X (α j₁)
f₂' : Y ⟶ X (α j₂)
hf₁ : autoParam (f₁ ≫ f' j₁ = q) pullFunctorObjHom_eq._auto_1
hf₂ : autoParam (f₂ ≫ f' j₂ = q) pullFunctorObjHom_eq._auto_3
hq' : autoParam (q ≫ p = q') pullFunctorObjHom_eq._auto_5
hf₁' : autoParam (f₁ ≫ p' j₁ = f₁') pullFunctorObjHom_eq._auto_7
hf₂' : autoParam (f₂ ≫ p' j₂ = f₂') pullFunctorObjHom_eq._auto_9
⊢ (f₂ ≫ p' j₂) ≫ f (α j₂) = q ≫ p
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 : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows (𝟙 Y ≫ g)

Tactic:
simpa using hg

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
x✝ : Cᵒᵖ ⥤ A
⊢ (ρ_ (Φ.presheafFiber.obj x✝)).inv =
    Φ.presheafFiber.map (ρ_ x✝).inv ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x x✝ ⊗ₘ Φ.toPresheafFiber X x (𝟙_ (Cᵒᵖ ⥤ A))) ⋯ ≫
        Φ.presheafFiber.obj x✝ ◁ Φ.presheafFiberDesc (fun x x_1 ↦ 𝟙 ((𝟙_ (Cᵒᵖ ⥤ A)).obj (Opposite.op x))) ⋯

Tactic:
ext
    simp [tensorHom_def, ← MonoidalCategory.whiskerLeft_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
⊢ ∀ ⦃i₁ i₂ : ι'⦄ (f₁ : Y ⟶ X' i₁) (f₂ : Y ⟶ X' i₂) (hf₁ : f₁ ≫ f' i₁ = q) (hf₂ : f₂ ≫ f' i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' i₁ ≫ f (α i₁)) (p' i₁) (p'' i₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' i₂ ≫ f (α i₂)) (p' i₂) (p'' i₂) ⋯ ⋯).hom

Tactic:
j₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ : ι'
⊢ ∀ ⦃i₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' i₂) (hf₁ : f₁ ≫ f' j₁ = q) (hf₂ : f₂ ≫ f' i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' i₂ ≫ f (α i₂)) (p' i₂) (p'' i₂) ⋯ ⋯).hom
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ ∃ i y_1, (ConcreteCategory.hom (Φ.obj.fiber.map (g i))) y_1 = y

Tactic:
obtain ⟨T, a, ⟨_, b, _, ⟨i⟩, hb⟩, ⟨z, hz₁⟩, hz₂⟩ := hS (⟨_, ⟨⟨Φ, Φ.obj.fiber.map f y⟩⟩⟩)
      (⟨by exact y, by rw [FunctorToTypes.mem_fromOverSubfunctor_iff]; rfl⟩)

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y✝ : C
f : Y✝ ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
T : Over X
a : T ⟶ Over.mk f
Y : C
i : ι
b : (Over.forget X).obj T ⟶ Z i
hb : b ≫ g i = (Over.forget X).map a
z : (Over.forget X ⋙ ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber).obj T
hz₁ :
  z ∈
    (FunctorToTypes.fromOverSubfunctor ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber
          ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd).obj
      T
hz₂ :
  (ConcreteCategory.hom
        ({
                  obj :=
                    ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.over
                      ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd,
                  property := ⋯ }.obj.fiber.map
          a))
      ⟨z, hz₁⟩ =
    ⟨y, ⋯⟩
⊢ ∃ i y_1, (ConcreteCategory.hom (Φ.obj.fiber.map (g i))) y_1 = y
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
⊢ ∀ ⦃f : β ⟶ α⦄,
    discretePresieve α f →
      (ConcreteCategory.hom (S.map f.op)) (typesGlue S hs α ⇑(ConcreteCategory.hom (eval S α s))) =
        (ConcreteCategory.hom (S.map f.op)) s

Tactic:
f

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
⊢ discretePresieve α f →
    (ConcreteCategory.hom (S.map f.op)) (typesGlue S hs α ⇑(ConcreteCategory.hom (eval S α s))) =
      (ConcreteCategory.hom (S.map f.op)) s
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
inst✝ : Finite ι
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
⊢ G.IsFinite

Tactic:
by
  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
  exact ⟨Fin n, inferInstance, _, _, ⟨h.of_equiv e.symm⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
p : M ⟶ M'
S : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.map (MonCat.Hom.hom (p.app U✝)) (S.obj U✝) ≤
    Submonoid.comap (MonCat.Hom.hom (M'.map i)) (Submonoid.map (MonCat.Hom.hom (p.app V✝)) (S.obj V✝))

Tactic:
rw [← Submonoid.map_le_iff_le_comap, Submonoid.map_map, ← MonCat.hom_comp, ← p.naturality,
      MonCat.hom_comp, ← Submonoid.map_map]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
p : M ⟶ M'
S : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.map (MonCat.Hom.hom (p.app V✝)) (Submonoid.map (MonCat.Hom.hom (M.map i)) (S.obj U✝)) ≤
    Submonoid.map (MonCat.Hom.hom (p.app V✝)) (S.obj V✝)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M N : ↑(F.obj { as := op S })
φ : M ⟶ N
⊢ (subtypeCompatibleHomEquiv F f)
      (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun i ↦ Over.homMk (f i) ⋯) (F.presheafHomObjHomEquiv φ)) =
    (F.toDescentData f).map φ

Tactic:
by
  ext i
  simp [subtypeCompatibleHomEquiv, presheafHomObjHomEquiv, pullHom,
    ← Functor.map_comp, Pseudofunctor.mapComp'_id_comp_hom_app_assoc,
    Pseudofunctor.mapComp'_id_comp_inv_app]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
Y : Over S₀
⊢ ∀ (f : Y ⟶ Over.mk a),
    ((Sieve.overEquiv (Over.mk a)).symm R).arrows f →
      (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
            (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
        f

Tactic:
f

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
Y : Over S₀
f : Y ⟶ Over.mk a
⊢ ((Sieve.overEquiv (Over.mk a)).symm R).arrows f →
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
          (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
      f
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
Y Z : C
⊢ ∀ {f : Y ⟶ Opposite.unop X},
    (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
      ∀ (g : Z ⟶ Y), ∃ a, (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) a

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
⊢ (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
    ∀ (g : Z ⟶ Y), ∃ a, (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) a
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
⊢ ∀ (f : Y ⟶ Opposite.unop X),
    J.Covers ((ConcreteCategory.hom ((χ m).app X)) x) f → ((ConcreteCategory.hom ((χ m).app X)) x).arrows f

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
⊢ J.Covers ((ConcreteCategory.hom ((χ m).app X)) x) f → ((ConcreteCategory.hom ((χ m).app X)) x).arrows f
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
⊢ (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) (⋯.amalgamate a ⋯)

Tactic:
refine (hG _ hf).ext fun Z f' hf' => ?_

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
Z : C
f' : Z ⟶ Y
hf' :
  (Sieve.pullback f
        ((ConcreteCategory.hom
            (↾fun x ↦
              {
                arrows := fun Y f ↦
                  ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                downward_closed := ⋯ }))
          x)).arrows
    f'
⊢ (ConcreteCategory.hom (G.map f'.op)) ((ConcreteCategory.hom (G.map f.op)) x) =
    (ConcreteCategory.hom (G.map f'.op)) ((ConcreteCategory.hom (m.app (Opposite.op Y))) (⋯.amalgamate a ⋯))
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
      ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom =
    (Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)).hom ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝

Tactic:
by ext; apply biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
      ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom =
    (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)).hom ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝

Tactic:
by ext; apply biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply

Goal state after: