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

Goal state before:
pp: case left
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))

Tactic:
intro x y h

Goal state after:
case left
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x y : (forget D).obj ((J.plusObj P).obj (op X))
h :
  (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) x =
    (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) y
⊢ x = y
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: X Y : TopCat
⊢ (X.prodIsoProd Y).inv ≫ prod.fst = prodFst

Tactic:
by simp [Iso.inv_comp_eq]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: X Y : TopCat
⊢ (X.prodIsoProd Y).inv ≫ prod.snd = prodSnd

Tactic:
by simp [Iso.inv_comp_eq]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
⊢ range ⇑(ConcreteCategory.hom (prod.map f g)) =
    ⇑(ConcreteCategory.hom prod.fst) ⁻¹' range ⇑(ConcreteCategory.hom f) ∩
      ⇑(ConcreteCategory.hom prod.snd) ⁻¹' range ⇑(ConcreteCategory.hom g)

Tactic:
ext x
  constructor
  · rintro ⟨y, rfl⟩
    simp_rw [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range, ← ConcreteCategory.comp_apply,
      Limits.prod.map_fst, Limits.prod.map_snd, ConcreteCategory.comp_apply, exists_apply_eq_apply,
      and_self_iff]
  · rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
    use (prodIsoProd W X).inv (x₁, x₂)
    apply Concrete.limit_ext
    rintro ⟨⟨⟩⟩
    · rw [← ConcreteCategory.comp_apply]
      erw [Limits.prod.map_fst]
      rw [ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_fst_apply]
      exact hx₁
    · rw [← ConcreteCategory.comp_apply]
      erw [Limits.prod.map_snd]
      rw [ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_snd_apply]
      exact hx₂

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

Goal state before:
pp: case intro
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
⊢ Function.Injective ⇑(ConcreteCategory.hom (colimitLimitToLimitColimit F))

Tactic:
intro x y h

Goal state after:
case intro
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
x y : colimit (curry.obj (swap K J ⋙ F) ⋙ lim)
h : (ConcreteCategory.hom (colimitLimitToLimitColimit F)) x = (ConcreteCategory.hom (colimitLimitToLimitColimit F)) y
⊢ x = y
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case neg.hf
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous (⇑⋯.toHomeomorph.symm ∘ Subtype.map (fun a ↦ a) this)

Tactic:
apply Continuous.comp (by fun_prop)

Goal state after:
case neg.hf
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous (Subtype.map (fun a ↦ a) this)
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ IsInitial
    (match i, j, hij with
      | WalkingPair.left, WalkingPair.right, hij => s
      | WalkingPair.right, WalkingPair.left, hij => s.flip).pt

Tactic:
split <;> exact H

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: 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
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPullbacksOfInclusions C
X Y Z : C
f : Z ⟶ X ⨿ Y
⊢ HasPullback f coprod.inr

Tactic:
have : IsPullback (𝟙 _) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom :=
    IsPullback.of_horiz_isIso ⟨by simp⟩

Goal state after:
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
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPullbacksOfInclusions C
X Y Z : C
f : Z ⟶ X ⨿ Y
this : IsPullback (𝟙 Z) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom
⊢ HasPullback f coprod.inr
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: 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
⊢ ⋯.IsVanKampen

Tactic:
introv W' hf hg hh hi w
  simpa only [IsPushout.flip_iff, IsPullback.flip_iff, and_comm] using
    H' g' f' i' h' αW αY αX αZ hg hf hi hh w.flip

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁.left
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
⊢ IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ f
    (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

pp: case h₁.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
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
⊢ IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ f
    (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
· refine ⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inl y := by
        intro x
        rcases h : s.fst x with val | val
        · simp
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαY val :).symm
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨↾(l), ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩
      · ext x
        exact (hl x).symm
      · ext x
        exact hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm

Goal state after:
case h₁.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
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
⊢ IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ f
    (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
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
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
⊢ ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'

Tactic:
exact H'.exists_cube_filling hh hi

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: 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
⊢ FinitaryExtensive (Type u)

Tactic:
by
  classical
  rw [finitaryExtensive_iff_of_isTerminal (Type u) PUnit Types.isTerminalPUnit _
      (Types.binaryCoproductColimit _ _)]
  apply BinaryCofan.isVanKampen_mk _ _ (fun X Y => Types.binaryCoproductColimit X Y) _
      fun f g => (Limits.Types.pullbackLimitCone f g).2
  · intro _ _ _ _ f hαX hαY
    constructor
    · refine ⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inl y := by
        intro x
        rcases h : s.fst x with val | val
        · simp
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαY val :).symm
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨↾(l), ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩
      · ext x
        exact (hl x).symm
      · ext x
        exact hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm
    · refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · simp
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨↾l, ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩
      · ext x
        exact (hl x).symm
      · ext x
        exact hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm
  · intro Z f
    dsimp [Limits.Types.binaryCoproductCocone]
    have : ∀ x, f x = Sum.inl PUnit.unit ∨ f x = Sum.inr PUnit.unit := by
      intro x
      rcases f x with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
      exacts [Or.inl rfl, Or.inr rfl]
    let eX : { p : Z × PUnit // f p.fst = Sum.inl p.snd } ≃ { x : Z // f x = Sum.inl PUnit.unit } :=
      ⟨fun p => ⟨p.1.1, by convert! p.2⟩, fun x => ⟨⟨_, _⟩, x.2⟩, fun _ => by ext; rfl,
        fun _ => by ext; rfl⟩
    let eY : { p : Z × PUnit // f p.fst = Sum.inr p.snd } ≃ { x : Z // f x = Sum.inr PUnit.unit } :=
      ⟨fun p => ⟨p.1.1, p.2.trans (congr_arg Sum.inr <| Subsingleton.elim _ _)⟩,
        fun x => ⟨⟨_, _⟩, x.2⟩, fun _ => by ext; rfl, fun _ => by ext; rfl⟩
    fapply BinaryCofan.isColimitMk
    · exact fun s => ↾fun x => dite _ (fun h => s.inl <| eX.symm ⟨x, h⟩)
        fun h => s.inr <| eY.symm ⟨x, (this x).resolve_left h⟩
    · intro s
      ext ⟨⟨x, ⟨⟩⟩, _⟩
      dsimp
      split_ifs with h <;> tauto
    · intro s
      ext ⟨⟨x, ⟨⟩⟩, hx⟩
      dsimp
      split_ifs with h
      · cases h.symm.trans hx
      · rfl
    · intro s m e₁ e₂
      ext x
      simp only [TypeCat.Fun.toFun_apply, Types.binaryCoproductCocone_pt, pair_obj_left,
        Functor.const_obj_obj, pair_obj_right, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
      split_ifs
      · rw [← e₁]
        rfl
      · rw [← e₂]
        rfl

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

Goal state before:
pp: case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (f ×ₘ 𝟙 k''))) ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) =
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')))) (y j')

Tactic:
simp only [← comp_apply, ← Functor.map_comp, prod_comp, id_comp, comp_id]

Goal state after:
case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j) =
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')))) (y j')
Module: Mathlib.CategoryTheory.ObjectProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
J : Type u'
inst✝ : Category.{v', u'} J
Z : C
x✝ : W.isLocal.limitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.LimitOfShape J Z
g₁ g₂ : Y ⟶ Z
h : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
j : J
⊢ (fun g ↦ f ≫ g) (g₁ ≫ { pt := Z, π := p.π }.π.app j) = (fun g ↦ f ≫ g) (g₂ ≫ { pt := Z, π := p.π }.π.app j)

Tactic:
simp [reassoc_of% h]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Tactic:
let W := ((MorphismProperty.isomorphisms C₂).inverseImage G)
  have hG : W.IsInvertedBy G := fun _ _ _ hf => hf
  have : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X) := fun X =>
    Localization.inverts W.Q W _ (by
      change IsIso _
      infer_instance)
  have : IsIso (whiskerRight adj.unit W.Q) := NatIso.isIso_of_isIso_app _
  let e : W.Localization ≌ C₂ := Equivalence.mk (Localization.lift G hG W.Q) (F ⋙ W.Q)
    (liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) _ _
    (W.Q.leftUnitor.symm ≪≫ asIso (whiskerRight adj.unit W.Q)))
    (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Localization.fac G hG W.Q) ≪≫
      asIso adj.counit)
  apply Functor.IsLocalization.of_equivalence_target W.Q W G e
    (Localization.fac G hG W.Q)

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

Goal state before:
pp: case refine_1
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
this✝¹ : PreservesColimitsOfSize.{?u.95, ?u.94, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    (Gl.mapCocone
      ((Cocone.precompose (spanCompIso Gr f g).hom).obj
        (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)))

pp: case refine_2
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
this✝¹ : PreservesColimitsOfSize.{?u.95, ?u.94, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))

Tactic:
· exact isColimitOfPreserves Gl ((IsColimit.precomposeHomEquiv _ _).symm <| pushoutIsPushout _ _)

Goal state after:
case refine_2
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
this✝¹ : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
Y : C
p : Y ⟶ Opposite.unop X
r : ↑(R.obj (Opposite.op Y))
hr : (ConcreteCategory.hom (α.app (Opposite.op Y))) r = (ConcreteCategory.hom (R'.map p.op)) r'
hg :
  ∀ (z : ↑(M₁.obj X)),
    (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) z) =
      (ConcreteCategory.hom (M₂.map p.op)) ((ConcreteCategory.hom (g.app X)) z)
⊢ (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) (r' • m)) =
    (ModuleCat.Hom.hom (g.app (Opposite.op Y))) (r • (ConcreteCategory.hom (M₁.map p.op)) m)

Tactic:
rw [M₁.map_smul, ← hr]

Goal state after:
C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
Y : C
p : Y ⟶ Opposite.unop X
r : ↑(R.obj (Opposite.op Y))
hr : (ConcreteCategory.hom (α.app (Opposite.op Y))) r = (ConcreteCategory.hom (R'.map p.op)) r'
hg :
  ∀ (z : ↑(M₁.obj X)),
    (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) z) =
      (ConcreteCategory.hom (M₂.map p.op)) ((ConcreteCategory.hom (g.app X)) z)
⊢ (ConcreteCategory.hom (g.app (Opposite.op Y)))
      ((ConcreteCategory.hom (α.app (Opposite.op Y))) r • (ConcreteCategory.hom (M₁.map p.op)) m) =
    (ModuleCat.Hom.hom (g.app (Opposite.op Y))) (r • (ConcreteCategory.hom (M₁.map p.op)) m)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
R : Cᵒᵖ ⥤ RingCat
F : D ⥤ PresheafOfModules R
inst✝¹ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
inst✝ : HasLimitsOfShape D AddCommGrpCat
hc : IsLimit c
hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf
⊢ Presheaf.IsSheaf J c.pt.presheaf

Tactic:
by
  let G : D ⥤ Sheaf J AddCommGrpCat.{v} :=
    { obj := fun j => ⟨(F.obj j).presheaf, hF j⟩
      map := fun φ => ⟨(PresheafOfModules.toPresheaf R).map (F.map φ)⟩ }
  exact Sheaf.isSheaf_of_isLimit G _ (isLimitOfPreserves (toPresheaf R) hc)

Goal state after: