mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ x.IsAmalgamation y ↔
    ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
constructor

Goal state after:
case mp
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ x.IsAmalgamation y →
    ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))

case mpr
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ (∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))) →
    x.IsAmalgamation y
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ S.toPullbackObj P x = S.toPullbackObj P y

Tactic:
ext

Goal state after:
case fst
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ (↑(S.toPullbackObj P x)).1 = (↑(S.toPullbackObj P y)).1

case snd
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ (↑(S.toPullbackObj P x)).2 = (↑(S.toPullbackObj P y)).2
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝² x✝¹ x✝ : OneCochain G U
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁷ x✝⁶ x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁷ * x✝⁶ * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = (x✝⁷ * (x✝⁶ * x✝⁵)).ev x✝⁴ x✝³ x✝¹ x✝
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝² x✝¹ x✝ : OneCochain G U
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
by ext; apply mul_assoc

Goal state after:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝ : OneCochain G U
⊢ 1 * x✝ = x✝

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (1 * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = x✝⁵.ev x✝⁴ x✝³ x✝¹ x✝
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝ : OneCochain G U
⊢ x✝ * 1 = x✝

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁵ * 1).ev x✝⁴ x✝³ x✝¹ x✝ = x✝⁵.ev x✝⁴ x✝³ x✝¹ x✝
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝ : OneCochain G U
⊢ x✝⁻¹ * x✝ = 1

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁵⁻¹ * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = ev 1 x✝⁴ x✝³ x✝¹ x✝
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
⊢ ∀ {x y : OneCocycle G U}, x.IsCohomologous y → y.IsCohomologous x

Tactic:
rintro γ₁ γ₂ ⟨α, h⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂.toOneCochain α
⊢ γ₂.IsCohomologous γ₁
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✝ Y✝ : Cᵒᵖ ⥤ A
x✝¹ : X✝ ⟶ Y✝
x✝ : Cᵒᵖ ⥤ A
⊢ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x X✝ ⊗ₘ Φ.toPresheafFiber X x x✝) ⋯ ≫
      Φ.presheafFiber.map x✝¹ ▷ Φ.presheafFiber.obj x✝ =
    Φ.presheafFiber.map (x✝¹ ▷ x✝) ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x Y✝ ⊗ₘ Φ.toPresheafFiber X x x✝) ⋯

Tactic:
ext

Goal state after:
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✝¹ Y✝ : Cᵒᵖ ⥤ A
x✝² : X✝¹ ⟶ Y✝
x✝¹ : Cᵒᵖ ⥤ A
X✝ : C
x✝ : Φ.fiber.obj X✝
⊢ Φ.toPresheafFiber X✝ x✝ (X✝¹ ⊗ x✝¹) ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x X✝¹ ⊗ₘ Φ.toPresheafFiber X x x✝¹) ⋯ ≫
        Φ.presheafFiber.map x✝² ▷ Φ.presheafFiber.obj x✝¹ =
    Φ.toPresheafFiber X✝ x✝ (X✝¹ ⊗ x✝¹) ≫
      Φ.presheafFiber.map (x✝² ▷ x✝¹) ≫
        Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x Y✝ ⊗ₘ Φ.toPresheafFiber X x x✝¹) ⋯
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✝ Y✝ P : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P ⊗ₘ Φ.toPresheafFiber X x X✝) ⋯ ≫
      Φ.presheafFiber.obj P ◁ Φ.presheafFiber.map f =
    Φ.presheafFiber.map (P ◁ f) ≫ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P ⊗ₘ Φ.toPresheafFiber X x Y✝) ⋯

Tactic:
ext

Goal state after:
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✝¹ Y✝ P : Cᵒᵖ ⥤ A
f : X✝¹ ⟶ Y✝
X✝ : C
x✝ : Φ.fiber.obj X✝
⊢ Φ.toPresheafFiber X✝ x✝ (P ⊗ X✝¹) ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P ⊗ₘ Φ.toPresheafFiber X x X✝¹) ⋯ ≫
        Φ.presheafFiber.obj P ◁ Φ.presheafFiber.map f =
    Φ.toPresheafFiber X✝ x✝ (P ⊗ X✝¹) ≫
      Φ.presheafFiber.map (P ◁ f) ≫
        Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P ⊗ₘ Φ.toPresheafFiber X x Y✝) ⋯
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 (𝟙_ (Cᵒᵖ ⥤ A)) ⊗ₘ Φ.toPresheafFiber X x x✝) ⋯ ≫
        Φ.presheafFiberDesc (fun x x_1 ↦ 𝟙 ((𝟙_ (Cᵒᵖ ⥤ A)).obj (Opposite.op x))) ⋯ ▷ Φ.presheafFiber.obj x✝

Tactic:
ext

Goal state after:
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
X✝ : C
x✝ : Φ.fiber.obj X✝
⊢ Φ.toPresheafFiber X✝ x✝ x✝¹ ≫ (λ_ (Φ.presheafFiber.obj x✝¹)).inv =
    Φ.toPresheafFiber X✝ x✝ x✝¹ ≫
      Φ.presheafFiber.map (λ_ x✝¹).inv ≫
        Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x (𝟙_ (Cᵒᵖ ⥤ A)) ⊗ₘ Φ.toPresheafFiber X x x✝¹) ⋯ ≫
          Φ.presheafFiberDesc (fun x x_1 ↦ 𝟙 ((𝟙_ (Cᵒᵖ ⥤ A)).obj (Opposite.op x))) ⋯ ▷ Φ.presheafFiber.obj x✝¹
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

Goal state after:
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
X✝ : C
x✝ : Φ.fiber.obj X✝
⊢ Φ.toPresheafFiber X✝ x✝ x✝¹ ≫ (ρ_ (Φ.presheafFiber.obj x✝¹)).inv =
    Φ.toPresheafFiber X✝ x✝ x✝¹ ≫
      Φ.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))) ⋯
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
inst✝ : IsCofiltered N
U : N
X : C
f₁ f₂ : p.obj U ⟶ X
hf : fiberMk f₁ = fiberMk f₂
V : Nᵒᵖ
g : op U ⟶ V
hg :
  (hom ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).map g)) (shrinkYonedaObjObjEquiv.symm f₁) =
    (hom ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).map g)) (shrinkYonedaObjObjEquiv.symm f₂)
⊢ p.map g.unop ≫ f₁ = p.map g.unop ≫ f₂

Tactic:
simpa [shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}] using hg

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, a ≫ g = p.map q ≫ f
X : C
R : Sieve X
hR : R ∈ J X
x : (ofIsCofiltered.fiber p).obj X
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (hom ((ofIsCofiltered.fiber p).map f)) y = x

Tactic:
by
    obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x
    obtain ⟨Y, g, hg, V, q, a, ha⟩ := hp R hR f
    exact ⟨Y, g, hg, fiberMk a, by simp [ha]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x✝ : F.obj (Opposite.op X)
Z✝ : C
R✝ : Presieve Z✝
hR : R✝ ∈ K.coverings Z✝
y✝ : Presieve.FamilyOfElements F R✝
hy : y✝.Compatible
hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), K.SubsheafClosure 𝒮 W (y✝ r hr)
t✝ : F.obj (Opposite.op Z✝)
ht : y✝.IsAmalgamation t✝
x : ⦃W : C⦄ → (r : W ⟶ Z✝) → R✝ r → Witness K ι W
hx : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), Witness.eval hF ι t (x r hr) = some (y✝ r hr)
⊢ Witness.eval hF ι t (Witness.amalgamate hR x) = some t✝

Tactic:
simp [Witness.eval, hx]; grind

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
x y : { x // K.SubsheafClosure 𝒮 X x }
hxy : (fun x ↦ i ↑x ⋯) x = (fun x ↦ i ↑x ⋯) y
⊢ x = y

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := ⋯
t : (X : C) → ι X → F.obj (Opposite.op X) := ⋯
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
x y : { x // K.SubsheafClosure 𝒮 X x }
hxy : (fun x ↦ i ↑x ⋯) x = (fun x ↦ i ↑x ⋯) y
⊢ ↑x = ↑y
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α : Type u
x✝ : α ⟶ S.obj (op PUnit.{u + 1})
⊢ eval S α ((fun f ↦ typesGlue S ⋯ α ⇑(ConcreteCategory.hom f)) x✝) = x✝

Tactic:
ext

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α : Type u
x✝¹ : α ⟶ S.obj (op PUnit.{u + 1})
x✝ : α
⊢ (ConcreteCategory.hom (eval S α ((fun f ↦ typesGlue S ⋯ α ⇑(ConcreteCategory.hom f)) x✝¹))).toFun x✝ =
    (ConcreteCategory.hom x✝¹).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
⊢ S.map f ≫ (evalEquiv S hs (unop β)).toIso.hom = (evalEquiv S hs (unop α)).toIso.hom ≫ ↾fun g ↦ f.unop ≫ g

Tactic:
ext

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
x✝¹ : S.obj α
x✝ : unop β
⊢ (ConcreteCategory.hom ((ConcreteCategory.hom (S.map f ≫ (evalEquiv S hs (unop β)).toIso.hom)).toFun x✝¹)).toFun x✝ =
    (ConcreteCategory.hom
          ((ConcreteCategory.hom ((evalEquiv S hs (unop α)).toIso.hom ≫ ↾fun g ↦ f.unop ≫ g)).toFun x✝¹)).toFun
      x✝
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

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

Tactic:
Submonoid.map_le_iff_le_comap,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
M : C ⥤ MonCat
S : SubmonoidFunctor M
U V : C
f : U ⟶ V
⊢ S.obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (S.obj V)
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B ↔
    A ≤ B

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B →
    A ≤ B

case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ A ≤ B →
    { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ f = Over.homMk g ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ Over.Hom.left f = Over.Hom.left (Over.homMk g ⋯)
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
⊢ HasSubobjectClassifier C ↔ (Subobject.presheaf C).IsRepresentable

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
⊢ HasSubobjectClassifier C → (Subobject.presheaf C).IsRepresentable

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
⊢ (Subobject.presheaf C).IsRepresentable → HasSubobjectClassifier C
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
⊢ m ≫ χ m = (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F ≫ truth C

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
x✝¹ : Cᵒᵖ
x✝ : F.obj x✝¹
⊢ (ConcreteCategory.hom ((m ≫ χ m).app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F ≫ truth C).app x✝¹)).toFun x✝
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
Ω : C
h : (Subobject.presheaf C).RepresentableBy Ω
⊢ HasSubobjectClassifier C

Tactic:
constructor

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
Ω : C
h : (Subobject.presheaf C).RepresentableBy Ω
⊢ Nonempty (Subobject.Classifier C)
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
Ω : C
h : (Subobject.presheaf C).RepresentableBy Ω
⊢ Nonempty (Subobject.Classifier C)

Tactic:
constructor

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
Ω : C
h : (Subobject.presheaf C).RepresentableBy Ω
⊢ Subobject.Classifier C
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ IsPullback m (e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)))
    (e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))) (e.functor.map 𝒞₁.truth)

Tactic:
by
    apply ((𝒞₁.isPullback (e.inverse.map m)).map e.functor).of_iso (e.counitIso.app _)
      (e.counitIso.app _) (.refl _) (.refl _) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
⊢ IsPullback (e.inverse.map m) (e.inverse.map χ₀' ≫ e.unitInv.app 𝒞₁.Ω₀) (e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω)
    𝒞₁.truth

Tactic:
exact (hχ'.map e.inverse).paste_vert <| IsPullback.of_vert_isIso_mono .mk

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 : ℕ
y : ↑(F.H' n S.X₄)
⊢ ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
      ((ConcreteCategory.hom
          (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
        y) =
    ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
      ((ConcreteCategory.hom
          (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
        ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
          (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))

Tactic:
ext

Goal state after:
case fst
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 : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).1 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).1

case snd
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 : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).2 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).2