mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
g : (free R).obj (yoneda.obj X) ⟶ M
⊢ (ModuleCat.Hom.hom (f₁.app (Opposite.op X))) (freeYonedaEquiv g) =
    (ModuleCat.Hom.hom (f₂.app (Opposite.op X))) (freeYonedaEquiv g)

Tactic:
exact congr_arg freeYonedaEquiv (h _ ⟨X⟩ g)

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
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : limit.π ((curry.obj G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂) = limit.π ((curry.obj G).obj x.1) y.2
⊢ 𝟙 (limit (curry.obj G ⋙ lim)) ≫ limit.π (curry.obj G ⋙ lim) y.1 ≫ limit.π ((curry.obj G).obj y.1) y.2 =
    (limit.π (curry.obj G ⋙ lim) x.1 ≫ limit.π ((curry.obj G).obj x.1) x.2) ≫ G.map (f₁, f₂)

Tactic:
rw [← limit.w (F := curry.obj G ⋙ lim) (f := f₁)]

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
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : limit.π ((curry.obj G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂) = limit.π ((curry.obj G).obj x.1) y.2
⊢ 𝟙 (limit (curry.obj G ⋙ lim)) ≫
      (limit.π (curry.obj G ⋙ lim) x.1 ≫ (curry.obj G ⋙ lim).map f₁) ≫ limit.π ((curry.obj G).obj y.1) y.2 =
    (limit.π (curry.obj G ⋙ lim) x.1 ≫ limit.π ((curry.obj G).obj x.1) x.2) ≫ G.map (f₁, f₂)
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
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
Q' : (j : J) → IsLimit (Q.obj j) := fun j ↦ limit.isLimit ((curry.obj G).obj j)
c' : Cone G
f : c'.pt ⟶ (coneOfHasLimitCurryCompLim G).pt
h : ∀ (j : J × K), f ≫ (coneOfHasLimitCurryCompLim G).π.app j = c'.π.app j
⊢ f = limit.lift (curry.obj G ⋙ lim) (coneOfConeCurry G Q' c')

Tactic:
by
      dsimp [coneOfHasLimitCurryCompLim] at f h ⊢
      refine limit.hom_ext (F := curry.obj G ⋙ lim) (fun j ↦ limit.hom_ext (fun k ↦ ?_))
      simp [h ⟨j, k⟩, Q']

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'
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
⊢ ∃ U_1 x_1 x'_1,
    ιM x_1 =
        ((ConcreteCategory.hom
              ((((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM')).ι.app U))
            (x, x')).1 ∧
      ιM x'_1 =
        ((ConcreteCategory.hom
              ((((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM')).ι.app U))
            (x, x')).2

Tactic:
exact ⟨U, x, x', rfl, rfl⟩

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''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
⊢ ∀ (m : ↑cR.pt) (x : ModuleColimit hcR hcM), φ (m • x) = m • φ x

Tactic:
refine (map_smul_homEquiv'_iff hcR hcM φ).1 (fun U r m ↦ ?_)

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''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ (ConcreteCategory.hom (((homEquiv' hcR hcM) φ).app U)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((homEquiv' hcR hcM) φ).app U)) m
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
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
⊢ (fun x ↦ (hom f) x = y) x' → x' = (hom ↑(Fork.IsLimit.lift' t y' hy')) PUnit.unit

Tactic:
hx'

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
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom f) x' = y
⊢ x' = (hom ↑(Fork.IsLimit.lift' t y' hy')) PUnit.unit
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
⊢ ((ofArrows Z g).bind fun x f H ↦ ofArrows (W f H) (k f H)) =
    ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
by
  funext Y
  ext f
  constructor
  · rintro ⟨_, _, _, ⟨i⟩, ⟨i'⟩, rfl⟩
    exact ofArrows.mk (Sigma.mk _ _)
  · rintro ⟨i⟩
    exact bind_comp _ (ofArrows.mk _) (ofArrows.mk _)

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ≤ R

Tactic:
rintro _ _ ⟨X, h⟩

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
Y : C
X : Over S
h : R X.hom
⊢ R { obj := X, property := h }.obj.hom
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ x₁ = x₂

Tactic:
rw [← extend_restrict t₁, ← extend_restrict t₂]
  congr

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
⊢ (x.map f).Compatible

Tactic:
by
  intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq
  unfold FamilyOfElements.map
  rwa [← NatTrans.naturality_apply, ← NatTrans.naturality_apply, h]

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : { x // x.Compatible }
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hf : f ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
e_1✝ : F.obj Z = F.obj (op (unop Z))
⊢ shrinkYonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map g)) f) =
    unop g ≫ shrinkYonedaObjObjEquiv f

Tactic:
simp only [Opposite.op_unop, shrinkYonedaObjObjEquiv_obj_map]

Goal state after:
case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : { x // x.Compatible }
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hf : f ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
e_1✝ : F.obj Z = F.obj (op (unop Z))
⊢ g.unop ≫ shrinkYonedaObjObjEquiv f = unop g ≫ shrinkYonedaObjObjEquiv f
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
H : J = ⊤
F : Sheaf J A
⊢ IsTerminal F

Tactic:
by
  refine IsTerminal.isTerminalOfObj (sheafToPresheaf _ _) _ ?_
  refine Functor.isTerminal fun X ↦ Sheaf.isTerminalOfBotCover _ _ ?_
  simp [H]

Goal state after:
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
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
⊢ IsLimit (s.mapCone (Fork.ofι (forkMap R P) ⋯)) ≃ IsLimit (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯)

Tactic:
let e : parallelPair (s.map (firstMap R P)) (s.map (secondMap R P)) ≅
    parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R)
      (Equalizer.Presieve.secondMap (P ⋙ s) R) := by
    refine parallelPair.ext (PreservesProduct.iso s _) ((PreservesProduct.iso s _))
      (limit.hom_ext (fun j => ?_)) (limit.hom_ext (fun j => ?_))
    · dsimp [Equalizer.Presieve.firstMap, firstMap]
      simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt,
        Fan.mk_π_app, assoc, piComparison_comp_π_assoc]
    · dsimp [Equalizer.Presieve.secondMap, secondMap]
      simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt,
        Fan.mk_π_app, assoc, piComparison_comp_π_assoc]

Goal state after:
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
e : parallelPair (s.map (firstMap R P)) (s.map (secondMap R P)) ≅
  parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext (PreservesProduct.iso s fun f ↦ P.obj (op f.fst))
    (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) ⋯ ⋯
⊢ IsLimit (s.mapCone (Fork.ofι (forkMap R P) ⋯)) ≃ IsLimit (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯)
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 : Sheaf J D
⊢ ((sheafificationAdjunction J D).counit.app P).hom = sheafifyLift J (𝟙 P.obj) ⋯

Tactic:
unfold sheafifyLift

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 : Sheaf J D
⊢ ((sheafificationAdjunction J D).counit.app P).hom =
    (((sheafificationAdjunction J D).homEquiv P.obj { obj := P.obj, property := ⋯ }).symm (𝟙 P.obj)).hom
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
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)
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
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := S.bind T
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := meqOfSep P hsep X S s T t ht
I : S.Arrow
II : (T I).Arrow
e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯
IV : ((J.pullback II.f).obj (T I)).Arrow
IA : B.Arrow := { Y := IV.Y, f := (IV.f ≫ II.f) ≫ I.f, hf := ⋯ }
IB : S.Arrow := IA.fromMiddle
IC : (T IB).Arrow := IA.toMiddle
ID : (T I).Arrow := { Y := IV.Y, f := IV.f ≫ II.f, hf := ⋯ }
IR : S.Relation := { fst := IB, snd := I, r := { Z := IA.Y, g₁ := IA.toMiddleHom, g₂ := IV.f ≫ II.f, w := ⋯ } }
⊢ (ConcreteCategory.hom ((J.plusObj P).map IC.f.op)) (↑s IB) = (ConcreteCategory.hom ((J.plusObj P).map ID.f.op)) (↑s I)

Tactic:
exact s.condition IR

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
ι : Type u_5
inst✝ : Category.{v_2, u_3} C
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ 𝟙 (F.obj { as := i }) ≫ α.app { as := i } = α.app { as := i } ≫ 𝟙 (G.obj { as := i })

Tactic:
by rw [Category.id_comp, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
inst✝ : Category.{v_2, u_3} C
ι : Type u_6
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ 𝟙 (F.obj { as := i }) ≫ α.app { as := i } = α.app { as := i } ≫ 𝟙 (G.obj { as := i })

Tactic:
by rw [Category.id_comp, Category.comp_id]

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

Goal state before:
pp: case mpr
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U) →
    ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)

Tactic:
rintro h (_ | _)

Goal state after:
case mpr.zero
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app WalkingParallelPair.zero)) ⁻¹' U)

case mpr.one
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app WalkingParallelPair.one)) ⁻¹' U)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
let X := F.obj ⟨WalkingPair.left⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
⊢ IsVanKampenColimit c
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
this :
  ∀ (i : Discrete WalkingPair) (Z : C) (f : Z ⟶ X ⨿ Y),
    PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app i)) F
⊢ IsVanKampenColimit (BinaryCofan.mk coprod.inl coprod.inr)

Tactic:
refine (FinitaryExtensive.vanKampen _
    (isColimitOfPreserves F (coprodIsCoprod X Y))).of_mapCocone F

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit
    (extendCofan (Cofan.mk (∐ fun i ↦ f i.succ) (Sigma.ι fun i ↦ f i.succ)) (BinaryCofan.mk coprod.inl coprod.inr))

Tactic:
apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit (Cofan.mk (∐ fun i ↦ f i.succ) (Sigma.ι fun i ↦ f i.succ))

C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit (BinaryCofan.mk coprod.inl coprod.inr)

C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    HasPullback (BinaryCofan.mk coprod.inl coprod.inr).inr i
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
e : ∐ f ≅ f i ⨿ ∐ fun j ↦ f ↑j :=
  { hom := Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j), hom_inv_id := ⋯, inv_hom_id := ⋯ }
e' : c.pt ≅ f i ⨿ ∐ fun j ↦ f ↑j := hc.coconePointUniqueUpToIso (getColimitCocone (Discrete.functor f)).isColimit ≪≫ e
⊢ HasPullback g (c.ι.app { as := i })

Tactic:
have : coprod.inl ≫ e'.inv = c.ι.app ⟨i⟩ := by
    simp only [e, e', Iso.trans_inv, coprod.desc_comp, colimit.ι_desc,
      BinaryCofan.ι_app_left, BinaryCofan.mk_inl]
    exact colimit.comp_coconePointUniqueUpToIso_inv _ _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
e : ∐ f ≅ f i ⨿ ∐ fun j ↦ f ↑j :=
  { hom := Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j), hom_inv_id := ⋯, inv_hom_id := ⋯ }
e' : c.pt ≅ f i ⨿ ∐ fun j ↦ f ↑j := hc.coconePointUniqueUpToIso (getColimitCocone (Discrete.functor f)).isColimit ≪≫ e
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ HasPullback g (c.ι.app { as := i })
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
      (G'.associator F' G').hom ≫ G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F') =
    NatTrans.id (𝟭 D₁ ⋙ G')

Tactic:
apply natTrans_ext L₁ W₁
        intro X₁
        have eq := adj.left_triangle_components X₁
        rw [NatTrans.comp_app, NatTrans.comp_app, whiskerRight_app, Localization.ε_app,
          Functor.associator_hom_app, id_comp, whiskerLeft_app, G'.map_comp, G'.map_comp,
          assoc, assoc]
        erw [(Localization.η adj L₁ L₂ W₂ G' F').naturality, Localization.η_app,
          assoc, assoc, ← G'.map_comp_assoc, ← G'.map_comp_assoc, assoc, Iso.hom_inv_id_app,
          comp_id, (CatCommSq.iso G L₁ L₂ G').inv.naturality_assoc, ← L₂.map_comp_assoc, eq,
          L₂.map_id, id_comp, Iso.inv_hom_id_app]
        rfl

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

Goal state before:
pp: J : Type v'
inst✝⁴ : Category.{u', v'} J
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✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (fst a b) (snd a b) := inr (fst a b) (snd a b)
this✝¹ : Mono u := mono_of_isPushout_of_mono_right (of_hasPushout (fst a b) (snd a b))
this✝ : Mono v := mono_of_isPushout_of_mono_left (of_hasPushout (fst a b) (snd a b))
sq_f_u : IsPullback (fst f u) (snd f u) f u := of_hasPullback f u
sq_f_v : IsPullback (fst f v) (snd f v) f v := of_hasPullback f v
sq_g_u : IsPullback (fst g u) (snd g u) g u := of_hasPullback g u
sq_g_v : IsPullback (fst g v) (snd g v) g v := of_hasPullback g v
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := Eq.mpr (id (congrArg (fun _a ↦ Mono _a) (Eq.symm (isoPullback_hom_fst p₁)))) inferInstance
sq₂₁ : IsPullback (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := of_hasPullback m₂ l₁
sq₂₂ : IsPullback (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := of_hasPullback m₂ l₂
⊢ Mono (v ≫ pushout.desc a b ⋯)

Tactic:
by rwa [pushout.inr_desc]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
⊢ W ≤ W.isLocal.isLocal

Tactic:
ObjectProperty.le_isLocal_iff

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
⊢ W.isLocal ≤ W.isLocal