mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ f k ≤ { as := f j.as }.as

Tactic:
;

Goal state after:
J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ f k ≤ { as := f j.as }.as
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X Y : SSet
B : Y.Subcomplex
e : X ≅ Y
x : (B.preimage e.hom).N
⊢ ((SSet.N.orderIsoOfIso e) x.toN).simplex ∉ B.obj (Opposite.op ⦋((SSet.N.orderIsoOfIso e) x.toN).dim⦌)

Tactic:
;

Goal state after:
X Y : SSet
B : Y.Subcomplex
e : X ≅ Y
x : (B.preimage e.hom).N
⊢ ((SSet.N.orderIsoOfIso e) x.toN).simplex ∉ B.obj (Opposite.op ⦋((SSet.N.orderIsoOfIso e) x.toN).dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index hd))) (y.cast ⋯).simplex = (x.cast hd).simplex

Tactic:
;

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index hd))) (y.cast ⋯).simplex = (x.cast hd).simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex
⊢ Mono f

Tactic:
;

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex
⊢ Mono f
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex
⊢ Mono (SimplexCategory.δ (hxy.index hd))

Tactic:
;

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex
⊢ Mono (SimplexCategory.δ (hxy.index hd))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i))) =
    ↑(Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i))))

Tactic:
;

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i))) =
    ↑(Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i))))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i = Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))
⊢ ↑((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
        (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i))))) =
    ↑(Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i))

Tactic:
;

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i = Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))
⊢ ↑((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
        (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i))))) =
    ↑(Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x✝ : Fin ((unop (II ^⦋n + 1⦌)).len + 1)
⊢ (Hom.toOrderHom (II.δ i).unop) x✝ = (Hom.toOrderHom (σ i).op.unop) x✝

Tactic:
;

Goal state after:
n : ℕ
i : Fin (n + 2)
x✝ : Fin ((unop (II ^⦋n + 1⦌)).len + 1)
⊢ (Hom.toOrderHom (II.δ i).unop) x✝ = (Hom.toOrderHom (σ i).op.unop) x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
x : Fin ((unop (II ^⦋n⦌)).len + 1)
⊢ (Hom.toOrderHom (II.σ i).unop) x = (Hom.toOrderHom (δ i.succ.castSucc).op.unop) x

Tactic:
;

Goal state after:
n : ℕ
i : Fin (n + 1)
x : Fin ((unop (II ^⦋n⦌)).len + 1)
⊢ (Hom.toOrderHom (II.σ i).unop) x = (Hom.toOrderHom (δ i.succ.castSucc).op.unop) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ ↑((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
        (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i))))) =
    ↑(Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i))))

Tactic:
;

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ ↑((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
        (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i))))) =
    ↑(Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i))))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝¹ : X.Nonsingular
x y : X.N
h : x ≤ y
inst✝ : Mono (monoOfLE h)
⊢ (ConcreteCategory.hom (X.map (monoOfLE h).op)) y.simplex = x.simplex

Tactic:
;

Goal state after:
X : SSet
inst✝¹ : X.Nonsingular
x y : X.N
h : x ≤ y
inst✝ : Mono (monoOfLE h)
⊢ (ConcreteCategory.hom (X.map (monoOfLE h).op)) y.simplex = x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))

Tactic:
simpa using f.lt hxy

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ (↑(h.equivII x)).dim = (↑(h.equivII y)).dim →
    f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))

Tactic:
simpa using f.lt hxy

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{?u.4, u_1} J
inst✝³ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst✝² : Finite ι
X : ι → SSet
inst✝¹ : HasCoproduct X
inst✝ : ∀ (j : ι), (X j).Finite
this : HasColimitsOfShape (Discrete ι) (Type u)
x✝ : Discrete ι
j : ι
⊢ (X j).Finite

Tactic:
;

Goal state after:
J : Type u_1
inst✝⁴ : Category.{?u.4, u_1} J
inst✝³ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst✝² : Finite ι
X : ι → SSet
inst✝¹ : HasCoproduct X
inst✝ : ∀ (j : ι), (X j).Finite
this : HasColimitsOfShape (Discrete ι) (Type u)
x✝ : Discrete ι
j : ι
⊢ (X j).Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ ¬(↑c.s).subcomplex ≤ c.horn.image c.map

Tactic:
intro h
  simp only [Subfunctor.ofSection_le_iff, image_obj, Set.mem_image] at h
  obtain ⟨x, h₁, h₂⟩ := h
  obtain ⟨g, rfl⟩ := stdSimplex.objEquiv.symm.surjective x
  rw [← stdSimplex.map_objEquiv_op_apply, Equiv.apply_symm_apply] at h₂
  have := mono_of_nonDegenerate (x := ⟨_, c.s.val.nonDegenerate⟩) _ _ _ h₂
  obtain rfl := (P.isUniquelyCodimOneFace c.s).unique rfl _ h₂
  rw [← ofSimplex_le_iff, subcomplex_le_horn_iff, ← stdSimplex.face_singleton_compl] at h₁
  tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app none =
    𝟙 (c x✝).pt ≫ (c x✝).π.app none

pp: case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.left) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.left)

pp: case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.right) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.right)

Tactic:
;

Goal state after:
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app none =
    𝟙 (c x✝).pt ≫ (c x✝).π.app none

case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.left) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.left)

case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.right) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.right)
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ Sᶜ
⊢ α x = -β (γ₁ x)

Tactic:
dsimp [α, β, γ₁]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ Sᶜ
⊢ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1 = -((-1) ^ (↑x.2 + (↑x.1 + 1)) • H.h x.1.succ ≫ Y.δ x.2.castSucc)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ ({ app := fun X ↦ (c X).fst, naturality := ⋯ } ≫ f).app x✝ =
    ({ app := fun X ↦ (c X).snd, naturality := ⋯ } ≫ g).app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ ({ app := fun X ↦ (c X).fst, naturality := ⋯ } ≫ f).app x✝ =
    ({ app := fun X ↦ (c X).snd, naturality := ⋯ } ≫ g).app x✝
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
H : ∀ (k : K), ∃ j y_1, (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j)) y_1 = ↑y k
j : K → J := fun k ↦ ⋯.choose
z : (k : K) → (F.obj k).obj (X.obj (j k)) := fun k ↦ ⋯.choose
hz : ∀ (k : K), (ConcreteCategory.hom ((F.obj k).map (cX.ι.app (j k)))) (z k) = ↑y k
k : K
⊢ (ConcreteCategory.hom ((F.obj k).map (cX.ι.app (j k)))) (z k) =
    (ConcreteCategory.hom ((F.obj k).map (cX.ι.app (j k)))) (z k)

Tactic:
;

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
H : ∀ (k : K), ∃ j y_1, (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j)) y_1 = ↑y k
j : K → J := fun k ↦ ⋯.choose
z : (k : K) → (F.obj k).obj (X.obj (j k)) := fun k ↦ ⋯.choose
hz : ∀ (k : K), (ConcreteCategory.hom ((F.obj k).map (cX.ι.app (j k)))) (z k) = ↑y k
k : K
⊢ (ConcreteCategory.hom ((F.obj k).map (cX.ι.app (j k)))) (z k) =
    (ConcreteCategory.hom ((F.obj k).map (cX.ι.app (j k)))) (z k)
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasEqualizers C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
⊢ p = q

Tactic:
have := hf (equalizer.lift f h) (equalizer.ι p q) (by simp)
    rw [← cancel_epi (equalizer.ι p q), equalizer.condition]

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
⊢ ExtremalEpi f ↔ StrongEpi f

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, fun A B i _ ↦ ⟨fun {t b} sq ↦ ⟨⟨?_⟩⟩⟩⟩,
    fun _ ↦ inferInstance⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
⊢ sq.LiftStruct
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
hs : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∈ (f.sigmaStdSimplex j).nonDegenerate d
hs' : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∉ (range (f.m j)).obj (op ⦋d⦌)
h : s ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((x.ιSigmaHorn ≫ f.m j).app (op ⦋d⦌))) ⟨s, h⟩ =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s

Tactic:
;

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
hs : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∈ (f.sigmaStdSimplex j).nonDegenerate d
hs' : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∉ (range (f.m j)).obj (op ⦋d⦌)
h : s ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((x.ιSigmaHorn ≫ f.m j).app (op ⦋d⦌))) ⟨s, h⟩ =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x✝ : ↑h.smallCategoryOfSet.obj
⊢ h.homEquiv (h.smallCategoryOfSet.id x✝) = 𝟙 (h.objEquiv x✝)

Tactic:
;

Goal state after:
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x✝ : ↑h.smallCategoryOfSet.obj
⊢ h.homEquiv (h.smallCategoryOfSet.id x✝) = 𝟙 (h.objEquiv x✝)
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X✝ Y✝ Z✝ : ↑h.smallCategoryOfSet.obj
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ h.homEquiv (h.smallCategoryOfSet.comp x✝¹ x✝) = h.homEquiv x✝¹ ≫ h.homEquiv x✝

Tactic:
;

Goal state after:
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X✝ Y✝ Z✝ : ↑h.smallCategoryOfSet.obj
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ h.homEquiv (h.smallCategoryOfSet.comp x✝¹ x✝) = h.homEquiv x✝¹ ≫ h.homEquiv x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsLimit (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.mapCone (PullbackCone.mk (f.t j) (f.m j) ⋯))

Tactic:
refine (isLimitMapConePullbackConeEquiv _ _).symm
      (IsPullback.isLimit ?_)

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsPullback (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.t j))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (homOfLE ⋯))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
k : Kᵒᵖ
⊢ (coyoneda.obj (op (Y.obj (unop k)))).IsCardinalAccessible κ

Tactic:
;

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
k : Kᵒᵖ
⊢ (coyoneda.obj (op (Y.obj (unop k)))).IsCardinalAccessible κ