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

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := ⋯
n : ↑S.X₁
cn : ι →₀ R
hnm : (cn.sum fun a b ↦ (Hom.hom S.f) (b • v a)) = m - m'
hn : (cn.sum fun i a ↦ a • v i) = n
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ m' ∈ span R (range u)

Tactic:
rw [Finsupp.mem_span_range_iff_exists_finsupp]

Goal state after:
case a
ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
n : ↑S.X₁
cn : ι →₀ R
hnm : (cn.sum fun a b ↦ (Hom.hom S.f) (b • v a)) = m - m'
hn : (cn.sum fun i a ↦ a • v i) = n
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ ∃ c, (c.sum fun i a ↦ a • u i) = m'
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Function.Surjective ⇑(ConcreteCategory.hom S.g)
⊢ ⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w = w

Tactic:
rw [← Function.comp_assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE),
      Function.id_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ alternatingMapLinearEquiv (ιMulti R n) = LinearMap.id

Tactic:
ext
  simp only [alternatingMapLinearEquiv_comp_ιMulti, ιMulti_apply_coe,
    LinearMap.compAlternatingMap_apply, LinearMap.id_coe, id_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s ∈ powersetCard I n
⊢ ↑((⇑(map n f) ∘ ιMulti_family R n v) ⟨s, hs⟩) = ↑(ιMulti_family R n (⇑f ∘ v) ⟨s, hs⟩)

Tactic:
simp only [ιMulti_family, Function.comp_apply, map_apply_ιMulti]

Goal state after:
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s ∈ powersetCard I n
⊢ ↑((ιMulti R n) (⇑f ∘ v ∘ ⇑(ofFinEmbEquiv.symm ⟨s, hs⟩))) = ↑((ιMulti R n) ((⇑f ∘ v) ∘ ⇑(ofFinEmbEquiv.symm ⟨s, hs⟩)))
Module: Mathlib.CategoryTheory.Discrete.StructuredArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
F : C ⥤ Discrete T
t : T
inst✝ : Subsingleton T
X : C
⊢ { as := t } = F.obj X

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.StructuredArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
F : C ⥤ Discrete T
t : T
inst✝ : Subsingleton T
X : C
⊢ F.obj X = { as := t }

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
this : snd A I = uncurry (t.to (A ⟹ I))
⊢ uncurry (t.to (A ⟹ I)) ≫ t.to (A ⊗ I) = 𝟙 (A ⊗ I)

Tactic:
← uncurry_natural_right,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
this : snd A I = uncurry (t.to (A ⟹ I))
⊢ uncurry (t.to (A ⟹ I) ≫ (ihom A).map (t.to (A ⊗ I))) = 𝟙 (A ⊗ I)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
x✝ : J
⊢ isTerminalTensorUnit.from (Y.obj x✝) =
    (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone (𝟙_ (J ⥤ C))) fun x ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit (((evaluation J C).obj x).mapCone (asEmptyCone (𝟙_ (J ⥤ C))))
              (Iso.refl (𝟙_ C)))
          Y).app
      x✝

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
x✝ : J
⊢ isTerminalTensorUnit.from (X.obj x✝) =
    (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone (𝟙_ (J ⥤ C))) fun x ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit (((evaluation J C).obj x).mapCone (asEmptyCone (𝟙_ (J ⥤ C))))
              (Iso.refl (𝟙_ C)))
          X).app
      x✝

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ (colimitCompCoyonedaIso F d).toEquiv ((ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s) =
    (colimitCompCoyonedaIso F d).toEquiv ((ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s')

Tactic:
subsingleton

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
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj (j', k').1).π.app k' = ((Cone.postcompose (F.map fj)).obj (D.obj (j, k).1)).π.app k'
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k' ≫ (F.map fj).app k'

Tactic:
dsimp at w

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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj j').π.app k' = (D.obj j).π.app k' ≫ (F.map fj).app k'
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k' ≫ (F.map fj).app k'
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
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj (j, k).1).ι.app k ≫ (D.map fj).hom = ((Cocone.precompose (F.map fj)).obj (D.obj (j', k').1)).ι.app k
⊢ (F.map fj).app k ≫ (D.obj j').ι.app k ≫ 𝟙 (D.obj j').pt ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
dsimp at w

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
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
⊢ (F.map fj).app k ≫ (D.obj j').ι.app k ≫ 𝟙 (D.obj j').pt ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ Sieve.generate R ≤ S

Tactic:
rwa [Sieve.giGenerate.gc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : K ≤ J.toPretopology
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ Sieve.generate R ≤ S

Tactic:
rwa [Sieve.giGenerate.gc]

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
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
Z : C
f : Z ⟶ Y
⊢ ∃ Z_1 g, (Sieve.pullback h S).arrows (g ≫ f)

Tactic:
rcases H (f ≫ h) with ⟨W, g, H'⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
Z : C
f : Z ⟶ Y
W : C
g : W ⟶ Z
H' : S.arrows (g ≫ f ≫ h)
⊢ ∃ Z_1 g, (Sieve.pullback h S).arrows (g ≫ f)
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
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
Z : C
f : Z ⟶ Y
W : C
g : W ⟶ Z
H' : S.arrows (g ≫ f ≫ h)
⊢ (Sieve.pullback h S).arrows (g ≫ f)

Tactic:
by simpa

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
𝒮 : Set (Sieve X)
x✝² x✝¹ : C
f : x✝² ⟶ X
hf : ∃ S ∈ 𝒮, S.arrows f
x✝ : x✝¹ ⟶ x✝²
⊢ ∃ S ∈ 𝒮, S.arrows (x✝ ≫ f)

Tactic:
obtain ⟨S, hS, hf⟩ := hf
    exact ⟨S, hS, S.downward_closed hf _⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Presieve X
Y Z W : C
g : Y ⟶ W
f : W ⟶ X
hf : R f
h : Z ⟶ Y
⊢ ∃ Y_1 h_1 g_1, R g_1 ∧ h_1 ≫ g_1 = h ≫ g ≫ f

Tactic:
exact ⟨_, h ≫ g, _, hf, by simp⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward (g ≫ f) R).arrows h
f₁ : W ⟶ Z
hq : f₁ ≫ g ≫ f = h
hf₁ : R.arrows f₁
⊢ (f₁ ≫ g) ≫ f = h

Tactic:
by simpa

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
S : Sieve X
Z : C
g : Z ⟶ X
hg : S.arrows g
⊢ (g ≫ section_ f) ≫ f = g ∧ (pullback f S).arrows (g ≫ section_ f)

Tactic:
by simpa

Goal state after:
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 : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)

