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

Goal state before:
pp: case refine_2.mp
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ : (pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i = pullback.snd αY c.inr ≫ c.inr
⊢ IsPullback i' αY αZ i

Tactic:
obtain ⟨hc₄⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
      (BinaryCofan.mk _ _) αW _ _ e₁.symm e₂.symm).mpr <| by
        constructor
        · apply IsPullback.of_right _ e₁ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst, ← H.w, ← w.w]; exact hf.paste_horiz hc₄
        · apply IsPullback.of_right _ e₂ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst]; exact hc₃

Goal state after:
case refine_2.mp
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄✝ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ : (pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i = pullback.snd αY c.inr ≫ c.inr
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
⊢ IsPullback i' αY αZ i
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ mapPair f f ≫ (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι =
    (BinaryCofan.mk (𝟙 A) (𝟙 A)).ι ≫ (const (Discrete WalkingPair)).map f

Tactic:
ext ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ (mapPair f f ≫ (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι).app { as := WalkingPair.left } =
    ((BinaryCofan.mk (𝟙 A) (𝟙 A)).ι ≫ (const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ (mapPair f f ≫ (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι).app { as := WalkingPair.right } =
    ((BinaryCofan.mk (𝟙 A) (𝟙 A)).ι ≫ (const (Discrete WalkingPair)).map f).app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: 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
⊢ mapPair αX αY ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f

Tactic:
ext ⟨⟨⟩⟩

Goal state after:
case left
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
⊢ (mapPair αX αY ≫ c.ι).app { as := WalkingPair.left } =
    (c'.ι ≫ (const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }

case right
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
⊢ (mapPair αX αY ≫ c.ι).app { as := WalkingPair.right } =
    (c'.ι ≫ (const (Discrete WalkingPair)).map f).app { as := WalkingPair.right }
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✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : P.isLocal g
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
by
    rw [← Function.Bijective.of_comp_iff _ (hg Z hZ)]
    simpa using! hfg Z hZ

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr

Tactic:
ext ⟨⟨⟩⟩

Goal state after:
case refine_1.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ (mapPair (initial.to X) (𝟙 Y) ≫ c.ι).app { as := WalkingPair.left } =
    ((BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr).app { as := WalkingPair.left }

case refine_1.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ (mapPair (initial.to X) (𝟙 Y) ≫ c.ι).app { as := WalkingPair.right } =
    ((BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr).app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr

Tactic:
ext ⟨⟨⟩⟩

Goal state after:
case refine_1.left
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ (mapPair (initial.to X) (𝟙 Y) ≫ c.ι).app { as := WalkingPair.left } =
    ((BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr).app { as := WalkingPair.left }

case refine_1.right
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ (mapPair (initial.to X) (𝟙 Y) ≫ c.ι).app { as := WalkingPair.right } =
    ((BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr).app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mp.refine_1
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₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
a✝ : IsLocallyInjective J φ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)
S : Sieve (unop X) := equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve Y :=
  fun Y f x_1 ↦ equalizerSieve ((ConcreteCategory.hom (F₁.map f.op)) x) ((ConcreteCategory.hom (F₁.map f.op)) y)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop X
hg : S.arrows g
ha : (T hg).arrows a
⊢ (equalizerSieve x y).arrows (a ≫ g)

Tactic:
simpa using! ha

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

Goal state before:
pp: case refine_4.refine_1
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 }) ⋯)
⊢ mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι =
    (BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι ≫ (const (Discrete WalkingPair)).map i

Tactic:
ext ⟨⟨⟩⟩

Goal state after:
case refine_4.refine_1.left
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 }) ⋯)
⊢ (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι).app { as := WalkingPair.left } =
    ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι ≫ (const (Discrete WalkingPair)).map i).app
      { as := WalkingPair.left }

case refine_4.refine_1.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 }) ⋯)
⊢ (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι).app { as := WalkingPair.right } =
    ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι ≫ (const (Discrete WalkingPair)).map i).app
      { as := WalkingPair.right }
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✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop (op X)
hg : S.arrows g
ha : (T g hg).arrows a
⊢ (ConcreteCategory.hom (f₁.app (op Y)))
      ((ConcreteCategory.hom (F₁.map a.op)) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) g hg)) =
    (ConcreteCategory.hom (F₂.map (a ≫ g).op)) x

Tactic:
simpa using! ha

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
P✝ Q✝ R✝ : SheafOfModules R
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝

Tactic:
ext1

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
P✝ Q✝ R✝ : SheafOfModules R
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).val = (f✝ ≫ g✝ + f'✝ ≫ g✝).val
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
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₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
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 α
Hc : IsColimit c
j : Fin (n + 1)
⊢ mapPair (α.app { as := 0 }) (Sigma.desc fun b ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι =
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).ι ≫
      (const (Discrete WalkingPair)).map i

Tactic:
ext ⟨⟨⟩⟩

Goal state after:
case refine_1.left
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₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
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 α
Hc : IsColimit c
j : Fin (n + 1)
⊢ (mapPair (α.app { as := 0 }) (Sigma.desc fun b ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι).app
      { as := WalkingPair.left } =
    ((BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).ι ≫
          (const (Discrete WalkingPair)).map i).app
      { as := WalkingPair.left }

case refine_1.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₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
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 α
Hc : IsColimit c
j : Fin (n + 1)
⊢ (mapPair (α.app { as := 0 }) (Sigma.desc fun b ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι).app
      { as := WalkingPair.right } =
    ((BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).ι ≫
          (const (Discrete WalkingPair)).map i).app
      { as := WalkingPair.right }
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
φ : (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

Tactic:
simp only [← hφ, Equiv.symm_apply_apply]

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 (φ.app X)) (r • m) = r • (ConcreteCategory.hom (φ.app X)) m
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
inst✝² : Balanced C
F : C ⥤ D
inst✝¹ : F.ReflectsMonomorphisms
inst✝ : F.ReflectsEpimorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (F.map f)
⊢ IsIso f

Tactic:
have : Epi f := epi_of_epi_map F inferInstance

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
inst✝² : Balanced C
F : C ⥤ D
inst✝¹ : F.ReflectsMonomorphisms
inst✝ : F.ReflectsEpimorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (F.map f)
this : Epi f
⊢ IsIso f
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N : M.Submodule
s : Set M.Submodule
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ⨅ N ∈ s, N.obj X✝ ≤ Submodule.comap (M.restrictₛₗ f) (⨅ N ∈ s, N.obj Y✝)

Tactic:
by
        simp_rw [Submodule.comap_iInf, le_iInf₂_iff]
        intro N hN
        refine iInf₂_le_of_le _ hN (N.map _)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
M₀ : PresheafOfModules R₀
⊢ sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
      ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯ =
    𝟙 (sheafify α (CategoryTheory.toSheafify J M₀.presheaf))

Tactic:
ext1

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
M₀ : PresheafOfModules R₀
⊢ (sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯).val =
    (𝟙 (sheafify α (CategoryTheory.toSheafify J M₀.presheaf))).val
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
X✝ Y✝ Z✝ : PresheafOfModules R₀
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Z✝.presheaf) (x✝¹ ≫ x✝)
      ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (x✝¹ ≫ x✝)) ⋯ =
    sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Y✝.presheaf) x✝¹
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x✝¹) ⋯ ≫
      sheafifyMap α (CategoryTheory.toSheafify J Y✝.presheaf) (CategoryTheory.toSheafify J Z✝.presheaf) x✝
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x✝) ⋯

Tactic:
ext1

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
X✝ Y✝ Z✝ : PresheafOfModules R₀
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Z✝.presheaf) (x✝¹ ≫ x✝)
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (x✝¹ ≫ x✝)) ⋯).val =
    (sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Y✝.presheaf) x✝¹
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x✝¹) ⋯ ≫
        sheafifyMap α (CategoryTheory.toSheafify J Y✝.presheaf) (CategoryTheory.toSheafify J Z✝.presheaf) x✝
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x✝) ⋯).val
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case refine_2.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : HasProjectiveDimensionLT X 0
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑0

Tactic:
exact ⟨⊥, fun _ _ ↦ hasProjectiveDimensionLT_of_ge _ 0 _ (by simp), by decide⟩

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

Goal state before:
pp: case refine_1
b₀✝ b₁✝ b₂✝ b₃✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
g✝ : b₁✝ ⟶ b₂✝
h✝ : b₂✝ ⟶ b₃✝
⊢ (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (f✝ ≫ g✝)) (Hom.hom h✝))).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom g✝))).hom
          (extendScalars (Hom.hom h✝)).toCatHom ≫
        (Bicategory.associator (extendScalars (Hom.hom f✝)).toCatHom (extendScalars (Hom.hom g✝)).toCatHom
              (extendScalars (Hom.hom h✝)).toCatHom).hom ≫
          Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom
              (Cat.Hom.isoMk (extendScalarsComp (Hom.hom g✝) (Hom.hom h✝))).inv ≫
            (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (g✝ ≫ h✝)))).inv =
    eqToHom ⋯

Tactic:
ext1

Goal state after:
case refine_1
b₀✝ b₁✝ b₂✝ b₃✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
g✝ : b₁✝ ⟶ b₂✝
h✝ : b₂✝ ⟶ b₃✝
⊢ ((Cat.Hom.isoMk (extendScalarsComp (Hom.hom (f✝ ≫ g✝)) (Hom.hom h✝))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom g✝))).hom
            (extendScalars (Hom.hom h✝)).toCatHom ≫
          (Bicategory.associator (extendScalars (Hom.hom f✝)).toCatHom (extendScalars (Hom.hom g✝)).toCatHom
                (extendScalars (Hom.hom h✝)).toCatHom).hom ≫
            Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom
                (Cat.Hom.isoMk (extendScalarsComp (Hom.hom g✝) (Hom.hom h✝))).inv ≫
              (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (g✝ ≫ h✝)))).inv).toNatTrans =
    (eqToHom ⋯).toNatTrans
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_2
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀✝)) (Hom.hom f✝))).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀✝)).hom (extendScalars (Hom.hom f✝)).toCatHom ≫
        (Bicategory.leftUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom =
    eqToHom ⋯

Tactic:
ext1

Goal state after:
case refine_2
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ ((Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀✝)) (Hom.hom f✝))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀✝)).hom (extendScalars (Hom.hom f✝)).toCatHom ≫
          (Bicategory.leftUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom).toNatTrans =
    (eqToHom ⋯).toNatTrans