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

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd) ⋯

Tactic:
·

Goal state after:
case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd) ⋯
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case refine_3.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m ≫ F.obj.map (WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄).op =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        ⋯ ≫
      F.obj.map (WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄).op

pp: case refine_3.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m ≫ F.obj.map (WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄).op =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        ⋯ ≫
      F.obj.map (WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄).op

Tactic:
·

Goal state after:
case refine_3.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m ≫ F.obj.map (WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄).op =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        ⋯ ≫
      F.obj.map (WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄).op
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case refine_3.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m ≫ F.obj.map (WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄).op =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        ⋯ ≫
      F.obj.map (WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄).op

Tactic:
·

Goal state after:
case refine_3.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m ≫ F.obj.map (WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄).op =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        ⋯ ≫
      F.obj.map (WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄).op
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case hex
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
⊢ ∃ x_1, x.IsAmalgamation x_1

pp: case hunique
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₁ y₂ : (presheafHom F G).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Tactic:
·

Goal state after:
case hex
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
⊢ ∃ x_1, x.IsAmalgamation x_1
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case hunique
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₁ y₂ : (presheafHom F G).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Tactic:
·

Goal state after:
case hunique
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₁ y₂ : (presheafHom F G).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: case refine_1
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
⊢ ∀ (d : (fiber p).Elements), ∃ c, Nonempty ((functor p).obj c ⟶ d)

pp: case refine_2
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
⊢ ∀ {d : (fiber p).Elements} {c : N} (s s' : (functor p).obj c ⟶ d),
    ∃ c' t, (functor p).map t ≫ s = (functor p).map t ≫ s'

Tactic:
·

Goal state after:
case refine_1
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
⊢ ∀ (d : (fiber p).Elements), ∃ c, Nonempty ((functor p).obj c ⟶ d)
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: case refine_2
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
⊢ ∀ {d : (fiber p).Elements} {c : N} (s s' : (functor p).obj c ⟶ d),
    ∃ c' t, (functor p).map t ≫ s = (functor p).map t ≫ s'

Tactic:
·

Goal state after:
case refine_2
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
⊢ ∀ {d : (fiber p).Elements} {c : N} (s s' : (functor p).obj c ⟶ d),
    ∃ c' t, (functor p).map t ≫ s = (functor p).map t ≫ s'
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSeparatedFor F S.arrows

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ ∀ (x : Presieve.FamilyOfElements F S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSeparatedFor F S.arrows
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ ∀ (x : Presieve.FamilyOfElements F S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ ∀ (x : Presieve.FamilyOfElements F S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ K.toGrothendieck ≤ J

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ J ≤ K.toGrothendieck

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ K.toGrothendieck ≤ J
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ J ≤ K.toGrothendieck

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ J ≤ K.toGrothendieck
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
h : K.Generates J
⊢ K.toGrothendieck = J

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
⊢ K.toGrothendieck = J → K.Generates J

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
h : K.Generates J
⊢ K.toGrothendieck = J
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
⊢ K.toGrothendieck = J → K.Generates J

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
⊢ K.toGrothendieck = J → K.Generates J
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
α : Type u
s : S₁.obj.obj (op α)
x : α
⊢ (ConcreteCategory.hom
          ((ConcreteCategory.hom ((equivYoneda S₂.obj ⋯).hom.app (op α)))
            ((ConcreteCategory.hom (f.hom.app (op α))) s))).toFun
      x =
    (ConcreteCategory.hom
          ((ConcreteCategory.hom ((equivYoneda S₁.obj ⋯).hom.app (op α))) s ≫ f.hom.app (op PUnit.{u + 1}))).toFun
      x

Tactic:
exact eval_app S₁ S₂ f α s x

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'
S : Set (SubmonoidFunctor M)
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ ⨅ F ∈ S, F.obj U✝ ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (⨅ F ∈ S, F.obj V✝)

Tactic:
(Submonoid.gc_map_comap (M.map f).hom).u_iInf₂

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'
S : Set (SubmonoidFunctor M)
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ ⨅ F ∈ S, F.obj U✝ ≤ ⨅ i ∈ S, Submonoid.comap (MonCat.Hom.hom (M.map f)) (i.obj V✝)
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: 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

pp: 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

Tactic:
·

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
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: 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

Tactic:
·

Goal state after:
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.Subobject.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾(pullback (x✝¹ ≫ x✝).unop).obj = ↾(pullback x✝¹.unop).obj ≫ ↾(pullback x✝.unop).obj

Tactic:
by ext : 3; simp [pullback_comp]

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

Goal state before:
pp: case e'_2.refine_1
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 })
⊢ ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows ≤
    Presieve.ofArrows (fun i ↦ Over.mk i.obj.hom) fun i ↦ Over.homMk i.obj.hom ⋯

pp: case e'_2.refine_2
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 })
⊢ (Presieve.ofArrows (fun i ↦ Over.mk i.obj.hom) fun i ↦ Over.homMk i.obj.hom ⋯) ≤
    ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows

Tactic:
·

Goal state after:
case e'_2.refine_1
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 })
⊢ ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows ≤
    Presieve.ofArrows (fun i ↦ Over.mk i.obj.hom) fun i ↦ Over.homMk i.obj.hom ⋯
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case e'_2.refine_2
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 })
⊢ (Presieve.ofArrows (fun i ↦ Over.mk i.obj.hom) fun i ↦ Over.homMk i.obj.hom ⋯) ≤
    ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows

Tactic:
·

Goal state after:
case e'_2.refine_2
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 })
⊢ (Presieve.ofArrows (fun i ↦ Over.mk i.obj.hom) fun i ↦ Over.homMk i.obj.hom ⋯) ≤
    ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows
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
⊢ (Sieve.overEquiv (Over.mk a)).symm R ≤
    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))

pp: case refine_2
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
⊢ 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)) ≤
    (Sieve.overEquiv (Over.mk a)).symm R

Tactic:
·

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
⊢ (Sieve.overEquiv (Over.mk a)).symm R ≤
    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))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case refine_2
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
⊢ 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)) ≤
    (Sieve.overEquiv (Over.mk a)).symm R

Tactic:
·

Goal state after:
case refine_2
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
⊢ 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)) ≤
    (Sieve.overEquiv (Over.mk a)).symm R
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:
intro Y Z f ⟨a, ha⟩ g

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 : (fun X ↦ X) (F.obj (Opposite.op Y))
ha : (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.Subobject.Classifier.Defs

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

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

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
h : HasSubobjectClassifier C
⊢ (Subobject.presheaf C).IsRepresentable
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
h : (Subobject.presheaf C).IsRepresentable
⊢ HasSubobjectClassifier C

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
h : (Subobject.presheaf C).IsRepresentable
⊢ HasSubobjectClassifier C
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₁ y₁ : (fun X ↦ X) (F.obj X)),
    (ConcreteCategory.hom (m.app X)) x₁ = (ConcreteCategory.hom (m.app X)) y₁ ∧
        (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ =
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) y₁ →
      x₁ = y₁

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
    (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
      ∃ x₁,
        (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₁ y₁ : (fun X ↦ X) (F.obj X)),
    (ConcreteCategory.hom (m.app X)) x₁ = (ConcreteCategory.hom (m.app X)) y₁ ∧
        (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ =
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) y₁ →
      x₁ = y₁