mathlib-initiative/mathlib-tactics huggingface dataset:
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 })
⊢ Function.Bijective (F.toDescentData f).map ↔
    Presieve.IsSheafFor (F.presheafHom M N) (Presieve.ofArrows (fun i ↦ Over.mk (f i)) fun i ↦ Over.homMk (f i) ⋯)

Tactic:
by

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

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
S : C
R : Sieve S
⊢ F.IsPrestackFor R.arrows ↔
    ∀ (M N : ↑(F.obj { as := op S })),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows

Tactic:
by

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
S : C
R : Sieve S
⊢ (∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := op S₀ })) (a : S ⟶ S₀),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows) →
    ∀ (M N : ↑(F.obj { as := op S })),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Types

Goal state before:
pp: α : Type u
f g : MonoOver α
t : f ⟶ g
⊢ Set.range ⇑(hom f.obj.hom) ⊆ Set.range ⇑(hom g.obj.hom)

Tactic:
by

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
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
hf : ((Sieve.overEquiv (Over.mk a)).symm R).arrows f
⊢ 𝟙 Y.left ≫ ((Over.map a).obj (Over.mk (Over.Hom.left f))).hom = Y.hom

Tactic:
by

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
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
hf : ((Sieve.overEquiv (Over.mk a)).symm R).arrows f
⊢ f ≫ (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv =
    Over.homMk (𝟙 Y.left) ⋯ ≫ (Over.map a).map (Over.homMk (Over.Hom.left f) ⋯)

Tactic:
by

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
S : C
R : Sieve S
⊢ F.IsPrestackFor R.arrows ↔
    ∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := op S₀ })) (a : S ⟶ S₀),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows

Tactic:
by

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
S₀ : C
S : Over S₀
R : Sieve S
hF : F.IsPrestackFor ((Sieve.overEquiv S) R).arrows
M N : ↑(F.obj { as := op S₀ })
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows

Tactic:
by

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
⊢ Nonempty (F.toDescentData f).FullyFaithful

Tactic:
by

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
S : C
R : Presieve S
hR : Sieve.generate R ∈ J S
⊢ (Sieve.ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ∈ ?m.35 S

Tactic:
by

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
S : C
R : Presieve S
hR : Sieve.generate R ∈ J S
⊢ F.IsPrestackFor R

Tactic:
by

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
S : C
R : Sieve S
hR : R ∈ J S
⊢ Sieve.generate R.arrows ∈ ?m.23 S

Tactic:
by

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
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows
S✝ : C
M N : ↑(F.obj { as := op S✝ })
⊢ Presheaf.IsSheaf (J.over S✝) (F.presheafHom M N)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : D
f : X ⟶ Y
⊢ (associator C D E).map ((inl_ (C ⊕ D) E).map ((inr_ C D).map f)) = (inr_ C (D ⊕ E)).map ((inl_ D E).map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : E
f : X ⟶ Y
⊢ (associator C D E).map ((inr_ (C ⊕ D) E).map f) = (inr_ C (D ⊕ E)).map ((inr_ D E).map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : C
f : X ⟶ Y
⊢ (inverseAssociator C D E).map ((inl_ C (D ⊕ E)).map f) = (inl_ (C ⊕ D) E).map ((inl_ C D).map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : D
f : X ⟶ Y
⊢ (inverseAssociator C D E).map ((inr_ C (D ⊕ E)).map ((inl_ D E).map f)) = (inl_ (C ⊕ D) E).map ((inr_ C D).map f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
c : Classifier C
Y : C
f : Y ⟶ c.Ω₀
⊢ c.χ (𝟙 Y) = c.χ₀ Y ≫ c.truth

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X : C
φ : X ⟶ 𝒞.Ω
⊢ IsPullback (pullback.fst φ 𝒞.truth) ?m.52 φ 𝒞.truth

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ 𝒞.χ i ≫ (Iso.refl 𝒞.Ω).hom = (Iso.refl X).hom ≫ 𝒞.χ i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ 𝒞.truth ≫ (Iso.refl 𝒞.Ω).hom = (Iso.refl 𝒞.Ω₀).hom ≫ 𝒞.truth

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X : C
φ : X ⟶ 𝒞.Ω
⊢ 𝒞.χ ((pullback φ).obj 𝒞.truth_as_subobject).arrow = φ

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X✝ : C
φ : X✝ ⟶ 𝒞.Ω
⊢ (fun x ↦ 𝒞.χ (arrow x)) ((fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject) φ) = φ

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X✝ : C
x : (Subobject.presheaf C).obj (Opposite.op X✝)
⊢ (fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject) ((fun x ↦ 𝒞.χ (arrow x)) x) = x

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X✝ X'✝ : C
x✝¹ : X✝ ⟶ X'✝
x✝ : X'✝ ⟶ 𝒞.Ω
⊢ { toFun := fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject, invFun := fun x ↦ 𝒞.χ (arrow x), left_inv := ⋯,
        right_inv := ⋯ }
      (x✝¹ ≫ x✝) =
    (ConcreteCategory.hom ((Subobject.presheaf C).map x✝¹.op))
      ({ toFun := fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject, invFun := fun x ↦ 𝒞.χ (arrow x), left_inv := ⋯,
          right_inv := ⋯ }
        x✝)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
f : X ⟶ Ω
⊢ h.homEquiv f = (Subobject.pullback f).obj h.Ω₀

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
x : Subobject X
⊢ (Subobject.pullback (h.homEquiv.symm x)).obj h.Ω₀ = x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ Over.Hom.left (h.iso m).inv.hom ≫ h.π m = pullbackπ (h.χ m) h.Ω₀

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
χ' : X ⟶ Ω
π : U ⟶ underlying.obj h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
⊢ χ' = h.χ m

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
π' : X ⟶ underlying.obj h.Ω₀
⊢ ∀ (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow), s.fst ≫ 𝟙 X = s.fst

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
π' : X ⟶ underlying.obj h.Ω₀
s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
⊢ s.fst ≫ π' = s.snd

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
π' : X ⟶ underlying.obj h.Ω₀
s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
m : s.pt ⟶ X
hm : m ≫ 𝟙 X = s.fst
x✝ : m ≫ π' = s.snd
⊢ m = s.fst

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
π' : X ⟶ underlying.obj h.Ω₀
⊢ π' = h.π (𝟙 X)

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U✝ X✝ : C
m : U✝ ⟶ X✝
x✝ : Mono m
⊢ m ≫ (Iso.refl X✝).hom = (Iso.refl U✝).hom ≫ m

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U✝ X✝ : C
m : U✝ ⟶ X✝
x✝ : Mono m
⊢ h.χ m ≫ (Iso.refl Ω).hom = (Iso.refl X✝).hom ≫ h.χ m

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U✝ X✝ : C
m : U✝ ⟶ X✝
x✝ : Mono m
⊢ h.Ω₀.arrow ≫ (Iso.refl Ω).hom = h.isoΩ₀.hom ≫ h.isoΩ₀.inv ≫ h.Ω₀.arrow

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ (associativity C D E).functor.IsEquivalence

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ m ≫ (Iso.refl X).hom = (Iso.refl U).hom ≫ m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ (associativity C D E).inverse.IsEquivalence

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ χ' ≫ (Iso.refl Ω).hom = (Iso.refl X).hom ≫ χ'

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ (h.isoΩ₀.inv ≫ h.Ω₀.arrow) ≫ (Iso.refl Ω).hom = h.isoΩ₀.symm.hom ≫ h.Ω₀.arrow

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ χ' = h.χ m

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ CommSq 𝒞.truth eΩ₀.hom eΩ.hom t

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ IsPullback m (from' F) (𝒞.χ m ≫ eΩ.hom) t

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ CommSq t eΩ₀.inv eΩ.inv 𝒞.truth

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ χ' ≫ eΩ.inv = 𝒞.χ m

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ ∀ {χ₀' : F ⟶ Ω₀} {χ' : G ⟶ Ω}, IsPullback m χ₀' χ' t → χ' = 𝒞.χ m ≫ eΩ.hom

Tactic:
by

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
⊢ 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

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)
⊢ e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω = 𝒞₁.χ (e.inverse.map m)

Tactic:
by

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 𝒞₁.Ω},
    IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth) → χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

Tactic:
by

Goal state after:
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
inst✝ : Mono m
⊢ IsPullback m ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F) (χ m) (truth C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
A' : Type u_2
inst✝¹ : Category.{v_2, u_2} A'
B : Type u
inst✝ : Category.{v, u} B
F : A ⊕ A' ⥤ B
⊢ natTransOfWhiskerLeftInlInr (𝟙 (inl_ A A' ⋙ F)) (𝟙 (inr_ A A' ⋙ F)) = 𝟙 F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
A' : Type u_2
inst✝¹ : Category.{v_2, u_2} A'
B : Type u
inst✝ : Category.{v, u} B
F G H : A ⊕ A' ⥤ B
η₁ : inl_ A A' ⋙ F ⟶ inl_ A A' ⋙ G
η₂ : inr_ A A' ⋙ F ⟶ inr_ A A' ⋙ G
ν₁ : inl_ A A' ⋙ G ⟶ inl_ A A' ⋙ H
ν₂ : inr_ A A' ⋙ G ⟶ inr_ A A' ⋙ H
⊢ natTransOfWhiskerLeftInlInr (η₁ ≫ ν₁) (η₂ ≫ ν₂) =
    natTransOfWhiskerLeftInlInr η₁ η₂ ≫ natTransOfWhiskerLeftInlInr ν₁ ν₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
A' : Type u_2
inst✝¹ : Category.{v_2, u_2} A'
B : Type u
inst✝ : Category.{v, u} B
F G : A ⊕ A' ⥤ B
η₁ : inl_ A A' ⋙ F ≅ inl_ A A' ⋙ G
η₂ : inr_ A A' ⋙ F ≅ inr_ A A' ⋙ G
⊢ natIsoOfWhiskerLeftInlInr η₁ η₂ =
    (functorEquiv A A' B).unitIso.app F ≪≫
      (functorEquiv A A' B).inverse.mapIso (η₁.prod η₂) ≪≫ (functorEquiv A A' B).unitIso.symm.app G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: A : Type u_1
inst✝³ : Category.{v_1, u_1} A
A' : Type u_2
inst✝² : Category.{v_2, u_2} A'
B : Type u
inst✝¹ : Category.{v, u} B
T : Type u_3
inst✝ : Category.{v_3, u_3} T
⊢ ∀ {X Y : (A ⊕ A') ⊕ T ⥤ B} (f : X ⟶ Y),
    ((sum.associativity A A' T).congrLeft.trans
                ((functorEquiv A (A' ⊕ T) B).trans (Equivalence.refl.prod (functorEquiv A' T B)))).functor.map
          f ≫
        ((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y).symm ≪≫
                isoWhiskerRight (sum.inlCompInverseAssociator A A' T) Y ≪≫
                  (inl_ A A').associator (inl_ (A ⊕ A') T) Y).prod
            (((inl_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y).symm ≪≫
                  ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y).symm ≪≫
                    isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) Y ≪≫
                      (inr_ A A').associator (inl_ (A ⊕ A') T) Y).prod
              ((inr_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y).symm ≪≫
                ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y).symm ≪≫
                  isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) Y))).hom =
      ((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X).symm ≪≫
                isoWhiskerRight (sum.inlCompInverseAssociator A A' T) X ≪≫
                  (inl_ A A').associator (inl_ (A ⊕ A') T) X).prod
            (((inl_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X).symm ≪≫
                  ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X).symm ≪≫
                    isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) X ≪≫
                      (inr_ A A').associator (inl_ (A ⊕ A') T) X).prod
              ((inr_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X).symm ≪≫
                ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X).symm ≪≫
                  isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) X))).hom ≫
        (((functorEquiv (A ⊕ A') T B).trans ((functorEquiv A A' B).prod Equivalence.refl)).trans
                (prod.associativity (A ⥤ B) (A' ⥤ B) (T ⥤ B))).functor.map
          f

Tactic:
intros
      ext
      all_goals
        dsimp
        simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Goal state after: