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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
A B : (J.Cover X)ᵒᵖ
f : A ⟶ B
g : (unop B).shape.L
⊢ (F.map
          (Multiequalizer.lift ((unop B).index P) (multiequalizer ((unop A).index P))
            (fun I ↦ Multiequalizer.ι ((unop A).index P) (I.map f.unop)) ⋯) ≫
        ((isLimitOfPreserves F (limit.isLimit ((unop B).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop B).index P).multicospan ⋙ F))).hom ≫
          (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop B)).symm).hom) ≫
      Multiequalizer.ι ((unop B).index (P ⋙ F)) g =
    ((((isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop A).index P).multicospan ⋙ F))).hom ≫
          (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm).hom) ≫
        Multiequalizer.lift ((unop B).index (P ⋙ F)) (multiequalizer ((unop A).index (P ⋙ F)))
          (fun I ↦ Multiequalizer.ι ((unop A).index (P ⋙ F)) (I.map f.unop)) ⋯) ≫
      Multiequalizer.ι ((unop B).index (P ⋙ F)) g

Tactic:
simp [← F.map_comp]

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

Goal state before:
pp: case h.refine_1
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst✝ : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback l (pullback.snd αX f) αY g

Tactic:
refine IsPullback.of_right' ?_ hi

Goal state after:
case h.refine_1
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst✝ : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (g ≫ i)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case h.refine_2
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst✝ : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback l (pullback.snd αX f) αY g

Tactic:
refine IsPullback.of_right' ?_ hi

Goal state after:
case h.refine_2
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst✝ : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (g ≫ i)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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
c : BinaryCofan X Y
hc : IsColimit c
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
d : c.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c₀.pt).obj { as := WalkingPair.left }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
⊢ (αY ≫ HT.from Y) ≫ c₀.inr = c'.inr ≫ f ≫ d

Tactic:
rw [← reassoc_of% hY, hd', Category.assoc]

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

Goal state before:
pp: case mpr.refine_2
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
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ∀ ⦃X_1 Y_1 : WalkingSpan⦄ (f_1 : X_1 ⟶ Y_1),
    ((span f' g').map f_1 ≫ Option.casesOn Y_1 αW fun val ↦ WalkingPair.casesOn val αX αY) =
      (Option.casesOn X_1 αW fun val ↦ WalkingPair.casesOn val αX αY) ≫ (span f g).map f_1

Tactic:
rintro i _ (_ | _ | _)
      · dsimp; simp only [Functor.map_id, Category.comp_id, Category.id_comp]
      exacts [hf.w, hg.w]

Goal state after:
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.inr (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.inr 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.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:
· apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm

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.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
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.mp
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
inst✝ : HasPullback αX f
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
    ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'

pp: case mp.mpr
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
inst✝ : HasPullback αX f
⊢ (∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i') →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
· intro ⟨hh, hi⟩
      exact H'.exists_cube_filling hh hi

Goal state after:
case mp.mpr
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
inst✝ : HasPullback αX f
⊢ (∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i') →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₂.fac_right
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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
⊢ ((↾fun p ↦ (↑p).1) ≫
      ↾fun x ↦
        if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
        else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩)) =
    s.inr

Tactic:
ext ⟨⟨x, ⟨⟩⟩, hx⟩

Goal state after:
case h₂.fac_right
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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
x : Z
hx : (ConcreteCategory.hom f) (x, PUnit.unit).1 = (ConcreteCategory.hom (↾Sum.inr)) (x, PUnit.unit).2
⊢ (ConcreteCategory.hom
          ((↾fun p ↦ (↑p).1) ≫
            ↾fun x ↦
              if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
              else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩))).toFun
      ⟨(x, PUnit.unit), hx⟩ =
    (ConcreteCategory.hom s.inr).toFun ⟨(x, PUnit.unit), hx⟩
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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑X'
h : (ConcreteCategory.hom s.fst) x = Sum.inl val
⊢ ∃! y, Sum.inl val = Sum.inr 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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑Y'
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inr y

Tactic:
· apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm

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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑Y'
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inr y
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 : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ (CatCommSq.iso G L₁ L₂ G').inv.app ((𝟭 C₁).obj X₁) ≫
      L₂.map (G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁)) ≫
        (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
eq,

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 : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ (CatCommSq.iso G L₁ L₂ G').inv.app ((𝟭 C₁).obj X₁) ≫
      L₂.map (𝟙 (G.obj X₁)) ≫ (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
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₂)
⊢ (𝟭 D₁).map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      L₁.map (adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂)) ≫
        (CatCommSq.iso F L₂ L₁ F').hom.app ((𝟭 C₂).obj X₂) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
eq,

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₂) ≫
      L₁.map (𝟙 (F.obj X₂)) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app ((𝟭 C₂).obj 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
P : ObjectProperty C
X Z : C
x✝ : P Z
⊢ Function.Bijective fun g ↦ 𝟙 X ≫ g

Tactic:
simpa [id_comp] using! Function.bijective_id

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
⊢ P.isoClosure.isColocal = P.isColocal

Tactic:
by
  ext Y Z g
  constructor
  · intro hg X hX
    exact hg _ (P.le_isoClosure _ hX)
  · rintro hg X ⟨X', hX', ⟨e⟩⟩
    constructor
    · intro f₁ f₂ eq
      rw [← cancel_epi e.inv]
      apply (hg _ hX').1
      simp [eq]
    · intro f
      obtain ⟨a, h⟩ := (hg _ hX').2 (e.inv ≫ f)
      exact ⟨e.hom ≫ a, by simp [h]⟩

Goal state after:
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
P : ObjectProperty C
x✝² x✝¹ : C
x✝ : P x✝¹
⊢ Function.Bijective fun f ↦ f ≫ 𝟙 x✝²

Tactic:
simpa [id_comp] using! Function.bijective_id

Goal state after:
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
⊢ F.IsLocalization ((MorphismProperty.isomorphisms D).inverseImage F)

Tactic:
exact adj.isLocalization'

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (adj₁.unit.app P₁ ≫ (sheafToPresheaf J A).map (G₁.map f)) F)

Tactic:
whiskerRight_comp,

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (adj₁.unit.app P₁) F ≫ whiskerRight ((sheafToPresheaf J A).map (G₁.map f)) F)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝¹ : J.HasSheafCompose F
inst✝ : J.PreservesSheafification F
⊢ IsIso (sheafComposeNatTrans J F adj₁ adj₂)

Tactic:
← J.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝¹ : J.HasSheafCompose F
inst✝ : J.PreservesSheafification F
⊢ J.PreservesSheafification F
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_4.refine_2.right
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι.app { as := WalkingPair.right })
    ((mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i)).app { as := WalkingPair.right }) i
    (c₂.ι.app { as := WalkingPair.right })

Tactic:
simp only [pair_obj_right, Functor.const_obj_obj, BinaryCofan.mk_pt, BinaryCofan.ι_app_right,
        BinaryCofan.mk_inr, mapPair_right]
      exact (IsPullback.of_hasPullback (BinaryCofan.inr c₂) i).flip

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
N : PresheafOfModules R
hN : Presheaf.IsSheaf J N.presheaf
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : IsLocallySurjective J f
inst✝ : IsLocallyInjective J f
ψ : M₁ ⟶ N
⊢ ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₂.obj X)),
    (ConcreteCategory.hom (((ObjectProperty.isLocal.homEquiv ⋯ N.presheaf hN).symm ((toPresheaf R).map ψ)).app X))
        (r • m) =
      r •
        (ConcreteCategory.hom (((ObjectProperty.isLocal.homEquiv ⋯ N.presheaf hN).symm ((toPresheaf R).map ψ)).app X)) m

Tactic:
obtain ⟨φ, hφ⟩ := ((J.W_of_isLocallyBijective
          ((PresheafOfModules.toPresheaf R).map f)).homEquiv _ hN).surjective
          ((PresheafOfModules.toPresheaf R).map ψ)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
N : PresheafOfModules R
hN : Presheaf.IsSheaf J N.presheaf
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : IsLocallySurjective J f
inst✝ : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ : (ObjectProperty.isLocal.homEquiv ⋯ N.presheaf hN) φ = (toPresheaf R).map ψ
⊢ ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₂.obj X)),
    (ConcreteCategory.hom (((ObjectProperty.isLocal.homEquiv ⋯ N.presheaf hN).symm ((toPresheaf R).map ψ)).app X))
        (r • m) =
      r •
        (ConcreteCategory.hom (((ObjectProperty.isLocal.homEquiv ⋯ N.presheaf hN).symm ((toPresheaf R).map ψ)).app X)) m