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

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ j.succ = 0

Tactic:
← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
    (by simp)),

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ ((kernelSubobject (X.δ j.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
        (kernelSubobject (X.δ j.succ)).arrow) ≫
      X.δ j.succ =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ : ¬Mono θ
⊢ X.map θ.op ≫ PInfty.f n = 0

Tactic:
rw [SimplexCategory.mono_iff_injective] at hθ
  cases n
  · exfalso
    apply hθ
    intro x y h
    fin_cases x
    fin_cases y
    rfl
  · obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
    rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B = A
⊢ s.N (unop B.fst).len ⟶ s.N (unop A.fst).len

Tactic:
exact eqToHom (by subst h; rfl)

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ PInfty.f n ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A ↦ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    PInfty.f n

Tactic:
conv_rhs =>
    rw [← PInfty_f_idem]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ PInfty.f n ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A ↦ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    PInfty.f n ≫ PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬A.EqId
⊢ (s.cofan (op ⦋j⦌)).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Tactic:
A.eqId_iff_mono

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ (s.cofan (op ⦋j⦌)).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x

Tactic:
comp_as_mul,

Goal state after:
G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ f⁻¹ * f = 𝟙 x
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
by
  ext ⟨t, _⟩
  rw [trans_apply, symm_apply, trans_apply]
  simp only [coe_symm_eq, symm_apply]
  split_ifs with h₁ h₂ h₂
  · have ht : (t : ℝ) = 1 / 2 := by linarith
    norm_num [ht]
  · congr 2
    apply Subtype.ext
    simp only [coe_symm_eq]
    linarith
  · congr 2
    apply Subtype.ext
    simp only [coe_symm_eq]
    linarith
  · exfalso
    linarith

Goal state after:
Module: Mathlib.Topology.Homotopy.Equiv

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (h₂.toFun.comp h₂.invFun)

Tactic:
exact .comp (.refl _) <| .comp h₁.right_inv (.refl _)

Goal state after:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
⊢ projLeft (prod q₁ q₂) = q₁

Tactic:
induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
  rw [projLeft, prod_lift, ← Path.Homotopic.Quotient.mk_map]
  congr

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
set G : C(I × I, Y) := F.toContinuousMap.comp (.prodMap (.id _) p)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i✝ : Fin (n + 1)
i : ↑{i✝}ᶜ
⊢ (stdSimplex.face {↑i}ᶜ).toSSet.HasDimensionLT n

Tactic:
exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (stdSimplex.face {i}ᶜ).toSSet.HasDimensionLT n

Tactic:
exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
x₂ : X
h₂ : x₂ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₂, h₂⟩
⊢ x₁ = x₂

Tactic:
by simpa using h

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

Goal state before:
pp: m : SimplexCategoryᵒᵖ
x✝ : Δ[0].obj m
x : Fin 1
⊢ ∃ a, (stdSimplex.asOrderHom x✝) a = x

Tactic:
exact ⟨0, by subsingleton⟩

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

Goal state before:
pp: J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
x : X
hx : x ∈ F.obj i
y : X
hy : y ∈ F.obj j
h :
  (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) ⟨x, hx⟩ =
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) ⟨y, hy⟩
⊢ x = y

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₁ : X₁
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl z₁)

Tactic:
rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h, h', rfl⟩ := hyz
        · apply Rel'.inr_inl
        · obtain rfl := (mono_iff_injective f).1 inferInstance h'
          rw [h]
          apply Rel'.inr_inl

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

Goal state before:
pp: case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)

Tactic:
· simp only [sup_le_iff, iSup_le_iff]
    constructor
    · exact X.skeleton.monotone (by simp)
    · intro x
      apply X.ofSimplex_le_skeleton _ (by simp)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
a : F.HomObj G A
X Y : C
f : X ⟶ Y
⊢ ((F ⊗ A).map f ≫
      ↾fun x ↦
        match x with
        | (x, y) => (ConcreteCategory.hom (a.app Y y)) x) =
    (↾fun x ↦
        match x with
        | (x, y) => (ConcreteCategory.hom (a.app X y)) x) ≫
      G.map f

Tactic:
ext ⟨x, y⟩
    simpa using! ConcreteCategory.congr_hom (a.naturality f y) x

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ (X.fst ⊗ Y.fst) ◁ f ≫
      (α_ X.fst Y.fst U').hom ≫
        X.fst ◁ (Y.snd.β U').hom ≫ (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom =
    ((α_ X.fst Y.fst U).hom ≫
        X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ≫
      f ▷ (X.fst ⊗ Y.fst)

Tactic:
calc
          _ = 𝟙 _ ⊗≫
            (X.1 ◁ (Y.1 ◁ f ≫ (HalfBraiding.β Y.2 U').hom)) ⊗≫
              (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ := by monoidal
          _ = 𝟙 _ ⊗≫
            X.1 ◁ (HalfBraiding.β Y.2 U).hom ⊗≫
              (X.1 ◁ f ≫ (HalfBraiding.β X.2 U').hom) ▷ Y.1 ⊗≫ 𝟙 _ := by
            rw [HalfBraiding.naturality]; monoidal
          _ = _ := by rw [HalfBraiding.naturality]; monoidal

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
inst✝ : X.IsCoskeletal n
⊢ IsIso ((coskAdj n).unit.app X)

Tactic:
by
  rw [← isCoskeletal_iff_isIso]
  infer_instance

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

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ ((Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V)).multiplicativeClosure
    ((quotientFunctor V).map f)

Tactic:
refine strictMap_multiplicativeClosure_le _ _ _ ?_

Goal state after:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).multiplicativeClosure.strictMap (quotientFunctor V)
    ((quotientFunctor V).map f)
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
fac fac' : W₁.MapFactorizationData W₂ f
⊢ fac.Z = fac'.Z

Tactic:
by
  have := r.subsingleton_mapFactorizationData f
  obtain rfl : fac = fac' := Subsingleton.elim _ _
  rfl

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

Goal state before:
pp: case comp_σ.comp_of.succ
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i

Goal state after:
case comp_σ.comp_of.succ.inl
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : δ i ≫ σ j = 𝟙 (mk (n + 1))
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

case comp_σ.comp_of.succ.inr
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ simplicialEvalσ L L[k] = simplicialEvalσ L (L[k] + 1)

Tactic:
induction L generalizing m k

Goal state after:
case nil
m : ℕ
hL : IsAdmissible m []
k : ℕ
hk : k < [].length
⊢ simplicialEvalσ [] [][k] = simplicialEvalσ [] ([][k] + 1)

case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ :
  ∀ {m : ℕ},
    IsAdmissible m tail✝ →
      ∀ {k : ℕ} {hk : k < tail✝.length}, simplicialEvalσ tail✝ tail✝[k] = simplicialEvalσ tail✝ (tail✝[k] + 1)
m : ℕ
hL : IsAdmissible m (head✝ :: tail✝)
k : ℕ
hk : k < (head✝ :: tail✝).length
⊢ simplicialEvalσ (head✝ :: tail✝) (head✝ :: tail✝)[k] = simplicialEvalσ (head✝ :: tail✝) ((head✝ :: tail✝)[k] + 1)
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
mb : b ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
cases mb with

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

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
mb : b ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
cases mb with

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⦌.len ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
⊢ (ConcreteCategory.hom
          ((↾fun x ↦ lift sx s x) ≫
            ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app (StructuredArrow.mk (op f)))).toFun
      x =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))).toFun x

Tactic:
dsimp at hi ⊢

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
⊢ (ConcreteCategory.hom (X.map (op f)))
      (sx.spineToSimplex
        { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x
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:
| right j =>

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

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

Tactic:
obtain rfl : A.preimage e.inv = B := by aesop

Goal state after:
X : SSet
A : X.Subcomplex
Y : SSet
e : X ≅ Y
hA : (A.preimage e.inv).preimage e.hom = A
y : (A.preimage e.inv).N
⊢ ((SSet.N.orderIsoOfIso e).symm y.toN).simplex ∉ A.obj (Opposite.op ⦋((SSet.N.orderIsoOfIso e).symm y.toN).dim⦌)
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 (tensorObjOf x y).len.succ i)
⊢ Fin.cast ⋯ ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)

Tactic:
have e₂ := inr'_eval y z i

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 (tensorObjOf x y).len.succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
⊢ Fin.cast ⋯ ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ P.pairing.IsRegular ↔ Nonempty (P.WeakRankFunction ℕ)

Tactic:
Pairing.isRegular_iff_nonempty_weakRankFunction

Goal state after:
X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ Nonempty (P.pairing.WeakRankFunction ℕ) ↔ Nonempty (P.WeakRankFunction ℕ)
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✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
s : X.N
a✝ : s.subcomplex ≤ ⊤
⊢ s.subcomplex ≤ ⨆ i, f.filtration i

Tactic:
cases s using SSet.Subcomplex.N.cases A with

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable

Goal state before:
pp: C : Type u
hC : Category.{v, u} C
inst✝ : IsAccessibleCategory.{w, v, u} C
X : C
κ : Cardinal.{w}
w✝² : Fact κ.IsRegular
h✝ : IsCardinalAccessibleCategory C κ
w✝¹ : ObjectProperty C
w✝ : ObjectProperty.EssentiallySmall.{w, v, u} w✝¹
h : w✝¹.IsCardinalFilteredGenerator κ
⊢ IsPresentable.{w, v, u} X

Tactic:
apply h.presentable

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory := { obj := coequalizer φ₁ φ₂, property := ⋯ }
⊢ φ₁ ≫ (E.coconeAt X).ι.app j = φ₂ ≫ (E.coconeAt X).ι.app j

Tactic:
by simpa using h

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

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : X✝ ⟶ Y✝
x✝ : isomorphisms SSet e
f : Y✝ ⟶ Z✝
hf : strongAnodyneExtensions f
⊢ strongAnodyneExtensions (e ≫ f)

Tactic:
by
    obtain ⟨_, P, hP⟩ := hf
    refine ⟨inferInstance, P.ofIso (Iso.refl _) ?_, inferInstance⟩
    simp [Subcomplex.range_comp, Subcomplex.range_eq_top e,
      Subcomplex.image_top]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerAnodyneExtensions =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
rw [innerAnodyneExtensions_eq_llp_rlp,
    SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
this✝ :
  Mono
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
this :
  IsIso
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X

Tactic:
exact ⟨IsColimit.ofIsoColimit (colimit.isColimit _) (Cocone.ext
      (asIso (colimit.desc _ (E.coconeAt X))))⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝¹ : P.IsRegular
inst✝ : P.IsInner
j : ℕ
hj : ¬IsMax j
⊢ SSet.innerAnodyneExtensions (P.rankFunction.relativeCellComplex.F.map (CategoryTheory.homOfLE ⋯))

Tactic:
by
      refine (?_ : (_ : MorphismProperty _) ≤ _ ) _
        (P.rankFunction.relativeCellComplex.attachCells j hj).pushouts_coproducts
      simp only [pushouts_le_iff, coproducts_le_iff]
      rintro _ _ _ ⟨c⟩
      have h0 := Fin.pos_iff_ne_zero.mpr (IsInner.ne_zero c.s rfl)
      have hn := Fin.lt_last_iff_ne_last.mpr (IsInner.ne_last c.s rfl)
      have : NeZero c.dim := ⟨by grind⟩
      exact .horn_ι h0 hn

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

Goal state before:
pp: case inl.inr.refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ ((objEquiv (x.cast hd).simplex) i.castSucc).2 ≤ (k.castSucc, (x.cast hd).simplex.2 (min x hd)).2

Tactic:
exact stdSimplex.monotone_apply _
          (by dsimp; rw [← hi]; exact Fin.castSucc_le_succ i)

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

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
⊢ IsInitial X

Tactic:
exact IsInitial.ofUniqueHom (fun _ ↦
    { app _ := ↾fun x ↦ isEmptyElim x
      naturality _ _ _  := by ext x; exact isEmptyElim x })
    (fun _ _ ↦ by ext _ x; exact isEmptyElim x)

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

Goal state before:
pp: X Y Z : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
x y : X _⦋0⦌
e : Edge x y
⊢ f x = f y

Tactic:
exact hf e

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

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
⊢ (pairing k.castSucc.succ n).IsInner

Tactic:
simp only [← Fin.castSucc_succ, pairing_castSucc]

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
⊢ (pairingCore k.succ n).pairing.IsInner