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 (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cocone (uncurry.obj F) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
p : J × K
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p

Tactic:
have h1 := (Q p.1).fac ((Cocone.precompose (E p.1).inv).obj <|
        s.whisker (Prod.sectR p.1 K)) p.2

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 (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cocone (uncurry.obj F) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
p : J × K
h1 :
  (D.obj p.1).ι.app p.2 ≫ (Q p.1).desc ((Cocone.precompose (E p.1).inv).obj (Cocone.whisker (Prod.sectR p.1 K) s)) =
    ((Cocone.precompose (E p.1).inv).obj (Cocone.whisker (Prod.sectR p.1 K) s)).ι.app p.2
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p
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✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) = limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k

Tactic:
rw [← cancel_epi (limitIsoLimitCurryCompLim G).hom]
  simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'✝ : PresheafOfModules R
cM'✝ : Cocone M'✝.presheaf
hcM'✝ : IsColimit cM'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) ((ιR cR) r • ιM m) =
    (ιR cR) r • (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) (ιM m)

Tactic:
rw [ModuleColimit.smul_eq]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'✝ : PresheafOfModules R
cM'✝ : Cocone M'✝.presheaf
hcM'✝ : IsColimit cM'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) (ιM (r • m)) =
    (ιR cR) r • (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) (ιM m)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
F : PresheafOfModules R
G : ModuleCat ↑cR.pt
β : F ⟶ (constFunctor cR).obj G
X : Cᵒᵖ
m : ↑(F.obj X)
⊢ (ConcreteCategory.hom ((↑(homEquiv hcR (colimit.isColimit F.presheaf))).symm β)) (ιM m) =
    (ConcreteCategory.hom (β.app X)) m

Tactic:
apply homEquiv_symm_apply

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

Goal state before:
pp: case e'_5
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g✝ : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g✝ (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
Z : C
g : Z ⟶ Y
hg : Presieve.ofArrows P p₁ g
⊢ Presieve.ofArrows (P ∘ a) (fun i ↦ p₁ (a i)) g

Tactic:
exact .mk' (Sum.inr ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch)

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ trivial C ≤ ⊥

Tactic:
intro X S hS
        rw [trivial_covering] at hS
        apply covering_of_eq_top _ hS

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝¹ : PreservesLimitsOfShape WalkingCospan F
inst✝ : J.IsStableUnderBaseChange
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
hf : Presieve.ofArrows Y f ∈ (comap F J).coverings S
Z : C
g : Z ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Z
p₂ : (i : ι) → P i ⟶ Y i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ (comap F J).coverings Z

Tactic:
by
    simp only [mem_comap_iff, Presieve.map_ofArrows] at hf ⊢
    exact mem_coverings_of_isPullback _ hf _ _ _
      fun i ↦ CategoryTheory.Functor.map_isPullback F (h i)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₂
⊢ ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j)) z₁ =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j)) z₂

Tactic:
rintro ⟨⟨Y, Z, g, f, hf⟩⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₂
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) { as := ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ })) z₁ =
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) { as := ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ })) z₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
⊢ (FamilyOfElements.functorPullback F x).Compatible

Tactic:
intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq
  exact h (F.map g₁) (F.map g₂) h₁ h₂ (by simp only [← F.map_comp, eq])

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map (↑fg.1.snd).op ≫ P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝

Tactic:
← P.map_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map ((↑fg.1.snd).op ≫ (pullback.fst ↑fg.1.snd ↑fg.2.snd).op))).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map f.op ≫ P.map (pullback.fst f g).op = P.map g.op ≫ P.map (pullback.snd f g).op

Tactic:
← P.map_comp,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map (f.op ≫ (pullback.fst f g).op) = P.map g.op ≫ P.map (pullback.snd f g).op
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })
⊢ (s.map (Pi.lift fun x ↦ Pi.π (fun f ↦ P.obj (op f.fst)) x.1 ≫ P.map (pullback.fst ↑x.1.snd ↑x.2.snd).op) ≫
        piComparison s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) ≫
      limit.π (Discrete.functor fun fg ↦ s.obj (P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))) j =
    ((piComparison s fun f ↦ P.obj (op f.fst)) ≫
        Pi.lift fun fg ↦
          Pi.π (fun f ↦ s.obj (P.obj (op f.fst))) fg.1 ≫ s.map (P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd).op)) ≫
      limit.π (Discrete.functor fun fg ↦ s.obj (P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))) j

Tactic:
simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt,
        Fan.mk_π_app, assoc, piComparison_comp_π_assoc]

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })
⊢ (s.map (Pi.lift fun x ↦ Pi.π (fun f ↦ P.obj (op f.fst)) x.2 ≫ P.map (pullback.snd ↑x.1.snd ↑x.2.snd).op) ≫
        piComparison s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) ≫
      limit.π (Discrete.functor fun fg ↦ s.obj (P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))) j =
    ((piComparison s fun f ↦ P.obj (op f.fst)) ≫
        Pi.lift fun fg ↦
          Pi.π (fun f ↦ s.obj (P.obj (op f.fst))) fg.2 ≫ s.map (P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)) ≫
      limit.π (Discrete.functor fun fg ↦ s.obj (P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))) j

Tactic:
simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt,
        Fan.mk_π_app, assoc, piComparison_comp_π_assoc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs : s ∈ {s | G.sieveOfSection s ∈ J (unop U)}
⊢ Sieve.pullback i.unop (G.sieveOfSection s) ≤ G.sieveOfSection ((ConcreteCategory.hom (F.map i)) s)

Tactic:
intro _ _ h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs : s ∈ {s | G.sieveOfSection s ∈ J (unop U)}
Y✝ : C
f✝ : Y✝ ⟶ unop V
h : (Sieve.pullback i.unop (G.sieveOfSection s)).arrows f✝
⊢ (G.sieveOfSection ((ConcreteCategory.hom (F.map i)) s)).arrows f✝
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s

Tactic:
apply (h _ hs).isSeparatedFor.ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection s).arrows f →
      (ConcreteCategory.hom (F.map f.op)) ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) =
        (ConcreteCategory.hom (F.map f.op)) s
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presheaf.IsSheaf J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor

Tactic:
by
    rw [isSheaf_iff_isSheaf_of_type]
    apply Subfunctor.sheafify_isSheaf
    rw [← isSheaf_iff_isSheaf_of_type]
    exact F'.2

Goal state after:
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
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toSheafify J P ≫ sheafifyLift J η hQ = η

Tactic:
toSheafify,

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
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (sheafificationAdjunction J D).unit.app P ≫ sheafifyLift J η hQ = η
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.left } = S.π.app { as := WalkingPair.left }
x : ↑S.pt
⊢ ((ConcreteCategory.hom m) x).1 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).1

Tactic:
apply_fun fun e => e x at h

Goal state after:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
x : ↑S.pt
h :
  (ConcreteCategory.hom (m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.left })) x =
    (ConcreteCategory.hom (S.π.app { as := WalkingPair.left })) x
⊢ ((ConcreteCategory.hom m) x).1 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).1
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.right } = S.π.app { as := WalkingPair.right }
x : ↑S.pt
⊢ ((ConcreteCategory.hom m) x).2 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).2

Tactic:
apply_fun fun e => e x at h

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
x : ↑S.pt
h :
  (ConcreteCategory.hom (m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.right })) x =
    (ConcreteCategory.hom (S.π.app { as := WalkingPair.right })) x
⊢ ((ConcreteCategory.hom m) x).2 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).2
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom (i₁ ≫ g₁)) x₁ = (ConcreteCategory.hom (f₂ ≫ i₃)) x₂

Tactic:
eq₂,

Goal state after:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom (i₁ ≫ g₁)) x₁ = (ConcreteCategory.hom (i₂ ≫ g₂)) x₂
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
⊢ x ∈ ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U →
    x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U

Tactic:
rintro ⟨y, hy, eq⟩
  -- next 5 lines were
  -- `exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, by simpa, by simp⟩` before https://github.com/leanprover-community/mathlib4/pull/13170
    refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, ?_, ?_⟩
    · simp only [coe_of, Set.mem_preimage]
      convert! hy
      rw [pullbackIsoProdSubtype_inv_fst_apply]
    · rw [pullbackIsoProdSubtype_inv_snd_apply]

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

Goal state before:
pp: case mpr.refine_4
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
m : c.pt ⟶ T
x : ↑c.pt
⊢ (ConcreteCategory.hom m) x =
    if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
      (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
    else (ConcreteCategory.hom (c.inr ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)

Tactic:
split_ifs

Goal state after:
case pos
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
m : c.pt ⟶ T
x : ↑c.pt
h✝ : x ∈ range ⇑(ConcreteCategory.hom c.inl)
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h✝⟩)

case neg
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
m : c.pt ⟶ T
x : ↑c.pt
h✝ : x ∉ range ⇑(ConcreteCategory.hom c.inl)
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom (c.inr ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
⊢ IsVanKampenColimit c

Tactic:
by
  intro F' c' α f e hα
  have := fun x => hc x (((evaluation C D).obj x).mapCocone c') (whiskerRight α _)
      (((evaluation C D).obj x).map f)
      (by
        ext y
        dsimp
        exact NatTrans.congr_app (NatTrans.congr_app e y) x)
      (hα.whiskerRight _)
  constructor
  · rintro ⟨hc'⟩ j
    refine ⟨⟨(NatTrans.congr_app e j).symm⟩, ⟨evaluationJointlyReflectsLimits _ ?_⟩⟩
    refine fun x => (isLimitMapConePullbackConeEquiv _ _).symm ?_
    exact ((this x).mp ⟨isColimitOfPreserves _ hc'⟩ _).isLimit
  · exact fun H => ⟨evaluationJointlyReflectsColimits _ fun x =>
      ((this x).mpr fun j => (H j).map ((evaluation C D).obj x)).some⟩

Goal state after: