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

Goal state before:
pp: case inl
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : X'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inl val
⊢ ∃! y, Sum.inl val = Sum.inl y

pp: case inr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : Y'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inl y

Tactic:
· simp

Goal state after:
case inr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : Y'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inl y
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : Y'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inr y

Tactic:
· simp

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.uniq
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) (m : YE ⟶ s.pt),
    (c.inr ≫ fE) ≫ m = s.inl →
      iY ≫ m = s.inr → m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
intro s m e₁ e₂
      apply PushoutCocone.IsColimit.hom_ext H.isColimit
      · symm; exact (H.isColimit.fac _ WalkingSpan.left).trans e₂.symm
      · rw [H.isColimit.fac _ WalkingSpan.right]
        apply BinaryCofan.IsColimit.hom_ext hc
        · erw [hc.fac]
          erw [← H.w_assoc]
          rw [e₂]
          rfl
        · refine ((Category.assoc _ _ _).symm.trans e₁).trans ?_; symm; exact hc.fac _ _

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
⊢ (coprod.inl ≫
      coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j) ≫
        Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr) =
    coprod.inl ≫ 𝟙 (f i ⨿ ∐ fun j ↦ f ↑j)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
j : ↑{i}ᶜ
⊢ (Sigma.ι (fun j ↦ f ↑j) j ≫
      coprod.inr ≫
        coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j) ≫
          Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr) =
    Sigma.ι (fun j ↦ f ↑j) j ≫ coprod.inr ≫ 𝟙 (f i ⨿ ∐ fun j ↦ f ↑j)

Tactic:
· simp

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
j : ↑{i}ᶜ
⊢ (Sigma.ι (fun j ↦ f ↑j) j ≫
      coprod.inr ≫
        coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j) ≫
          Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr) =
    Sigma.ι (fun j ↦ f ↑j) j ≫ coprod.inr ≫ 𝟙 (f i ⨿ ∐ fun j ↦ f ↑j)
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ 𝟭 D₁ ⟶ G' ⋙ F'

Tactic:
by
  letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') :=
    Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso.symm
  exact Localization.liftNatTrans L₁ W₁ L₁ ((G ⋙ F) ⋙ L₁) (𝟭 D₁) (G' ⋙ F')
    (whiskerRight adj.unit L₁)

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
      F'.map (G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂)) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
← (Localization.ε _ _ _ _ _ _).naturality_assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (𝟭 D₁).map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (Localization.ε adj L₁ W₁ L₂ G' F').app ((F ⋙ L₁).obj X₂) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
P₁ P₂ : C
f : P₁ ⟶ P₂
⊢ isColocal (fun x ↦ x ∈ Set.range G.obj) f ↔ (MorphismProperty.isomorphisms D).inverseImage F f

Tactic:
rw [isColocal_iff_isIso_map adj]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
P₁ P₂ : C
f : P₁ ⟶ P₂
⊢ IsIso (F.map f) ↔ (MorphismProperty.isomorphisms D).inverseImage F f
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve X
hS : S ∈ J X
Z : Cᵒᵖ ⥤ Type w
hZ : Presieve.IsSheaf J Z
⊢ Function.Bijective fun g ↦ (shrinkFunctor.{w, v_1, u_1} S).ι ≫ g

Tactic:
rw [← Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve X
hS : S ∈ J X
Z : Cᵒᵖ ⥤ Type w
hZ : Presieve.IsSheaf J Z
⊢ Presieve.IsSheafFor Z S.arrows
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
⊢ Adhesive D

Tactic:
have := adj.leftAdjoint_preservesColimits
  have := adj.rightAdjoint_preservesLimits
  apply Adhesive.mk (hasPushout_of_mono_left := H₂)
  intro W X Y Z f g h i _ H
  have := Adhesive.van_kampen (IsPushout.of_hasPushout (Gr.map f) (Gr.map g))
  rw [IsPushout.isVanKampen_iff] at this ⊢
  refine (IsVanKampenColimit.precompose_isIso_iff
    (Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp ?_
  refine ((this.precompose_isIso (spanCompIso _ _ _).hom).map_reflective adj).of_iso
    (IsColimit.uniqueUpToIso ?_ ?_)
  · exact isColimitOfPreserves Gl ((IsColimit.precomposeHomEquiv _ _).symm <| pushoutIsPushout _ _)
  · exact (IsColimit.precomposeHomEquiv _ _).symm H.isColimit

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
⊢ IsSheaf J (F.op ⋙ G)

Tactic:
by
  intro X S hS
  rw [Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp, ← Functor.whiskeringLeft_obj_obj,
    ← adj.map_comp_bijective_iff]
  refine h hS _ ?_
  rwa [isSheaf_iff_isSheaf_of_type]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : (ConcreteCategory.hom ((J.toPlus P).app X)) x = (ConcreteCategory.hom ((J.toPlus P).app X)) y
⊢ equalizerSieve x y ∈ J (unop X)

Tactic:
rw [toPlus_eq_mk, toPlus_eq_mk, eq_mk_iff_exists] at h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : ∃ W h1 h2, (Meq.mk ⊤ x).refine h1 = (Meq.mk ⊤ y).refine h2
⊢ equalizerSieve x y ∈ J (unop X)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (F.obj (op U))
V : C
i : V ⟶ U
⊢ (imageSieve f ((ConcreteCategory.hom (f.app (op U))) s)).arrows i ↔ ⊤.arrows i

Tactic:
simp only [Sieve.top_apply, iff_true, imageSieve_apply]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (F.obj (op U))
V : C
i : V ⟶ U
⊢ ∃ t,
    (ConcreteCategory.hom (f.app (op V))) t =
      (ConcreteCategory.hom (G.map i.op)) ((ConcreteCategory.hom (f.app (op U))) s)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦ equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)

Tactic:
refine J.superset_covering ?_ (J.transitive hS (Sieve.bind S.1 T) ?_)

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦ equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
⊢ Sieve.bind S.arrows T ≤ equalizerSieve x₁ x₂

case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦ equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄, S.arrows f → Sieve.pullback f (Sieve.bind S.arrows T) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : HasWeakSheafify J A
inst✝ : J.WEqualsLocallyBijective A
P Q : Cᵒᵖ ⥤ A
φ : P ⟶ Q
⊢ IsLocallySurjective J ((sheafToPresheaf J A).map ((presheafToSheaf J A).map φ)) ↔
    IsLocallySurjective J (φ ≫ toSheafify J Q)

Tactic:
← comp_isLocallySurjective_iff J (toSheafify J P),

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : HasWeakSheafify J A
inst✝ : J.WEqualsLocallyBijective A
P Q : Cᵒᵖ ⥤ A
φ : P ⟶ Q
⊢ IsLocallySurjective J (toSheafify J P ≫ (sheafToPresheaf J A).map ((presheafToSheaf J A).map φ)) ↔
    IsLocallySurjective J (φ ≫ toSheafify J Q)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1.isFalse
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
k : ι
h✝ : ¬k = i
⊢ (eqToHom ⋯ ≫ initial.to (X k)) ≫ c.ι.app { as := k } = (eqToHom ⋯ ≫ initial.to (X i)) ≫ c.inj i

Tactic:
· simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((Discrete.functor f).obj i)) (𝟙 ((Discrete.functor f).obj i)) (c.ι.app i) (c.ι.app i)

Tactic:
← Category.id_comp (c.ι.app i)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((Discrete.functor f).obj i)) (𝟙 ((Discrete.functor f).obj i))
    (𝟙 ((Discrete.functor f).obj i) ≫ c.ι.app i) (c.ι.app i)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
e_5✝ : (Discrete.functor f).obj i = f i.as
⊢ 𝟙 ((Discrete.functor f).obj i) = eqToHom ⋯ ≫ if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as)

pp: case convert_6
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((Discrete.functor f).obj i)) (eqToHom ⋯) (𝟙 ((Discrete.functor f).obj i))
    (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as))

Tactic:
· simp

Goal state after:
case convert_6
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((Discrete.functor f).obj i)) (eqToHom ⋯) (𝟙 ((Discrete.functor f).obj i))
    (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as))
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
e : (Discrete.functor fun i ↦ uliftYoneda.{w, v, u}.obj (X i)) ≅
  Discrete.functor fun i ↦ shrinkYoneda.{max w v, v, u}.obj (X i) :=
  Discrete.natIso fun i ↦ uliftYonedaIsoShrinkYoneda.app (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
this :
  (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i)) ≫ uliftYonedaIsoShrinkYoneda.hom.app S =
    Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max v w, v, u}.map (f i)
⊢ Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max w v, v, u}.map (f i)) ↔
    Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i))

Tactic:
rw [← this, Presheaf.isLocallySurjective_comp_iff J]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback v u ≅ d.pt

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback.fst v u ≫ (Iso.refl B).hom = Iso.hom ?refine_1 ≫ Cofan.IsColimit.desc hd q₁

pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback.snd v u ≫ (Iso.refl a.pt).hom = Iso.hom ?refine_1 ≫ Cofan.IsColimit.desc hd fun x ↦ q₂ x ≫ a.inj x

Tactic:
· exact hc.coconePointUniqueUpToIso hd

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback.fst v u ≫ (Iso.refl B).hom = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₁

case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback.snd v u ≫ (Iso.refl a.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun x ↦ q₂ x ≫ a.inj x