Tactic:
rw [← ht _ h₁, ← ht _ h₂, ← comp_apply, ← Functor.map_comp, ← op_comp, comm]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map (g₂ ≫ f₂).op)) t =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)
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
⊢ forkMap P R ≫ firstMap P R = forkMap P R ≫ secondMap P R

Tactic:
by
  dsimp
  ext fg
  simp only [firstMap, secondMap, forkMap]
  simp only [limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app]
  have := Presieve.HasPairwisePullbacks.has_pullbacks fg.1.2.2 fg.2.2.2
  rw [← P.map_comp, ← op_comp, pullback.condition]
  simp

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

Goal state before:
pp: 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 : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ shrinkYonedaObjObjEquiv.symm f ∈ (shrinkFunctor.{w, v₁, u₁} S).obj (op Y)

Tactic:
by simpa

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
⊢ (∃ g, F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f

Tactic:
refine ⟨fun ⟨g, hcomp, hg⟩ ↦ ?_, fun hf ↦ ⟨f, rfl, hf⟩⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
x✝ : ∃ g, F.map g = F.map f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = F.map f
hg : R.arrows g
⊢ R.arrows f
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: 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)
X : C
P : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans (𝟙 P) X).app x✝ = (𝟙 (J.diagram P X)).app x✝

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)

Goal state after:
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)
X : C
P : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans (𝟙 P) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i =
    (𝟙 (J.diagram P X)).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: 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✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans 0 X).app x✝ = NatTrans.app 0 x✝

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)

Goal state after:
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✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans 0 X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i =
    NatTrans.app 0 x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: 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 Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans (η ≫ γ) X).app x✝ = (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X).app x✝

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)

Goal state after:
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 Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans (η ≫ γ) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index R) i =
    (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index R) i
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁵ : Category.{v₁, u₁} J
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
⊢ (colimMap (limitIsoSwapCompLim G).hom ≫
        colimitLimitToLimitColimit (uncurry.obj G) ≫ limMap (whiskerRight (currying.unitIso.inv.app G) colim)) ≫
      limit.π (G ⋙ colim) j =
    colimMap (limit.π G j)

Tactic:
ext1 k

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁵ : Category.{v₁, u₁} J
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
k : K
⊢ colimit.ι (limit G) k ≫
      (colimMap (limitIsoSwapCompLim G).hom ≫
          colimitLimitToLimitColimit (uncurry.obj G) ≫ limMap (whiskerRight (currying.unitIso.inv.app G) colim)) ≫
        limit.π (G ⋙ colim) j =
    colimit.ι (limit G) k ≫ colimMap (limit.π G j)
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
suffices Epi f ↔ Epi ((forget TopCat).map f) by
    rw [this, CategoryTheory.ofHom_epi_iff_surjective]
  constructor
  · intro
    apply Functor.map_epi -- was `infer_instance`
  · apply Functor.epi_of_epi_map

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ pullbackFst f g ≫ f = pullbackSnd f g ≫ g

Tactic:
dsimp [pullbackFst, pullbackSnd, Function.comp_def]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ ofHom { toFun := fun x ↦ (↑x).1, continuous_toFun := ⋯ } ≫ f =
    ofHom { toFun := fun x ↦ (↑x).2, continuous_toFun := ⋯ } ≫ g
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
D✝ : Type u''
inst✝³ : Category.{v'', u''} D✝
X✝ Y✝ : C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : HasBinaryCoproducts C
F : C ⥤ D
inst✝ : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f coprod.inr) F

Tactic:
apply preservesLimit_of_iso_diagram (K₁ := cospan (f ≫ (coprod.braiding X Y).hom) coprod.inl)
  apply cospanExt (Iso.refl _) (Iso.refl _) (coprod.braiding X Y).symm <;> simp

Goal state after:
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 : IsVanKampenColimit (PushoutCocone.mk h i✝ ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ 𝟙 ((span f' g').obj i) ≫ Option.rec αW (fun val ↦ WalkingPair.rec αX αY val) i =
    Option.rec αW (fun val ↦ WalkingPair.rec αX αY val) i ≫ 𝟙 ((span f g).obj i)

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

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

Goal state before:
pp: case h₁
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
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit 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
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, 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' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
i j : J
g : i ⟶ j
⊢ Gr.map (F'.map g ≫ α.app j ≫ adj.counit.app (F.obj j)) ≫ c.ι.app j =
    Gr.map (α.app i ≫ adj.counit.app (F.obj i)) ≫ c.ι.app i

Tactic:
· rw [α.naturality_assoc]
        dsimp
        rw [adj.counit_naturality, ← Category.assoc, Gr.map_comp_assoc]
        congr 1
        exact c.w _

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

Goal state before:
pp: case mpr.uniq.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ H.cocone.inr ≫ m =
    H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
rw [H.isColimit.fac _ WalkingSpan.right]
        apply BinaryCofan.IsColimit.hom_ext hc
        · erw [hc.fac]
          erw [← H.w_assoc]
          rw [e₂]
          rfl
        · refine ((Category.assoc _ _ _).symm.trans e₁).trans ?_; symm; exact hc.fac _ _

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u''
inst✝² : Category.{v'', u''} D
X✝ Y : C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
X : ι → C
c : Cofan X
hc : IsColimit c
i j : ι
e : i ≠ j
s : PullbackCone (c.inj i) (c.inj j)
hs : IsLimit s
⊢ { as := i } ≠ { as := j }

Tactic:
by simpa

Goal state after: