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

Goal state before:
pp: case refine_1
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ ⟨k, ⋯⟩ ≤ ⟨k + 1, ⋯⟩

pp: case refine_2
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ ⟨k + 1, ⋯⟩ ≤ ⟨k + 2, ⋯⟩

pp: case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ?refine_1 ?refine_2 ∈ Λ[n + 3, i].obj (op ⦋2⦌)

Tactic:
· simp only [Fin.mk_le_mk, le_add_iff_nonneg_right, zero_le]

Goal state after:
case refine_2
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ ⟨k + 1, ⋯⟩ ≤ ⟨k + 2, ⋯⟩

case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ?refine_2 ∈ Λ[n + 3, i].obj (op ⦋2⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : Fin.last (n + 3) ∈ {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩}
⊢ False

Tactic:
]

Goal state after:
case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : Fin.last (n + 3) ∈ {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩}
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
hS : {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
hk : ¬k = 0
this : 0 ∈ {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ False

Tactic:
]

Goal state after:
case neg
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
hS : {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
hk : ¬k = 0
this : 0 ∈ {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ∃ x, x ∉ {i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1

Tactic:
]

Goal state after:
case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ∃ x, x ∉ {i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ Subfunctor.equalizer σ₁ σ₂ = Λ[n + 1, i]

Tactic:
]

Goal state after:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ Subfunctor.equalizer σ₁ σ₂ = Λ[n + 1, i]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ face i j hij = face i j hij

Tactic:
]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ stdSimplex.δ j = stdSimplex.δ j

Tactic:
]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij = (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij

Tactic:
]

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij = (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₁ : X₁
hyz :
  (ConcreteCategory.hom f) y₀✝ = z₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) x₀ ∧ z₁ = (ConcreteCategory.hom f) y₀
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl z₁)

Tactic:
]

Goal state after:
case inl_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₁ : X₁
hyz :
  (ConcreteCategory.hom f) y₀✝ = z₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) x₀ ∧ z₁ = (ConcreteCategory.hom f) y₀
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl z₁)
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ y₁ : F₁.obj j
h : (hom (c₂.ι.app j)) ((hom (f.app j)) x₁) = (hom (c₂.ι.app j)) ((hom (f.app j)) y₁)
k : J
α : j ⟶ k
hk : (hom (f.app k)) ((hom (F₁.map α)) x₁) = (hom (f.app k)) ((hom (F₁.map α)) y₁)
⊢ (hom (c₁.ι.app k)) ((hom (F₁.map α)) y₁) = (hom (c₁.ι.app k)) ((hom (F₁.map α)) y₁)

Tactic:
]

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

Goal state before:
pp: case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₂ : X₂
hyz : ∃ s, (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) s ∧ z₂ = (ConcreteCategory.hom g) s
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)

Tactic:
]

Goal state after:
case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₂ : X₂
hyz : ∃ s, (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) s ∧ z₂ = (ConcreteCategory.hom g) s
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ cofibrations SSet f ↔ Mono f

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ cofibrations SSet f ↔ Mono f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ fibrations SSet f ↔ J.rlp f

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ fibrations SSet f ↔ J.rlp f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Cofibration f

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Cofibration f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : Mono f
⊢ Mono f

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝ : Mono f
⊢ Mono f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
hf : J.rlp f
n : ℕ
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι f

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
hf : J.rlp f
n : ℕ
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ J.rlp.IsMultiplicative

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ J.rlp.IsMultiplicative
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ J.rlp.IsStableUnderRetracts

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ J.rlp.IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (monomorphisms SSet).IsMultiplicative

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ (monomorphisms SSet).IsMultiplicative
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
hs : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr ((ConcreteCategory.hom g) x₀✝))

Tactic:
]

Goal state after:
case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
hs : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr ((ConcreteCategory.hom g) x₀✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (monomorphisms SSet).IsStableUnderRetracts

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ (monomorphisms SSet).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
⊢ J.rlp f

Tactic:
]

Goal state after:
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
⊢ J.rlp f
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : ∃ s_1, z₁ = (ConcreteCategory.hom f) s_1 ∧ (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s_1
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)

Tactic:
]

Goal state after:
case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : ∃ s_1, z₁ = (ConcreteCategory.hom f) s_1 ∧ (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s_1
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
]

Goal state after:
case inl_inr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₂ : X₂
hyz : (ConcreteCategory.hom g) s = z₂
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr z₂)
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 :
  (ConcreteCategory.hom f) s✝ = z₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) x₀ ∧ z₁ = (ConcreteCategory.hom f) y₀
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl z₁)

Tactic:
]

Goal state after:
case inr_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₁ : X₁
hyz :
  (ConcreteCategory.hom f) s✝ = z₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) x₀ ∧ z₁ = (ConcreteCategory.hom f) y₀
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl z₁)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
]

Goal state after:
case inr_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝ : S
h : (ConcreteCategory.hom g) s✝ = (ConcreteCategory.hom g) w✝
h' : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s✝
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) w✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
]

Goal state after:
case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₂ : X₂
hyz : ∃ s, (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s ∧ z₂ = (ConcreteCategory.hom g) s
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr z₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) y₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))

Tactic:
]

Goal state after:
case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) y₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ Function.LeftInverse (Quot.lift (Quot.mk (Rel f g)) ⋯) (Quot.lift (Quot.mk (Rel' f g)) ⋯)

Tactic:
by rintro ⟨x⟩; rfl

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ Function.RightInverse (Quot.lift (Quot.mk (Rel f g)) ⋯) (Quot.lift (Quot.mk (Rel' f g)) ⋯)

Tactic:
by rintro ⟨x⟩; rfl

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b

Tactic:
]

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

Goal state before:
pp: Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
⊢ J.rlp (terminal.from Z)

Tactic:
]

Goal state after:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
⊢ J.rlp (terminal.from Z)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (inr f g))

Tactic:
]

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (inr f g))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective ⇑(ConcreteCategory.hom f)
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom (Pushout.cocone f g).inl) x₁ = (ConcreteCategory.hom (Pushout.cocone f g).inr) x₂ ↔
    ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

Tactic:
]

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective ⇑(ConcreteCategory.hom f)
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom (Pushout.cocone f g).inl) x₁ = (ConcreteCategory.hom (Pushout.cocone f g).inr) x₂ ↔
    ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Mono f
⊢ Mono c.inr

Tactic:
]

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Mono f
⊢ Mono c.inr
Module: Mathlib.AlgebraicTopology.Quasicategory.Basic

Goal state before:
pp: S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
    (ConcreteCategory.hom (Λ[n + 2, i].ι.app (Opposite.op ⦋n + 1⦌) ≫ (yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌)))
      (horn.face i j hj)

Tactic:
]

Goal state after:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
    (ConcreteCategory.hom (Λ[n + 2, i].ι.app (Opposite.op ⦋n + 1⦌) ≫ (yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌)))
      (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 0] ∧ stdSimplex.face {0, 2} ≤ Λ[2, 0]

Tactic:
]

Goal state after:
case a
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 0] ∧ stdSimplex.face {0, 2} ≤ Λ[2, 0]
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ ∀ (i : ↑{0}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}

Tactic:
]

Goal state after:
case a
⊢ ∀ (i : ↑{0}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht : Function.Injective ⇑(ConcreteCategory.hom t)
⊢ t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun X ↦ X) X₁),
        (ConcreteCategory.hom t) x₁ = (ConcreteCategory.hom t) y₁ ∧
            (ConcreteCategory.hom l) x₁ = (ConcreteCategory.hom l) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃),
        (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) x₃ →
          ∃ x₁, (ConcreteCategory.hom t) x₁ = x₂ ∧ (ConcreteCategory.hom l) x₁ = x₃

Tactic:
]

Goal state after:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht : Function.Injective ⇑(ConcreteCategory.hom t)
⊢ t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun X ↦ X) X₁),
        (ConcreteCategory.hom t) x₁ = (ConcreteCategory.hom t) y₁ ∧
            (ConcreteCategory.hom l) x₁ = (ConcreteCategory.hom l) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃),
        (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) x₃ →
          ∃ x₁, (ConcreteCategory.hom t) x₁ = x₂ ∧ (ConcreteCategory.hom l) x₁ = x₃
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₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
⊢ Function.Injective ⇑(ConcreteCategory.hom k)

Tactic:
]

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₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
⊢ Function.Injective ⇑(ConcreteCategory.hom k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 1] ∧ stdSimplex.face {1, 2} ≤ Λ[2, 1]

Tactic:
]

Goal state after:
case a
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 1] ∧ stdSimplex.face {1, 2} ≤ Λ[2, 1]
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X : SSet
⊢ (∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (terminalIsTerminal.from X)) ↔
    innerFibrations (terminal.from X)

Tactic:
]

Goal state after:
X : SSet
⊢ (∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (terminalIsTerminal.from X)) ↔
    innerFibrations (terminal.from X)
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ InnerFibration (terminal.from X)

Tactic:
]

Goal state after:
X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ InnerFibration (terminal.from X)
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ innerFibrations (p ≫ terminal.from Y)

Tactic:
]

Goal state after:
X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ innerFibrations (p ≫ terminal.from Y)
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X : SSet
inst✝ : X.Quasicategory
⊢ X.Quasicategory

Tactic:
]

Goal state after:
X : SSet
inst✝ : X.Quasicategory
⊢ X.Quasicategory
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ ∀ (i : ↑{1}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}

Tactic:
]

Goal state after:
case a
⊢ ∀ (i : ↑{1}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d n : ℕ
h : d < n
⊢ ⊤ ⊆ (X.skeleton n).obj (op ⦋d⦌)

Tactic:
]

Goal state after:
X : SSet
d n : ℕ
h : d < n
⊢ ⊤ ⊆ (X.skeleton n).obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
⊢ ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ ⊤.obj (op ⦋n⦌) → ↑x ∈ (⨆ n, X.skeleton n).obj (op ⦋n⦌)

Tactic:
]

Goal state after:
X : SSet
⊢ ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ ⊤.obj (op ⦋n⦌) → ↑x ∈ (⨆ n, X.skeleton n).obj (op ⦋n⦌)