mathlib-initiative/mathlib-tactics huggingface dataset:
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
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
inst✝ : HasPullback αX f
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
W : C
f₁ f₂ : Z' ⟶ W
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
h'_w : h' ≫ f₁ = h' ≫ f₂
i'_w : i' ≫ f₁ = i' ≫ f₂
⊢ f₁ = f₂

Tactic:
by
  obtain ⟨W', f', g', αW, _, _, H''⟩ := H'.exists_cube_filling hh hi
  exact H''.hom_ext h'_w i'_w

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

Goal state before:
pp: 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 (𝟙 j' ×ₘ i f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)) =
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ i f))) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j'))

Tactic:
by
            rw [← wf f]

Goal state after:
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
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ HasPullback g (coprod.inl ≫ e'.inv)

Tactic:
have : IsPullback (𝟙 _) (g ≫ e'.hom) g e'.inv := IsPullback.of_horiz_isIso ⟨by simp⟩

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
this✝ : coprod.inl ≫ e'.inv = c.ι.app { as := i }
this : IsPullback (𝟙 X) (g ≫ e'.hom) g e'.inv
⊢ HasPullback g (coprod.inl ≫ e'.inv)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case e'_3
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✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝¹ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this✝ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := ⋯
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := ⋯
hl : IsColimit ((Cocone.precompose β.hom).obj c') := ⋯
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := ⋯
this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
e_1✝ :
  (c'.pt ⟶ (Gl.mapCocone c).pt) =
    (((Cocone.precompose β.hom).obj c').pt ⟶ (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }).pt)
⊢ f = hl.desc (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })

Tactic:
· clear_value α'
      apply hl.hom_ext
      intro j
      rw [hl.fac]
      dsimp [β]
      simp only [Category.comp_id, hα'', Category.assoc, Gl.map_comp]
      congr 1
      exact (NatTrans.congr_app h j).symm

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ IsPullback (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))
    (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X j)) (c.inj i) (c.inj j)

Tactic:
by
  refine (hc (Cofan.mk (X i) (f := fun k ↦ if k = i then X i else ⊥_ C)
    (fun k ↦ if h : k = i then (eqToHom <| if_pos h) else (eqToHom <| if_neg h) ≫ initial.to _))
    (Discrete.natTrans (fun k ↦ if h : k.1 = i then (eqToHom <| (if_pos h).trans
      (congr_arg X h.symm)) else (eqToHom <| if_neg h) ≫ initial.to _))
    (c.inj i) ?_ (.of_discrete _)).mp ⟨?_⟩ ⟨j⟩
  · ext ⟨k⟩
    simp only [Discrete.functor_obj, Functor.const_obj_obj, NatTrans.comp_app,
      Discrete.natTrans_app, Cofan.mk_pt, Cofan.mk_ι_app, Functor.const_map_app]
    split
    · subst ‹k = i›; rfl
    · simp
  · refine Cofan.IsColimit.mk _ (fun t ↦ (eqToHom (if_pos rfl).symm) ≫ t.inj i) ?_ ?_
    · intro t j
      simp only [Cofan.mk_pt, cofan_mk_inj]
      split
      · subst ‹j = i›; simp
      · rw [Category.assoc, ← IsIso.eq_inv_comp]
        exact initialIsInitial.hom_ext _ _
    · intro t m hm
      simp [← hm i]

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

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
obj✝¹ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝¹ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝¹ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝¹ Y)
obj✝ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝ Y)
h : ∀ (X : Cᵒᵖ), { obj := obj✝¹, map := map✝¹ }.obj X = { obj := obj✝, map := map✝ }.obj X
X : Cᵒᵖ
⊢ obj✝¹ X = obj✝ X

Tactic:
exact h X

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
⊢ HasProjectiveDimensionLT X 1

Tactic:
let := HasExt.standard C
  rw [hasProjectiveDimensionLT_iff]
  intro i hi Y e
  obtain _ | i := i
  · simp at hi
  · exact e.eq_zero_of_projective

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext S.X₃ Y i
⊢ (Ext.mk₀ S.g).comp x₃ ⋯ = 0

Tactic:
rw [x₃.eq_zero_of_hasProjectiveDimensionLT n hi, Ext.comp_zero]

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

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ (toPresheaf R₀).map ((sheafificationHomEquiv α) f) =
    ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map f)

Tactic:
rw [toPresheaf_map_sheafificationHomEquiv_def, Adjunction.homEquiv_unit]
  dsimp

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
n : ℕ
inst✝ : HasProjectiveDimensionLE M n
⊢ HasProjectiveDimensionLE N n

Tactic:
induction n generalizing M N e' with
  | zero =>
    have : HasProjectiveDimensionLE M 0 := ‹_›
    simp only [HasProjectiveDimensionLE, zero_add] at this ⊢
    rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at this ⊢
    exact Projective.of_equiv e'
  | succ n ih =>
    let S := M.projectiveShortComplex
    let S' := N.projectiveShortComplex
    have S_exact := M.shortExact_projectiveShortComplex
    have S'_exact := N.shortExact_projectiveShortComplex
    let eR : Shrink.{v} R ≃ₛₗ[RingHomClass.toRingHom e] Shrink.{v'} R' :=
      ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
    let e2 : S.X₂ ≃ₛₗ[RingHomClass.toRingHom e] S'.X₂ :=
      (Finsupp.mapDomain.linearEquiv (Shrink R) R e').trans (Finsupp.mapRange.linearEquiv eR)
    have comm : S'.g.hom.comp e2.toLinearMap = e'.toLinearMap.comp S.g.hom := by
      ext m r
      simp [S, S', e2, eR, Basis.constr_apply, map_smulₛₗ]
    have : S.g.hom.ker = Submodule.comap e2.toLinearMap S'.g.hom.ker := by
      rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]
    rw [Submodule.comap_equiv_eq_map_symm] at this
    let eker : S.X₁ ≃ₛₗ[RingHomClass.toRingHom e] S'.X₁ :=
      (LinearEquiv.ofEq _ _ this).trans (e2.symm.submoduleMap S'.g.hom.ker).symm
    have := (S_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mp ‹_›
    exact (S'_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mpr (ih eker)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
⊢ f₁ = f₂

Tactic:
let α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
    { app := fun X => eqToHom (by simp [← h₁]) }

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
⊢ f₁ = f₂
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Z : C
g : Z ⟶ S
val✝ : F.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f (Sum.inr val✝))

Tactic:
· exact Or.inr (.mk _)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a.inl
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : E.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (E.f i)

pp: case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : F.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (F.f i)

Tactic:
· exact ⟨Sum.inl i⟩

Goal state after:
case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : F.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (F.f i)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
let g' : A' ⟶ B' := StructuredArrow.homMk g.right
      congr($(IsCofiltered.eq_condition (T.map f) (T.map g)).right).symm

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ ∃ W h, h ≫ f = h ≫ g
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mp
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J → K ≤ J.toCoverage

pp: case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K ≤ J.toCoverage → K.toGrothendieck ≤ J

Tactic:
· intro H X S hS
      exact H _ <| Saturate.of _ _ hS

Goal state after:
case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K ≤ J.toCoverage → K.toGrothendieck ≤ J
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
⊢ whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫
      (L.associator (L.pointwiseLeftKanExtension F) G).hom ≫
        L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom =
    L.pointwiseLeftKanExtensionUnit (F ⋙ G)

Tactic:
by
  simpa [pointwiseLeftKanExtensionCompIsoOfPreserves] using
    descOfIsLeftKanExtension_fac
      (α := whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom)
      (β := L.pointwiseLeftKanExtensionUnit <| F ⋙ G)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i ≅
      (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).left
        i

Tactic:
exact fun _ ↦ .refl _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i ≅
      (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).right
        i

Tactic:
exact fun _ ↦ .refl _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
⊢ functorPullback (Over.forget X) (map (Over.forget X) S) = S

Tactic:
let R : Presieve Y.left := fun Z g ↦ S (Over.homMk g : Over.mk (g ≫ Y.hom) ⟶ Y)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
⊢ functorPullback (Over.forget X) (map (Over.forget X) S) = S
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

Tactic:
let s := fun (X : C) => (H _ (hY X)).amalgamate _
      (hx.familyOfElements_isCompatible X)
    have hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i) := fun {X} i f => by
      have h := Presieve.IsSheafFor.valid_glue (H _ (hY X))
          (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩
      simp only [op_id, F.map_id, types_id_apply] at h
      exact h.trans (hx.familyOfElements_apply _ _ _)
    have hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (_ : W ⟶ Y i), F.map a.op (s X) = s W := by
      intro W X a i b
      rw [hs i b]
      exact (Presieve.IsSheafFor.valid_glue (H _ (hY X))
        (hx.familyOfElements_isCompatible _) a ⟨i, ⟨b⟩⟩).trans (familyOfElements_apply hx _ _ _)
    refine ⟨⟨fun X => s X.unop, ?_⟩, fun i => (hs i (𝟙 (Y i))).trans (by simp)⟩
    rintro ⟨Y₁⟩ ⟨Y₂⟩ ⟨f : Y₂ ⟶ Y₁⟩
    change F.map f.op (s Y₁) = s Y₂
    apply (H.isSeparated _ (hY Y₂)).ext
    rintro Z φ ⟨i, ⟨g⟩⟩
    rw [hs' φ i g, ← hs' (φ ≫ f) i g, op_comp, F.map_comp]
    rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
⊢ Over.Hom.left f₂ ≫ Y₂.hom = W'.hom

Tactic:
by simpa using! (Over.forget _).congr_map h.symm =≫ Z.hom

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.functor.obj ((map U.inclusion').obj (⋯.functor.obj V)) = ⋯.functor.obj V

Tactic:
map_functor_eq V

Goal state after:
X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.functor.obj V = ⋯.functor.obj V
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ HasBinaryCoproducts α

Tactic:
have : ∀ x y : α, HasColimit (pair x y) := by
    let := hasFiniteColimits_of_hasFiniteColimits_of_size.{u} α
    infer_instance

Goal state after:
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
this : ∀ (x y : α), HasColimit (pair x y)
⊢ HasBinaryCoproducts α
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsCompatible F.obj U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.obj.obj (op (iSup U)))
gl_spec : IsGluing F.obj U sf gl
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
⊢ (fun s ↦ ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = sf i)
    ((ConcreteCategory.hom (F.obj.map (eqToHom V_eq_supr_U).op)) gl)

Tactic:
intro i
    rw [← ConcreteCategory.comp_apply, ← F.1.map_comp]
    exact gl_spec i

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case e'_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (F.obj.map ((eqToHom ⋯).op ≫ (eqToHom V_eq_supr_U).op))) s

Tactic:
eqToHom_op,

Goal state after:
case e'_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯ ≫ (eqToHom V_eq_supr_U).op))) s