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

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := (FinCategory.equivAsType K).symm.trans AsSmall.equiv
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
⊢ PreservesLimitsOfShape (AsSmall (FinCategory.AsType K)) (plusPlusSheaf J D)

Tactic:
constructor

Goal state after:
C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := ⋯
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
⊢ autoParam (∀ {K_1 : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D}, PreservesLimit K_1 (plusPlusSheaf J D))
    PreservesLimitsOfShape.preservesLimit._autoParam
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := (FinCategory.equivAsType K).symm.trans AsSmall.equiv
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D
⊢ PreservesLimit F (plusPlusSheaf J D)

Tactic:
constructor

Goal state after:
C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := ⋯
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D
⊢ ∀ {c : Cone F} (hc : IsLimit c), Nonempty (IsLimit ((plusPlusSheaf J D).mapCone c))
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := (FinCategory.equivAsType K).symm.trans AsSmall.equiv
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D
S : Cone F
hS : IsLimit S
⊢ Nonempty (IsLimit ((plusPlusSheaf J D).mapCone S))

Tactic:
constructor

Goal state after:
C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := ⋯
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D
S : Cone F
hS : IsLimit S
⊢ IsLimit ((plusPlusSheaf J D).mapCone S)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ IsVanKampenColimit c ↔
    ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ c.inl = c'.inl ≫ f →
        αY ≫ c.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ IsVanKampenColimit c →
    ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ c.inl = c'.inl ≫ f →
        αY ≫ c.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)

case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ (∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ c.inl = c'.inl ≫ f →
        αY ≫ c.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)) →
    IsVanKampenColimit c
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)) ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
constructor

Goal state after:
case mp.mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)) →
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

case mp.mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inr ↔
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
constructor

Goal state after:
case mpr.mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inr →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

case mpr.mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) →
    IsPullback c'.inl (α.app { as := WalkingPair.left })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inr
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.isoClosure.isLocal f ↔ P.isLocal f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.isoClosure.isLocal f → P.isLocal f

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.isLocal f → P.isoClosure.isLocal f
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
constructor

Goal state after:
case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Injective fun g ↦ f ≫ g

case mpr.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Surjective fun g ↦ f ≫ g
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
⊢ Nonempty (IsColimit c') → IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr → Nonempty (IsColimit c')
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
constructor

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Injective fun g ↦ f ≫ g

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Surjective fun g ↦ f ≫ g
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ P.isLocal f ↔ IsIso f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ P.isLocal f → IsIso f

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ IsIso f → P.isLocal f
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
constructor

Goal state after:
case mp.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := ⋯
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inl αX f c.inl

case mp.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := ⋯
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inr αY f c.inr
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
⊢ P.isoClosure.isColocal g ↔ P.isColocal g

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
⊢ P.isoClosure.isColocal g → P.isColocal g

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
⊢ P.isColocal g → P.isoClosure.isColocal g
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Function.Bijective fun f ↦ f ≫ g

Tactic:
constructor

Goal state after:
case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Function.Injective fun f ↦ f ≫ g

case mpr.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Function.Surjective fun f ↦ f ≫ g
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
⊢ Adhesive (D ⥤ C)

Tactic:
constructor

Goal state after:
J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
⊢ ∀ {W X Y Z : D ⥤ C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] (H : IsPushout f g h i), H.IsVanKampen
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Bijective fun f_1 ↦ f_1 ≫ f

Tactic:
constructor

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Injective fun f_1 ↦ f_1 ≫ f

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Surjective fun f_1 ↦ f_1 ≫ f
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Surjective fun f_1 ↦ f_1 ≫ f

Tactic:
intro g
    exact ⟨g ≫ inv f, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ P.isColocal f ↔ IsIso f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ P.isColocal f → IsIso f

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ IsIso f → P.isColocal f
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
P : Cᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf J P ↔ P ∈ Set.range (sheafToPresheaf J A).obj

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
P : Cᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf J P → P ∈ Set.range (sheafToPresheaf J A).obj

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
P : Cᵒᵖ ⥤ A
⊢ P ∈ Set.range (sheafToPresheaf J A).obj → Presheaf.IsSheaf J P