mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ prod (Quotient.mk a✝) (Quotient.mk b✝) ⬝ prod r₁ r₂ = prod (Quotient.mk a✝ ⬝ r₁) (Quotient.mk b✝ ⬝ r₂)

Tactic:
induction r₁, r₂ using Path.Homotopic.Quotient.ind₂

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a✝¹ : Path a₁ a₂
b✝¹ : Path b₁ b₂
a✝ : Path a₂ a₃
b✝ : Path b₂ b₃
⊢ prod (Quotient.mk a✝¹) (Quotient.mk b✝¹) ⬝ prod (Quotient.mk a✝) (Quotient.mk b✝) =
    prod (Quotient.mk a✝¹ ⬝ Quotient.mk a✝) (Quotient.mk b✝¹ ⬝ Quotient.mk b✝)
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
⊢ PathConnectedSpace X

Tactic:
have : ∀ x, Joined p x := fun x => ⟨(h.evalAt x).symm⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ PathConnectedSpace X
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
t x : ↑I
hx : x ∈ {0, 1}
⊢ { toFun := fun x ↦ (⇑f ∘ ⇑F) (t, x), continuous_toFun := ⋯ } x = (p.map ⋯).toContinuousMap x

Tactic:
rcases hx with hx | hx
    · simp [hx]
    · rw [Set.mem_singleton_iff] at hx
      simp [hx]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) =
    inv (adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj (mk X))))

Tactic:
push inv

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) =
    adjCounitIso.inv.app (bifibrantResolution.obj (toHoCat.obj (mk X)))
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) =
    inv (BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.hom.app (BifibrantObject.toHoCat.obj X)))

Tactic:
push inv

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) =
    BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.inv.app (BifibrantObject.toHoCat.obj X))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
k : Fin (n + 3)
hk : k ∉ S
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, not_or, S] at hk

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = j 0
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case «0»
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = j 0
⊢ ¬j ((fun i ↦ i) ⟨0, ⋯⟩) = k

Tactic:
exact Ne.symm hk.2

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

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : {i, a, b} = univ
⊢ False

Tactic:
by
      have := Finset.card_le_card hS.symm.le
      simp only [card_univ, Fintype.card_fin] at this
      lia

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ stdSimplex.face {↑j, ↑k}ᶜ = stdSimplex.face {↑j}ᶜ ⊓ stdSimplex.face {↑k}ᶜ

Tactic:
rw [stdSimplex.face_inter_face]

Goal state after:
n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ stdSimplex.face {↑j, ↑k}ᶜ = stdSimplex.face ({↑j}ᶜ ⊓ {↑k}ᶜ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
y : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : x ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
h : (ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) ⟨x, hx⟩ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y
⊢ ∃ x₁,
    (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = ⟨x, hx⟩ ∧ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = y

Tactic:
Subtype.ext_iff

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
y : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : x ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
h : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) ⟨x, hx⟩) = ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y)
⊢ ∃ x₁,
    (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = ⟨x, hx⟩ ∧ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ⋯⟩) =
    ⟨↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)), hx⟩

Tactic:
Subtype.ext_iff

Goal state after:
case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ ↑((ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ⋯⟩)) =
    ↑⟨↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)), hx⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case inr
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = y
f : op ⦋d⦌ ⟶ op n
hx : (ConcreteCategory.hom (Y.map f)) y ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈ ⊤.obj (op n)
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ (ConcreteCategory.hom ((b i d).app (op n)))
      ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f.unop)) =
    ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩

Tactic:
Subtype.ext_iff

Goal state after:
case inr
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = y
f : op ⦋d⦌ ⟶ op n
hx : (ConcreteCategory.hom (Y.map f)) y ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈ ⊤.obj (op n)
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ ↑((ConcreteCategory.hom ((b i d).app (op n)))
        ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f.unop))) =
    ↑⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : SimplexCategory
hm : m.len ≤ n + 1
x : X.obj (op { obj := m, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := m, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := m, property := hm }))).toFun x

Tactic:
induction m using SimplexCategory.rec with | _ m

Goal state after:
case mk
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m⦌, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋m⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋m⦌, property := hm }))).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h :
  (ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
      ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁)) =
    (ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
      ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂))
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)

Tactic:
Subtype.ext_iff

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ hComp (hComp η θ) κ = eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯

Tactic:
by
  ext
  simp only [hComp, base_mk, Hom.base_comp, Hom.base_eqToHom,
    ← heq_eq_eq, heq_eqToHom_comp_iff, heq_comp_eqToHom_iff,
    eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]
  conv => enter [1, 2]; exact ((id_comp _).trans (comp_id _)).symm
  conv => enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm
  iterate 4 rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]
  simp [CatEnriched.hComp_assoc_heq]

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F : V ⥤rq D
⊢ ∀ (x y : Paths V) (f₁ f₂ : x ⟶ y),
    FreeReflRel V x y f₁ f₂ → (Paths.lift F.toPrefunctor).map f₁ = (Paths.lift F.toPrefunctor).map f₂

Tactic:
by
    rintro _ _ _ _ ⟨h⟩
    simp

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

Goal state before:
pp: x y : OneTruncation₂ ((truncation 2).obj Δ[0])
x✝ : x ⟶ y
⊢ x✝ = ⋯ ▸ ⋯ ▸ 𝟙rq default

Tactic:
let : Subsingleton (((truncation 2).obj Δ[0]).obj (.op ⦋1⦌2)) :=
      inferInstanceAs (Subsingleton (ULift.{_, 0} (⦋1⦌ ⟶ ⦋0⦌)))

Goal state after:
x y : OneTruncation₂ ((truncation 2).obj Δ[0])
x✝ : x ⟶ y
this : Subsingleton (((truncation 2).obj Δ[0]).obj (op { obj := ⦋1⦌, property := ⋯ })) :=
  SSet.instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk._proof_1
⊢ x✝ = ⋯ ▸ ⋯ ▸ 𝟙rq default
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.succ) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j.castSucc))
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_of_gt H

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ upperBounds x✝

Tactic:
intro K hK _ ht

Goal state after:
case left
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
K : AbstractSimplicialComplex ι
hK : K ∈ x✝
a✝ : Finset ι
ht : a✝ ∈ (fun K ↦ K.faces) K
⊢ a✝ ∈ (fun K ↦ K.faces) (sSup x✝)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mpr.inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
hi : Fin.last (n + 1) ∈ finset f x
⊢ y.castSucc ≤ Fin.last (n + 1)

Tactic:
apply Fin.le_last

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝¹ : P.IsProper
inst✝ : P.IsInner
⊢ ∀ (x : ↑(P.ofIso e hA).II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ 0

Tactic:
rintro ⟨b, hb⟩ d hd

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝¹ : P.IsProper
inst✝ : P.IsInner
b : B.N
hb : b ∈ (P.ofIso e hA).II
d : ℕ
hd : (↑⟨b, hb⟩).dim = d
⊢ ⋯.index hd ≠ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝¹ : P.IsProper
inst✝ : P.IsInner
⊢ ∀ (x : ↑(P.ofIso e hA).II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ Fin.last (d + 1)

Tactic:
rintro ⟨b, hb⟩ d hd

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝¹ : P.IsProper
inst✝ : P.IsInner
b : B.N
hb : b ∈ (P.ofIso e hA).II
d : ℕ
hd : (↑⟨b, hb⟩).dim = d
⊢ ⋯.index hd ≠ Fin.last (d + 1)
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 ι
⊢ Monotone f.filtration

Tactic:
intro i₁ i₂ h

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
h : i₁ ≤ i₂
⊢ f.filtration i₁ ≤ f.filtration i₂
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
⊢ ∃ j x', x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

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
⊢ ∃ j x', x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'
Module: Mathlib.CategoryTheory.Presentable.Retracts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : EssentiallySmall.{max ?u.47 w, w, w} J
⊢ IsColimit ((coyoneda.obj (Opposite.op Y)).mapCocone c)

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this✝ : EssentiallySmall.{max ?u.47 w, w, w} J
this : IsFiltered J
⊢ IsColimit ((coyoneda.obj (Opposite.op Y)).mapCocone c)
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₂
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

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
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂
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

Goal state after:
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
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋x.dim + 1⦌)))) ∈
    (f.sigmaStdSimplex j).nonDegenerate (x.dim + 1)
hs : Mono (𝟙 (unop (op ⦋x.dim + 1⦌)))
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋x.dim + 1⦌)))) ∉
    (range (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' : stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋x.dim + 1⦌))) ∉ Λ[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 (𝟙 (unop (op ⦋x.dim + 1⦌)))))
          hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)))
            (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋x.dim + 1⦌)))))
          hs✝ hs'✝ =
        Cell.type₂ f c
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 : ℕ
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
y : X _⦋d⦌
hy : y ∈ (f.filtration j).obj (op ⦋d⦌)
h :
  ⟨↑⟨y, hy⟩, ⋯⟩ =
    (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
⊢ b ∈ ((f.filtration j).preimage x.map).obj (op ⦋d⦌)

Tactic:
Subtype.ext_iff

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 : ℕ
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
y : X _⦋d⦌
hy : y ∈ (f.filtration j).obj (op ⦋d⦌)
h :
  ↑⟨↑⟨y, hy⟩, ⋯⟩ =
    ↑((ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b))
⊢ b ∈ ((f.filtration j).preimage x.map).obj (op ⦋d⦌)
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)
⊢ IsColimit (c.pt.mapCocone cX)

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

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)
this : IsFiltered J
⊢ IsColimit (c.pt.mapCocone cX)