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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
X✝ Y✝ Z✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X✝).len + 1)))) C
⊢ EnrichedFunctor.comp SSet
      (SimplicialThickening.functor
        ((SimplexCategory.Hom.toOrderHom f.unop).uliftMap.comp (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))
      x✝ =
    (ConcreteCategory.hom
          (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
            ↾EnrichedFunctor.comp SSet
                (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))).toFun
      x✝

Tactic:
rw [SimplicialThickening.functor_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
X✝ Y✝ Z✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X✝).len + 1)))) C
⊢ EnrichedFunctor.comp SSet
      (EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)
        (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap))
      x✝ =
    (ConcreteCategory.hom
          (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
            ↾EnrichedFunctor.comp SSet
                (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))).toFun
      x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 2)
hz : z ∈ finset f y
⊢ z ∈ finset f x

Tactic:
obtain ⟨z, rfl⟩ | rfl := z.eq_castSucc_or_eq_last

Goal state after:
case inl
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 1)
hz : z.castSucc ∈ finset f y
⊢ z.castSucc ∈ finset f x

case inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
hz : Fin.last (n + 1) ∈ finset f y
⊢ Fin.last (n + 1) ∈ finset f x
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
i : Fin (n + 1)
⊢ ↑(x.1 i) + ↑(x.2 i) < m + 1

Tactic:
lia

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

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this : (objEquiv x) i ≤ (objEquiv x) j
h₁ : x.1 i ≤ x.1 j
h₂ : x.2 i ≤ x.2 j
⊢ ↑(x.1 i) + ↑(x.2 i) ≤ ↑(x.1 j) + ↑(x.2 j)

Tactic:
lia

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

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2

Tactic:
lia

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

Goal state before:
pp: p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hx : n ≤ p + q
⊢ False

Tactic:
lia

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) x ∈ X.nonDegenerate n

Tactic:
have := Nonsingular.mono' x hx

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
this : Mono (yonedaEquiv.symm x)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) x ∈ X.nonDegenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : orderHomOfSimplex z hn = OrderHom.id
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
⊢ a = b

Tactic:
simp only [DFunLike.ext_iff, orderHomOfSimplex_coe, OrderHom.id_coe, id_eq] at h

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ a = b
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i j : Fin (n + 2)
hij : (ConcreteCategory.hom (SimplicialObject.δ X i)) x = (ConcreteCategory.hom (SimplicialObject.δ X j)) x
⊢ i = j

Tactic:
apply SimplexCategory.δ_injective

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i j : Fin (n + 2)
hij : (ConcreteCategory.hom (SimplicialObject.δ X i)) x = (ConcreteCategory.hom (SimplicialObject.δ X j)) x
⊢ SimplexCategory.δ i = SimplexCategory.δ j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : SimplexCategory
f g : m ⟶ ⦋n⦌
h : (ConcreteCategory.hom (X.map f.op)) x = (ConcreteCategory.hom (X.map g.op)) x
⊢ f = g

Tactic:
have := Nonsingular.mono' x hx

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : SimplexCategory
f g : m ⟶ ⦋n⦌
h : (ConcreteCategory.hom (X.map f.op)) x = (ConcreteCategory.hom (X.map g.op)) x
this : Mono (yonedaEquiv.symm x)
⊢ f = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ n₀ ≤ n₀ + n + 1

Tactic:
lia

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ n₀ ≤ n₀ + n

Tactic:
lia

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p t)).cast ⋯).simplex }
⊢ ↑(P.p s) = ↑t

Tactic:
rw [(P.isUniquelyCodimOneFace t).δ_index rfl] at h

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ ↑(P.p s) = ↑t
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ h.index s = ⋯.index ⋯

Tactic:
simp [← (h.isUniquelyCodimOneFace s).δ_eq_iff]

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

Goal state before:
pp: case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
t : T
f : ⦋(↑↑t).dim⦌ ⟶ ⦋(↑(P.p y)).dim⦌
w✝ : CategoryTheory.Mono f
hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).simplex
⊢ (↑↑t).dim < (↑(P.p y)).dim

pp: case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
t : T
f : ⦋(↑↑t).dim⦌ ⟶ ⦋(↑(P.p y)).dim⦌
w✝ : CategoryTheory.Mono f
hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).simplex
⊢ ψ ⟨⟨(↑↑t).dim, ?refine_1⟩, f⟩ = (↑↑t).toS

Tactic:
· simpa using SSet.N.dim_lt_of_lt t.2.2

Goal state after:
case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
t : T
f : ⦋(↑↑t).dim⦌ ⟶ ⦋(↑(P.p y)).dim⦌
w✝ : CategoryTheory.Mono f
hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).simplex
⊢ ψ ⟨⟨(↑↑t).dim, ⋯⟩, f⟩ = (↑↑t).toS
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
⊢ (⊥_ SSet).Finite

Tactic:
by
  apply finite_of_isColimit (initialIsInitial (C := SSet.{u}))
  rintro ⟨⟨⟩⟩

Goal state after:
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
⊢ (stdSimplex.face {c.index}ᶜ).image c.map = (↑c.s).subcomplex

Tactic:
stdSimplex.face_singleton_compl,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ (ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))).image c.map = (↑c.s).subcomplex
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
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
k k' : K
φ : k ⟶ k'
⊢ (ConcreteCategory.hom ((F.obj k').map (cX.ι.app j₀))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
    (ConcreteCategory.hom ((F.obj k').map (cX.ι.app j₀))) (z k')

Tactic:
simpa only [← NatTrans.naturality_apply, ← hz] using! y.2 φ

Goal state after:
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 : ι
x' : f.Cell j
hy' : stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋x'.dim + 1⦌))) ∈ x'.horn.obj (op ⦋x'.dim + 1⦌)
⊢ False

Tactic:
exact objEquiv_symm_notMem_horn_of_isIso _ _ hy'

Goal state after:
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
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd✝ : d ≤ x.dim
hd : d < x.dim
⊢ d + 1 < x.dim + 1

Tactic:
lia

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
J : Type w
w✝ : Category.{w', w} J
p : P.ColimitOfShape J Y
φ : (j : J) → p.diag.obj j ⟶ X
hφ : ∀ (j : J), φ j ≫ i = p.ι.app j
c : Cocone p.diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
j : J
⊢ p.ι.app j ≫ p.isColimit.desc c ≫ i = p.ι.app j ≫ 𝟙 Y

Tactic:
rw [p.isColimit.fac_assoc, hφ, Category.comp_id]

Goal state after:
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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂

Tactic:
have hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁ := by simp [y₁]

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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Injective h.functor.mapArrow.obj

pp: case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Surjective h.functor.mapArrow.obj

Tactic:
· rintro ⟨x, y, f⟩ ⟨x', y', g⟩ hfg
      obtain rfl : x = x' := by simpa using! congr_arg Arrow.leftFunc.obj hfg
      obtain rfl : y = y' := by simpa using! congr_arg Arrow.rightFunc.obj hfg
      obtain rfl : f = g := by simpa [Arrow.mk_eq_mk_iff] using! hfg
      rfl

Goal state after:
case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Surjective h.functor.mapArrow.obj
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate (x.dim + 1)
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

Tactic:
obtain rfl := SimplexCategory.eq_id_of_mono g
    exact ⟨x, Or.inl rfl⟩

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

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ (f.mapN (Cell.type₁ f c)).simplex ∈ X.nonDegenerate (f.mapN (Cell.type₁ f c)).dim

Tactic:
f.mapN_type₁

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }.simplex ∈
    X.nonDegenerate { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }.dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ anodyneExtensions Λ[n, i].ι

Tactic:
rw [anodyneExtensions_eq_llp_rlp]

Goal state after:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ modelCategoryQuillen.J.rlp.llp Λ[n, i].ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
B : X.Subcomplex
h : range A.ι = B
⊢ B = A

Tactic:
simpa using h.symm

Goal state after:
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))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
h₄ :
  Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)
⊢ (n + 1) * (n + 2) + (n + 1 + (n + 1) + 2) = (n + 2 + 1) * (n + 1 + 1)

Tactic:
lia

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 : ℕ
hd : x.dim = d
i : Fin (d + 1)
h✝ : k.succ ≤ (x.cast hd).simplex.1 i
h : k.succ = (x.cast hd).simplex.1 i
⊢ i ∈ finset x hd

Tactic:
simpa using h.symm

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

Goal state before:
pp: case refine_1.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (n + 1)
i : Fin (d + 1)
hi : (x.cast hd).simplex.2 (l.castSucc.succAbove i) = j
⊢ ∃ x_1, (x.cast hd).simplex.2 (l.castSucc.succAbove x_1) = j

Tactic:
exact ⟨_, hi⟩

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

Goal state before:
pp: case refine_2.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (m + 1 + 1)
hj : ¬j = k.castSucc
i : Fin (d + 1)
hi : (x.cast hd).simplex.1 (l.castSucc.succAbove i) = j
⊢ ∃ x_1, (x.cast hd).simplex.1 (l.castSucc.succAbove x_1) = j

Tactic:
exact ⟨_, hi⟩

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : l.l ≫ (G.obj (op Y₁)).map f₃ = adj₂.homEquiv (Arrow.Hom.right α)
⊢ adj₂.homEquiv.symm (adj₂.homEquiv (Arrow.Hom.right α)) = Arrow.Hom.right α

Tactic:
Equiv.symm_apply_apply

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : l.l ≫ (G.obj (op Y₁)).map f₃ = adj₂.homEquiv (Arrow.Hom.right α)
⊢ Arrow.Hom.right α = Arrow.Hom.right α
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ ¬1 = n

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (Cocone.precompose
          (parallelPair.ext
              (-Iso.refl
                  ((parallelPair
                        ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                          (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                        0).obj
                    WalkingParallelPair.zero))
              (Iso.refl
                ((parallelPair
                      ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                        (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                      0).obj
                  WalkingParallelPair.one))
              ⋯ ⋯).inv).obj
      (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯)) ≅
    CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯

Tactic:
refine Cofork.ext (Iso.refl _) ?_
    ext
    simp [chainComplex, SSet.chainComplexFunctor, π₀.fromChainComplexXZero]

Goal state after: