mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₁)) x₁) = (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₂)) x₂)
⊢ (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)

Tactic:
have h₁ := congr_hom (Sigma.ι_map f i₁) x₁

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₁)) x₁) = (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₂)) x₂)
h₁ : (hom (Sigma.ι X₁ i₁ ≫ Limits.Sigma.map f)) x₁ = (hom (f i₁ ≫ Sigma.ι X₂ i₁)) x₁
⊢ (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d n i : ℕ
hi : i < n
y : X _⦋↑⟨i, hi⟩⦌
hy : y ∈ X.nonDegenerate ↑⟨i, hi⟩
f : unop (op ⦋d⦌) ⟶ unop (op ⦋↑⟨i, hi⟩⦌)
hx : (ConcreteCategory.hom (X.map (op f))) y ∈ X.nonDegenerate d
⊢ d < n

Tactic:
have := X.mono_of_nonDegenerate ⟨_, hx⟩ f y rfl

Goal state after:
X : SSet
d n i : ℕ
hi : i < n
y : X _⦋↑⟨i, hi⟩⦌
hy : y ∈ X.nonDegenerate ↑⟨i, hi⟩
f : unop (op ⦋d⦌) ⟶ unop (op ⦋↑⟨i, hi⟩⦌)
hx : (ConcreteCategory.hom (X.map (op f))) y ∈ X.nonDegenerate d
this : Mono f
⊢ d < n
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha✝ : a ∈ {i}ᶜ
b : Fin (n + 1 + 1 + 1)
hb✝ : b ∈ {i}ᶜ
hab : a < b
ha : ¬a = i
hb : ¬b = i
⊢ Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso a).inv ≫ f a ha✝ =
    Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso b).inv ≫ f b hb✝

Tactic:
rw [homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_pred_assoc _ _ hab,
        homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_castPred_assoc _ _ hab,
        hf.δ_pred_comp ..]

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.faceSingletonComplIso 0).inv ≫ ι₀) ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ =
    (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀

Tactic:
horn.faceSingletonComplIso_inv_ι

Goal state after:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ horn.faceι 1 0 ι₀._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.faceSingletonComplIso 2).inv ≫ ι₂) ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ =
    (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂

Tactic:
horn.faceSingletonComplIso_inv_ι

Goal state after:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ horn.faceι 1 2 ι₂._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.faceSingletonComplIso 3).inv ≫ ι₃) ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ =
    (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
horn.faceSingletonComplIso_inv_ι

Goal state after:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ horn.faceι 1 3 ι₃._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.faceSingletonComplIso 0).inv ≫ ι₀) ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ =
    (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀

Tactic:
horn.faceSingletonComplIso_inv_ι

Goal state after:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ horn.faceι 2 0 ι₀._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.faceSingletonComplIso 1).inv ≫ ι₁) ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ =
    (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁

Tactic:
horn.faceSingletonComplIso_inv_ι

Goal state after:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ horn.faceι 2 1 ι₁._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.faceSingletonComplIso 3).inv ≫ ι₃) ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ =
    (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
horn.faceSingletonComplIso_inv_ι

Goal state after:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ horn.faceι 2 3 ι₃._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g) ⊗ₘ 𝟙 (𝟙_ C) ≫ h) ≫ (α_ X Y Z).hom

Tactic:
← tensorHom_comp_tensorHom,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| (((λ_ (𝟙_ C)).inv ⊗ₘ 𝟙 (𝟙_ C)) ≫ ((f ⊗ₘ g) ⊗ₘ h)) ≫ (α_ X Y Z).hom
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
x : ((Center.ofBraided (Type v)).obj (unop α)).fst
f : X ⟶[Type v] Y
⊢ (ConcreteCategory.hom
          ((((Center.ofBraided (Type v)).obj (unop α)).snd.β (X ⟶[Type v] Y)).hom ≫
            (F.map X Y ⊗ₘ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app Y) ≫ eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y))).toFun
      (x, f) =
    (ConcreteCategory.hom
          (((↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X) ⊗ₘ G.map X Y) ≫
            eComp (Type v) (F.obj X) (G.obj X) (G.obj Y))).toFun
      (x, f)

Tactic:
exact (σ.hom x).naturality f

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ (ConcreteCategory.hom (X.map (mkOfSucc ⟨i, hi⟩).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) fac_aux₁._proof_1))) x

Tactic:
dsimp [lift]
  rw [spineToSimplex_arrow]
  rfl

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

Goal state before:
pp: V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : V.HomotopyCategory ⥤ D
φ : (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀ ⦃x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x✝¹ x✝ : V.HomotopyCategory
f : x✝¹ ⟶ x✝
this : (MorphismProperty.naturalityProperty fun x ↦ φ x.1.as) = ⊤
⊢ F.map f ≫ φ x✝.1.as = φ x✝¹.1.as ≫ G.map f

Tactic:
exact this.symm.le f (by simp)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ δ i.succ ≫ σ j.castSucc = σ j ≫ δ i

Tactic:
apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.δ_comp_σ_of_gt H

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case neg
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : hL.head.castSucc < t
h₂ : ¬a < ↑t
⊢ ↑(t.pred ⋯) = ↑t

Tactic:
simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val] at h₁; grind

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
b : α
mb : b ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
obtain ⟨s₀, ms₀⟩ := hS

Goal state after:
α : Type u_1
P : α → Prop
inst✝ : LE α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
b : α
mb : b ∈ ⋂₀ S
s₀ : Set α
ms₀ : s₀ ∈ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
b : α
mb : b ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
obtain ⟨s₀, ms₀⟩ := hS

Goal state after:
α : Type u_1
P : α → Prop
inst✝ : LE α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
b : α
mb : b ∈ ⋂₀ S
s₀ : Set α
ms₀ : s₀ ∈ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
x : Fin (n + 1)
⊢ map' OrderHom.id x.castSucc = x.castSucc

Tactic:
map'_eq_castSucc_iff

Goal state after:
case inl
n : ℕ
x : Fin (n + 1)
⊢ x.castSucc ≤ (OrderHom.id x).castSucc ∧ ∀ i < x, (OrderHom.id i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : map' g x.castSucc = y.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
map'_eq_castSucc_iff

Goal state after:
case inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (x.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j)))

Tactic:
SimplexCategory.Hom.ext_iff,

Goal state after:
case left
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : SimplexCategory.Hom.toOrderHom (inl' x y ≫ f) = SimplexCategory.Hom.toOrderHom (inl' x y ≫ g)
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (x.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j)))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ map' (g.comp f) x.castSucc = z.castSucc

Tactic:
map'_eq_castSucc_iff

Goal state after:
case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ x.castSucc ≤ ((g.comp f) z).castSucc ∧ ∀ i < z, ((g.comp f) i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case right
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (y.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j)))

Tactic:
SimplexCategory.Hom.ext_iff,

Goal state after:
case right
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : SimplexCategory.Hom.toOrderHom (inr' x y ≫ f) = SimplexCategory.Hom.toOrderHom (inr' x y ≫ g)
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (y.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j)))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ map' i.succAboveOrderEmb.toOrderHom x.succ.castSucc = x.castSucc

Tactic:
map'_eq_castSucc_iff

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ x.succ.castSucc ≤ (i.succAboveOrderEmb.toOrderHom x).castSucc ∧
    ∀ i_1 < x, (i.succAboveOrderEmb.toOrderHom i_1).castSucc < x.succ.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
Y : SSet
e : X ≅ Y
⊢ { dim := x.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex }.IsUniquelyCodimOneFace
    { dim := y.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex }

Tactic:
obtain ⟨d, x, rfl⟩ := x.mk_surjective
  obtain ⟨d', y, rfl⟩ := y.mk_surjective
  obtain rfl : d' = d + 1 := hxy.dim_eq
  rw [iff] at hxy ⊢
  simpa [← SSet.δ_naturality_apply, dsimp% (e.app (Opposite.op ⦋d⦌)).toEquiv.apply_eq_iff_eq]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = x.succ.castSucc

Tactic:
map'_eq_castSucc_iff

Goal state after:
case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x.castSucc ≤ ({ toFun := i.predAbove, monotone' := ⋯ } x.succ).castSucc ∧
    ∀ i_1 < x.succ, ({ toFun := i.predAbove, monotone' := ⋯ } i_1).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = x.castSucc.castSucc

Tactic:
map'_eq_castSucc_iff

Goal state after:
case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc ≤ ({ toFun := i.predAbove, monotone' := ⋯ } x.castSucc).castSucc ∧
    ∀ i_1 < x.castSucc, ({ toFun := i.predAbove, monotone' := ⋯ } i_1).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case fst
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
⊢ ((objEquiv ↑z₁) i).1 = ((objEquiv ↑z₂) i).1

Tactic:
exact DFunLike.congr_fun h i

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : h.IsProper
f : h.RankFunction α
⊢ h.IsRegular

Tactic:
by
  rw [← isRegular_pairing_iff]
  exact (h.rankFunctionEquiv α f).isRegular

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
⊢ (∐ X).Finite

Tactic:
have : HasColimitsOfShape (Discrete ι) (Type u) := by
    obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
    exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

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).Finite
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)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -((-1) ^ (n + 2 + (n + 1)) • H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 2)))

Tactic:
simp only [pow_add, even_two, Even.neg_pow, one_pow, mul_one,
      pow_one, mul_neg, neg_smul, neg_neg]

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)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    ((-1) ^ n * (-1) ^ n) • H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 2))
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 ι
j : ι
c : f.Cell j
⊢ ¬(↑c.s).subcomplex ≤ f.filtration j

Tactic:
simp only [ofSimplex_le_iff, filtration_def, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, not_or, not_exists]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
⊢ (↑c.s).simplex ∉ A.obj (op ⦋(↑c.s).dim⦌) ∧
    ∀ x < j, ∀ (x_2 : f.Cell x), (↑c.s).simplex ∉ (↑(P.p x_2.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
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
inst✝ : HasPushouts C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ (pushout.inl f g).app d ≫ (pushoutObjIso f g d).hom = pushout.inl (f.app d) (g.app d)

Tactic:
by
  simp [pushoutObjIso]

Goal state after:
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
inst✝ : HasPushouts C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ (pushout.inr f g).app d ≫ (pushoutObjIso f g d).hom = pushout.inr (f.app d) (g.app d)

Tactic:
by
  simp [pushoutObjIso]

Goal state after:
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
inst✝ : HasPushouts C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ pushout.inl (f.app d) (g.app d) ≫ (pushoutObjIso f g d).inv = (pushout.inl f g).app d

Tactic:
by
  simp [pushoutObjIso]

Goal state after:
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
inst✝ : HasPushouts C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ pushout.inr (f.app d) (g.app d) ≫ (pushoutObjIso f g d).inv = (pushout.inr f g).app d

Tactic:
by
  simp [pushoutObjIso]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : P.IsSeparating ∧ ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
X : C
A : Subobject X
hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ A = ⊤

Tactic:
rw [← Subobject.isIso_arrow_iff_eq_top]
    exact hS₂ A.arrow (fun G hG g ↦ ⟨_, Subobject.factorThru_arrow _ _ (hA G hG g)⟩)

Goal state after: