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

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
⊢ IsIso φ

Tactic:
rw [isIso_iff_bijective]

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
k : Fin (n + 3)
hk : k ≠ i
j : Fin (n + 2)
hj : j.castSucc ≠ i
hjk : j.castSucc < k
⊢ stdSimplex.δ (k.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k hk

Tactic:
obtain ⟨k, rfl⟩ := k.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hjk)

Goal state after:
case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map (tr (diag l) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (subinterval j l hjl) ⋯ ?h).op)) (sx.spineToSimplex m ?h f))

pp: case h
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ m ≤ n + 1

Tactic:
← Functor.map_comp_apply,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map ((tr (subinterval j l hjl) ⋯ ?h).op ≫ (tr (diag l) ⋯ ⋯).op)))
      (sx.spineToSimplex m ?h f)

case h
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ m ≤ n + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋a⦌ i) ⋯ hₐ).op)) ((ConcreteCategory.hom (X.map φ.op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ

Tactic:
← Functor.map_comp_apply,

Goal state after:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (φ.op ≫ (tr (⦋0⦌.const ⦋a⦌ i) ⋯ hₐ).op))) Δ =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f)) =
    f.vertex i.castSucc

Tactic:
← Functor.map_comp_apply,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f)) =
    f.vertex i.succ

Tactic:
← Functor.map_comp_apply,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f)) =
    f.arrow i.castSucc

Tactic:
← Functor.map_comp_apply,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (mkOfSucc i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ) =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i

Tactic:
← Functor.map_comp_apply,

Goal state after:
case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (ConcreteCategory.hom (X.map ((tr (subinterval j l h) ⋯ hₘ).op ≫ (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯).op))) Δ =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f)) =
    f.arrow i.succ

Tactic:
← Functor.map_comp_apply,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (mkOfSucc i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ) =
    Path.arrow
      { vertex := fun i ↦ (X.spine m hₘ Δ).vertex ⟨j + ↑i, ⋯⟩,
        arrow := fun i ↦ (ConcreteCategory.hom (X.map (tr (mkOfSucc ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ, arrow_src := ⋯,
        arrow_tgt := ⋯ }
      i

Tactic:
← Functor.map_comp_apply,

Goal state after:
case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (ConcreteCategory.hom (X.map ((tr (subinterval j l h) ⋯ hₘ).op ≫ (tr (mkOfSucc i) ⋯ ⋯).op))) Δ =
    Path.arrow
      { vertex := fun i ↦ (X.spine m hₘ Δ).vertex ⟨j + ↑i, ⋯⟩,
        arrow := fun i ↦ (ConcreteCategory.hom (X.map (tr (mkOfSucc ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ, arrow_src := ⋯,
        arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f)) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)

Tactic:
← Functor.map_comp_apply,

Goal state after:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (mkOfSucc i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (ConcreteCategory.hom (X.map (intervalEdge j l hjl).op)) (sx.spineToSimplex f) =
    (ConcreteCategory.hom (X.map (diag l).op))
      ((ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f))

Tactic:
← Functor.map_comp_apply,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (ConcreteCategory.hom (X.map (intervalEdge j l hjl).op)) (sx.spineToSimplex f) =
    (ConcreteCategory.hom (X.map ((subinterval j l hjl).op ≫ (diag l).op))) (sx.spineToSimplex f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (X.map (δ 0).op)) x) =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
← Functor.map_comp_apply,

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map ((δ 0).op ≫ (mkOfSucc i).op))) x = ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ i).op)) ((ConcreteCategory.hom (X.map (δ j).op)) (sx.spineToSimplex f)) =
    f.vertex i.castSucc

Tactic:
← Functor.map_comp_apply,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map ((δ j).op ≫ (⦋0⦌.const ⦋n⦌ i).op))) (sx.spineToSimplex f) = f.vertex i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ i).op)) ((ConcreteCategory.hom (X.map (δ j).op)) (sx.spineToSimplex f)) =
    f.vertex i.succ

Tactic:
← Functor.map_comp_apply,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map ((δ j).op ≫ (⦋0⦌.const ⦋n⦌ i).op))) (sx.spineToSimplex f) = f.vertex i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (X.map (δ j).op)) (sx.spineToSimplex f)) =
    f.arrow i.castSucc

Tactic:
← Functor.map_comp_apply,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map ((δ j).op ≫ (mkOfSucc i).op))) (sx.spineToSimplex f) = f.arrow i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (X.map (δ j).op)) (sx.spineToSimplex f)) =
    f.arrow i.succ

Tactic:
← Functor.map_comp_apply,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map ((δ j).op ≫ (mkOfSucc i).op))) (sx.spineToSimplex f) = f.arrow i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (X.map (δ j).op)) (sx.spineToSimplex f)) =
    sx.spineToDiagonal (f.interval (↑i) 2 ⋯)

Tactic:
← Functor.map_comp_apply,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map ((δ j).op ≫ (mkOfSucc i).op))) (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval (↑i) 2 ⋯)
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑(horn.primitiveTriangle i h₀ hₙ ↑k ⋯))) z =
    (stdSimplex.objEquiv.symm (mkOfSucc k ≫ SimplexCategory.δ j)) z

Tactic:
rw [mkOfSucc_δ_eq heq]

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑(horn.primitiveTriangle i h₀ hₙ ↑k ⋯))) z =
    (stdSimplex.objEquiv.symm (intervalEdge (↑k) 2 ⋯)) z
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
⊢ ∀ (h1 : (f ≫ g) ≫ h = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i) (h3 : (g ≫ h) ≫ i = g ≫ h ≫ i)
    (h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i),
    hComp (eqToIso h1).hom (𝟙 i) ≫ (eqToIso h2).hom ≫ hComp (𝟙 f) (eqToIso h3).hom =
      (eqToIso h4).hom ≫ (eqToIso pf✝).hom

Tactic:
generalize (f ≫ g) ≫ h = x, (g ≫ h) ≫ i = w

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
x : a✝ ⟶ d✝
w : b✝ ⟶ e✝
⊢ ∀ (h1 : x = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ w) (h3 : w = g ≫ h ≫ i) (h4 : x ≫ i = (f ≫ g) ≫ h ≫ i),
    hComp (eqToIso h1).hom (𝟙 i) ≫ (eqToIso h2).hom ≫ hComp (𝟙 f) (eqToIso h3).hom =
      (eqToIso h4).hom ≫ (eqToIso pf✝).hom
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'
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
1,

Goal state after:
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'
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
⊢ (range ((A.prod B).ι ≫ fst X Y)).obj i✝ ⊆ A.obj i✝

Tactic:
_

Goal state after:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
a✝ : X.obj i✝
⊢ a✝ ∈ (range ((A.prod B).ι ≫ fst X Y)).obj i✝ → a✝ ∈ A.obj i✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
⊢ (range ((A.prod B).ι ≫ snd X Y)).obj i✝ ⊆ B.obj i✝

Tactic:
_

Goal state after:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
a✝ : Y.obj i✝
⊢ a✝ ∈ (range ((A.prod B).ι ≫ snd X Y)).obj i✝ → a✝ ∈ B.obj i✝
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : V
f : x ⟶ y
⊢ motive ((quotientFunctor V).map f)

Tactic:
induction f with
    | nil => simpa using! id x
    | cons _ f h => simpa using! comp_homMk _ f h

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

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
X✝ : FreeRefl V
⊢ ∀ ⦃Y : FreeRefl V⦄ (f : X✝ ⟶ Y), ⊤ f → (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
_

Goal state after:
V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
⊢ ∀ (f : X✝ ⟶ Y✝), ⊤ f → (morphismPropertyHomMk V).multiplicativeClosure f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
X✝ : SimplexCategoryGenRel
⊢ ∀ ⦃Y : SimplexCategoryGenRel⦄ (f : X✝ ⟶ Y), generators.multiplicativeClosure f → P f

Tactic:
_

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
⊢ ∀ (f : X✝ ⟶ Y✝), generators.multiplicativeClosure f → P f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
X✝ : SimplexCategoryGenRel
⊢ ∀ ⦃Y : SimplexCategoryGenRel⦄ (f : X✝ ⟶ Y), generators.multiplicativeClosure' f → P f

Tactic:
_

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
⊢ ∀ (f : X✝ ⟶ Y✝), generators.multiplicativeClosure' f → P f
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelUpperSet (Subtype.val '' s) P
a b : { x // P x }
x : a ≤ b
y : a ∈ s
⊢ ↑a ∈ Subtype.val '' s

Tactic:
simp [a.2, y]

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

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelLowerSet (Subtype.val '' s) P
a b : { x // P x }
x : b ≤ a
y : a ∈ s
⊢ ↑a ∈ Subtype.val '' s

Tactic:
simp [a.2, y]

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
c x✝ : α
b : x✝ ∈ Icc a c
⊢ (fun x ↦ x ≤ c) x✝ ∧ ∀ ⦃b : α⦄, x✝ ≤ b → (fun x ↦ x ≤ c) b → b ∈ Icc a c

Tactic:
by
  simp_all only [mem_Icc, and_true, true_and]
  exact fun _ x _ ↦ b.1.trans x

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : x ∈ (fun s ↦ Finset.image f s) '' K.faces
⊢ x.Nonempty ∧ ∀ ⦃b : Finset β⦄, b ⊆ x → b.Nonempty → b ∈ (fun s ↦ Finset.image f s) '' K.faces

Tactic:
simp only [Set.mem_image] at h ⊢
    obtain ⟨s', hs', rfl⟩ := h
    constructor
    · exact Finset.image_nonempty.mpr (K.isRelLowerSet_faces hs').1
    · intro t hts ht
      obtain ⟨t', ht', rfl⟩ := Finset.subset_image_iff.mp hts
      exact ⟨t', (K.isRelLowerSet_faces hs').2 ht' (Finset.image_nonempty.mp ht), rfl⟩

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

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

Tactic:
_

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

Goal state before:
pp: case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
⊢ sSup x✝ ≤ L

Tactic:
_

Goal state after:
case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
⊢ a✝ ∈ (fun K ↦ K.faces) (sSup x✝) → a✝ ∈ (fun K ↦ K.faces) L
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ map' f x = Fin.last (n + 1) ↔ ∀ (i : Fin (n + 1)), (f i).castSucc < x

Tactic:
by
  simp only [map', Finset.min'_eq_iff, last_mem_finset, Fin.last_le_iff, true_and]
  constructor
  · intro h i
    by_contra!
    exact i.castSucc_ne_last (h i.castSucc (by simpa))
  · intro h i hi
    by_contra!
    obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last this
    simp only [castSucc_mem_finset_iff] at hi
    exact hi.not_gt (h i)

Goal state after: