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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
⊢ ((F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2) ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    ((D.obj p.1).ι.app p.2 ≫ s.ι.app p.1) ≫ 𝟙 s.pt

Tactic:
simp only [Category.assoc]

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
⊢ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2 ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1 ≫ 𝟙 s.pt
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
⊢ (uncurry.obj F).map f ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    ((D.obj p.1).ι.app p.2 ≫ s.ι.app p.1) ≫ ((const (J × K)).obj s.pt).map f

Tactic:
dsimp; simp only [Category.assoc]
              rcases p with ⟨j, k⟩
              rcases p' with ⟨j', k'⟩
              rcases f with ⟨fj, fk⟩
              dsimp
              slice_lhs 2 3 => rw [(D.obj j').ι.naturality]
              simp only [Functor.const_obj_map, Category.assoc]
              have w := (D.map fj).w k
              dsimp at w
              slice_lhs 1 2 => rw [← w]
              have n := s.ι.naturality fj
              dsimp at n
              simp only [Category.comp_id] at n
              rw [← n]
              simp

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (colimit.ι G (j, k) ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
HasColimit.ι_isoOfEquivalence_inv

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (G.map ((Prod.braiding K J).counitInv.app (j, k)) ≫
        (Iso.refl (Prod.swap K J ⋙ G)).hom.app ((Prod.braiding K J).inverse.obj (j, k)) ≫
          colimit.ι (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k))) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m₁ : ↑(M₁.obj X)
⊢ ∀ (m₂ : ↑(M₁.obj X)) (n : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) (m₁ + m₂) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n =
      (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n +
        (ConcreteCategory.hom (M₁.map f)) m₂ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n

Tactic:
m₁'

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m₁ m₁' : ↑(M₁.obj X)
⊢ ∀ (n : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) (m₁ + m₁') ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n =
      (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n +
        (ConcreteCategory.hom (M₁.map f)) m₁' ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (α_ x✝¹ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom = (ρ_ x✝¹).hom ▷ x✝

Tactic:
by ext1; apply triangle

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) =
    Presieve.ofArrows (fun p ↦ Y (incl p.fst) (fibincl p.fst p.snd)) fun p ↦
      g (incl p.fst) (fibincl p.fst p.snd) ≫ f (incl p.fst)

Tactic:
refine le_antisymm (fun T u hu ↦ ?_) fun T u ⟨p⟩ ↦ .mk (Sigma.mk (incl p.1) (fibincl p.1 p.2))
    exact .mk' ⟨Sum.inr ⟨⟨_, _⟩, hu⟩, .inl ⟨⟩⟩ hu.obj_idx.symm hu.eq_eqToHom_comp_hom_idx

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C = ⊤

Tactic:
by
      apply le_antisymm
      · exact (completeLatticeOfInf _ isGLB_sInf).le_top (discrete C)
      · intro X S _
        apply Set.mem_univ

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ (Presieve.singleton g).bind Ti ∈ {S | ∃ Y f, ∃ (_ : IsIso f), S = Presieve.singleton f}

Tactic:
refine ⟨_, f ≫ g, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ IsIso (f ≫ g)

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
⊢ ∃! x, (hom f) x = y

Tactic:
let y' : PUnit ⟶ Y := ↾fun _ => y

Goal state after:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
⊢ ∃! x, (hom f) x = y
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g → f = g

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g

Tactic:
· rintro ⟨a, rfl⟩
    rfl

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ ∃ i h, g = h ≫ f i

Tactic:
obtain ⟨_, h, _, ⟨i⟩, rfl⟩ := hg

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y✝ : I → C
f : (i : I) → Y✝ i ⟶ X
W Y : C
i : I
h : W ⟶ Y✝ i
⊢ ∃ i_1 h_1, h ≫ f i = h_1 ≫ f i_1
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
R : Presieve X
⊢ generate (Presieve.pushforward f R) = pushforward f (generate R)

Tactic:
ext
  grind [generate_apply, Presieve.pushforward, pushforward_apply]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
⊢ functorPushforward (𝟭 C) R = R

Tactic:
by
  ext X f
  constructor
  · intro hf
    obtain ⟨X, g, h, hg, rfl⟩ := hf
    exact R.downward_closed hg h
  · intro hf
    exact ⟨X, f, 𝟙 _, hf, by simp⟩

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

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (J.Cover (unop X))ᵒᵖ
⊢ Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index P) ((J.diagram P (unop X)).obj j✝)
        (fun I ↦ Multiequalizer.ι ((unop j✝).index P) (Cover.Arrow.base I)) ⋯ ≫
      (J.diagramNatTrans η (unop Y)).app ((J.pullback f.unop).op.obj j✝) =
    (J.diagramNatTrans η (unop X)).app j✝ ≫
      Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index Q) ((J.diagram Q (unop X)).obj j✝)
        (fun I ↦ Multiequalizer.ι ((unop j✝).index Q) (Cover.Arrow.base I)) ⋯

Tactic:
exact Multiequalizer.hom_ext _ _ _ (fun I => by simp)

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

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
I : (unop (op ((J.pullback f.unop).obj ⊤))).shape.L
⊢ ((P.map f ≫ Multiequalizer.lift (⊤.index P) (P.obj (op (unop Y))) (fun I ↦ P.map I.f.op) ⋯) ≫
        (J.diagram P (unop Y)).map e.op) ≫
      Multiequalizer.ι ((unop (op ((J.pullback f.unop).obj ⊤))).index P) I =
    (Multiequalizer.lift (⊤.index P) (P.obj (op (unop X))) (fun I ↦ P.map I.f.op) ⋯ ≫
        Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P) ((J.diagram P (unop X)).obj (op ⊤))
          (fun I ↦ Multiequalizer.ι (⊤.index P) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop (op ((J.pullback f.unop).obj ⊤))).index P) I

Tactic:
simp only [Category.assoc]

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
I : (unop (op ((J.pullback f.unop).obj ⊤))).shape.L
⊢ P.map f ≫
      Multiequalizer.lift (⊤.index P) (P.obj (op (unop Y))) (fun I ↦ P.map I.f.op) ⋯ ≫
        (J.diagram P (unop Y)).map e.op ≫ Multiequalizer.ι (((J.pullback f.unop).obj ⊤).index P) I =
    Multiequalizer.lift (⊤.index P) (P.obj (op (unop X))) (fun I ↦ P.map I.f.op) ⋯ ≫
      Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P) ((J.diagram P (unop X)).obj (op ⊤))
          (fun I ↦ Multiequalizer.ι (⊤.index P) (Cover.Arrow.base I)) ⋯ ≫
        Multiequalizer.ι (((J.pullback f.unop).obj ⊤).index P) I
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I ↦ Q.map I.f.op) ⋯ =
    Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I ↦ P.map I.f.op) ⋯ ≫
      (J.diagramNatTrans η (unop x✝)).app (op ⊤)

Tactic:
exact Multiequalizer.hom_ext _ _ _ (fun I => by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
⊢ IsIso (toRange p)

Tactic:
have := mono_of_mono_fac (toRange_ι p)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
⊢ IsIso (toRange p)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑((ConcreteCategory.hom ((homOfLe ⋯).app U)) s)).arrows i
this :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toFunctor.obj X),
    (ConcreteCategory.hom (f.app Y)) ((ConcreteCategory.hom (G.toFunctor.map f_1)) x) =
      (ConcreteCategory.hom (F'.map f_1)) ((ConcreteCategory.hom (f.app X)) x)
⊢ (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s) =
    (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom (f.app U)).toFun s)

Tactic:
exact (Presieve.IsSheafFor.valid_glue (h _ ((homOfLe (_ : _ ≤ sheafify _ _)).app _ _).2)
    ((G.family_of_elements_compatible _).map _) _ _).trans (this _ _)

Goal state after:
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ ((F.map
            (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
              (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
          F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop)))) ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
            (colimit.isColimit (J.diagram P (unop Y) ⋙ F))).hom) ≫
      (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    (((colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫
          (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom) ≫
        colimMap (J.diagramPullback (P ⋙ F) f.unop)) ≫
      colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op

Tactic:
simp only [Category.assoc]

Goal state after:
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
          (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
      F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))) ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
              (colimit.isColimit (J.diagram P (unop Y) ⋙ F))).hom ≫
          (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    (colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫
      (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
        colimMap (J.diagramPullback (P ⋙ F) f.unop) ≫ colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op
Module: Mathlib.CategoryTheory.Sites.Sheafification

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
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ η = γ

Tactic:
rw [sheafifyLift_unique J _ hQ _ h, ← h]
  exact (sheafifyLift_unique J _ hQ _ h.symm).symm

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

Goal state before:
pp: case e_a
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a✝ : ((unop W).pullback f.unop).shape.L
⊢ (F.map
          (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
        (J.diagramCompIso F P (unop Y)).hom.app (op ((unop W).pullback f.unop))) ≫
      Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a✝ =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift (((unop W).pullback f.unop).index (P ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun I ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) I.base) ⋯) ≫
      Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a✝

Tactic:
simp only [Category.assoc]

Goal state after:
case e_a
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a✝ : ((unop W).pullback f.unop).shape.L
⊢ F.map
        (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
          (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
      (J.diagramCompIso F P (unop Y)).hom.app (op ((unop W).pullback f.unop)) ≫
        Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a✝ =
    (J.diagramCompIso F P (unop X)).hom.app W ≫
      Multiequalizer.lift (((unop W).pullback f.unop).index (P ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun I ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) I.base) ⋯ ≫
        Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a✝
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ (S.ι (W.shape.fst i) ≫ (E.π.app k).app (op (W.shape.fst i).Y)) ≫ (W.index (F.obj k).obj).fst i =
    (S.ι (W.shape.snd i) ≫ (E.π.app k).app (op (W.shape.snd i).Y)) ≫ (W.index (F.obj k).obj).snd i

Tactic:
simp only [Category.assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ S.ι (W.shape.fst i) ≫ (E.π.app k).app (op (W.shape.fst i).Y) ≫ (W.index (F.obj k).obj).fst i =
    S.ι (W.shape.snd i) ≫ (E.π.app k).app (op (W.shape.snd i).Y) ≫ (W.index (F.obj k).obj).snd i
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
⊢ ((sheafificationAdjunction J D).counit.app (F.obj k)).hom ≫
      ((inv (sheafificationAdjunction J D).counit).app (F.obj k)).hom ≫ ((presheafToSheaf J D).map (E.ι.app k)).hom =
    ((sheafificationAdjunction J D).counit.app (F.obj k)).hom ≫ E.ι.app k ≫ toSheafify J E.pt

Tactic:
rw [← ObjectProperty.FullSubcategory.comp_hom_assoc,
    ← NatTrans.comp_app, IsIso.hom_inv_id, NatTrans.id_app]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
⊢ (𝟙 ((sheafToPresheaf J D ⋙ presheafToSheaf J D).obj (F.obj k))).hom ≫ ((presheafToSheaf J D).map (E.ι.app k)).hom =
    ((sheafificationAdjunction J D).counit.app (F.obj k)).hom ≫ E.ι.app k ≫ toSheafify J E.pt
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Tactic:
convert! h.comp (TopCat.homeoOfIso (asIso f).symm).isOpenEmbedding

Goal state after:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
⊢ ⇑(ConcreteCategory.hom g) = ⇑(ConcreteCategory.hom (f ≫ g)) ∘ ⇑(homeoOfIso (asIso f).symm)