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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
j : Fin (n + 2)
hj : j ≠ i
⊢ ι i j hj ≫ hf.desc ≫ p = ι i j hj ≫ Λ[n + 1, i].ι ≫ b

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
sq : CommSq hf.desc Λ[n + 1, i].ι p b
j : Fin (n + 2)
hj : j ≠ i
⊢ stdSimplex.δ j ≫ sq.lift = f j hj

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
sq : CommSq hf.desc Λ[n + 1, i].ι p b
⊢ sq.lift ≫ p = b

Tactic:
by

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
⊢ ∀ {x y z : X₁ ⊕ X₂}, Rel' f g x y → Rel' f g y z → Rel' f g x z

Tactic:
by

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ ∀ (a b : X₁ ⊕ X₂), Rel f g a b → Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
⊢ ∃ φ, (∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj) ∧ φ ≫ p = b

Tactic:
by

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ ∀ (a b : X₁ ⊕ X₂), Rel' f g a b → Quot.mk (Rel f g) a = Quot.mk (Rel f g) b

Tactic:
by

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.LeftInverse (Quot.lift (Quot.mk (Rel f g)) ⋯) (Quot.lift (Quot.mk (Rel' f g)) ⋯)

Tactic:
by

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

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 ↔ Rel' f g a b

Tactic:
by

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

Goal state before:
pp: S : SSet
inst✝ : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
⊢ σ₀ ≫ terminal.from S = Λ[n + 1, i].ι ≫ terminal.from Δ[n + 1]

Tactic:
by

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

Goal state before:
pp: S : SSet
inst✝ : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
sq' : CommSq σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from Δ[n + 1])
⊢ σ₀ = Λ[n + 1, i].ι ≫ sq'.lift

Tactic:
by

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

Goal state before:
pp: S : SSet
inst✝ : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[n + 1, i].ι ≫ σ

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst✝ : X.KanComplex
hf : horn.IsCompatible f
⊢ ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ terminal.from X = stdSimplex.δ j ≫ terminal.from Δ[n + 1]

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst✝ : X.KanComplex
hf : horn.IsCompatible f
⊢ ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj

Tactic:
by

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
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom (inl f g)) x₁ = (ConcreteCategory.hom (inr f g)) x₂ ↔
    ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

Tactic:
by

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
⊢ Mono (inr f g)

Tactic:
by

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
⊢ (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

Tactic:
by

Goal state after:
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
n : ℕ
X Y : SSet
i : Fin (n + 2)
t : Λ[n + 1, i].toSSet ⟶ Z
x✝¹ : Δ[n + 1] ⟶ ⊤_ SSet
x✝ : CommSq t Λ[n + 1, i].ι (terminal.from Z) x✝¹
φ : Δ[n + 1] ⟶ Z
hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = horn.ι i j hj ≫ t
⊢ ∀ (j : Fin (n + 2)) (hj : j ≠ i), horn.ι i j hj ≫ Λ[n + 1, i].ι ≫ φ = horn.ι i j hj ≫ t

Tactic:
by

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ ↔
    (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

Tactic:
by

Goal state after:
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₂
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
by

Goal state after:
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
n : ℕ
X Y : SSet
i : Fin (n + 2)
t : Λ[n + 1, i].toSSet ⟶ Z
x✝¹ : Δ[n + 1] ⟶ ⊤_ SSet
x✝ : CommSq t Λ[n + 1, i].ι (terminal.from Z) x✝¹
φ : Δ[n + 1] ⟶ Z
hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = horn.ι i j hj ≫ t
⊢ φ ≫ terminal.from Z = x✝¹

Tactic:
by

Goal state after:
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 c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ ↔
    ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

Tactic:
by

Goal state after:
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
inst✝ : Mono f
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
by

Goal state after:
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
inst✝ : Mono f
⊢ Mono c.inr

Tactic:
by

Goal state after:
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)
⊢ Function.Injective ⇑(ConcreteCategory.hom c.inr)

Tactic:
by

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

Goal state before:
pp: Z : SSet
⊢ Z.KanComplex ↔
    ∀ ⦃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

Tactic:
by

Goal state after:
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
x : (span t l).obj none
⊢ (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom (h.cocone.ι.app none)) x

Tactic:
by

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

Goal state before:
pp: S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
σ₀ : Λ[n, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[n, i].ι ≫ σ

Tactic:
by

Goal state after:
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)
⊢ ∃ σ, σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
by

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

Goal state before:
pp: S X : SSet
t : Limits.IsTerminal X
h : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (t.from S)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h0 : 0 < i
hn : i < Fin.last (n + 2)
this : HasLiftingProperty Λ[n + 2, i].ι (t.from S) := h h0 hn
⊢ σ₀ = Λ[n + 2, i].ι ≫ ⋯.lift

Tactic:
by

Goal state after:
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
x₄ : X₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨ ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄

Tactic:
by

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

Goal state before:
pp: ⊢ 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: ⊢ 1 ≠ 0

Tactic:
by

Goal state after:
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
x₄ : X₄
x₁ : X₁
hx₃ : (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁) = x₄
⊢ (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x₁) = x₄

Tactic:
by

Goal state after:
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
x₄ : X₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

Tactic:
by

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2} = Λ[2, 0]

Tactic:
by

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 1} ⊓ stdSimplex.face {0, 2} = stdSimplex.face {0}

Tactic:
by

Goal state after:
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)
⊢ IsPullback t l r b

Tactic:
by

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

Goal state before:
pp: ⊢ 0 < 1

Tactic:
by

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

Goal state before:
pp: ⊢ 0 < 2

Tactic:
by

Goal state after:
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' : Mono (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)
x₁ y₁ : (fun X ↦ X) X₁
h : (ConcreteCategory.hom l) x₁ = (ConcreteCategory.hom l) y₁
⊢ (ConcreteCategory.hom (l ≫ b ≫ k)) x₁ = (ConcreteCategory.hom (l ≫ b ≫ k)) y₁

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions Λ[n, i].ι

Tactic:
by

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

Goal state before:
pp: ⊢ IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂

Tactic:
by

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

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ Subcomplex.ofSimplex ↑x ≤ Subcomplex.ofSimplex ↑x

Tactic:
by

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

Goal state before:
pp: ⊢ 2 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: ⊢ innerHornInclusions = ⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι

Tactic:
by

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
by

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

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ Subcomplex.ofSimplex ↑x ≤ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
by

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

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ ↑k < j

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X : SSet
⊢ X.Quasicategory ↔ InnerFibration (terminal.from X)

Tactic:
by

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

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
⊢ (fun n ↦ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x) i ≤ (fun n ↦ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x) j

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
hY : IsTerminal Y
⊢ X.Quasicategory ↔ InnerFibration p

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : Y.Quasicategory
⊢ X.Quasicategory

Tactic:
by

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

Goal state before:
pp: X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w✝ : Epi f
y : ↑(X.nonDegenerate j)
⊢ Subcomplex.ofSimplex ↑y ≤ Subcomplex.ofSimplex ↑y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X : SSet
inst✝ : X.Quasicategory
⊢ InnerFibration (terminal.from X)

Tactic:
by

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

Goal state before:
pp: X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w✝ : Epi f
y : ↑(X.nonDegenerate j)
⊢ Subcomplex.ofSimplex ↑y ≤ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
by

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

Goal state before:
pp: X : SSet
i : ℕ
x : X _⦋i⦌
n : ℕ
hi : i < n
⊢ x ∈ (X.skeleton n).obj (op ⦋i⦌)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
i : ℕ
x : X _⦋i⦌
n : ℕ
hi : i < n
⊢ Subcomplex.ofSimplex x ≤ X.skeleton n

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
x : ↑(X.nonDegenerate d)
n : ℕ
⊢ ↑x ∈ (X.skeleton n).obj (op ⦋d⦌) ↔ d < n

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ X.skeleton 0 = ⊥

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ ⨆ n, X.skeleton n ≤ ⊤

Tactic:
by

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2} = Λ[2, 1]

Tactic:
by

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 1} ⊓ stdSimplex.face {1, 2} = stdSimplex.face {1}

Tactic:
by

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

Goal state before:
pp: ⊢ 1 < 2

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
a✝ : ↑x ∈ ⊤.obj (op ⦋n⦌)
⊢ n < n + 1

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ ⊤ ≤ ⨆ n, X.skeleton n

Tactic:
by

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

Goal state before:
pp: ⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂

Tactic:
by

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

Goal state before:
pp: ⊢ 1 ≠ 2

Tactic:
by

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

Goal state before:
pp: ⊢ 0 ≠ 2

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
hd✝ : d < d + 1
hd : d ≤ d
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ Subcomplex.ofSimplex ↑x

Tactic:
by

Goal state after:
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
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
hr' : Mono r'
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₃
⊢ Mono k

Tactic:
by

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} = Λ[2, 2]

Tactic:
by

Goal state after:
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₃
⊢ t ≫ r = l ≫ b

Tactic:
by

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 2} ⊓ stdSimplex.face {1, 2} = stdSimplex.face {2}

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
⊢ n ≤ n + 1

Tactic:
by

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

Goal state before:
pp: ⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
⊢ n < n + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ ⨆ i_1, stdSimplex.face {↑i_1}ᶜ = Λ[n, i]

Tactic:
by

Goal state after:
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
⊢ pushout.inl t l ≫ φ ≫ k = r'

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ pushout.inr t l ≫ φ ≫ k = b'

Tactic:
by

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n m : ℕ
h : n ≤ m
⊢ (fun n ↦ Subcomplex.range i ⊔ Y.skeleton n) n ≤ (fun n ↦ Subcomplex.range i ⊔ Y.skeleton n) m

Tactic:
by

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ (skeletonOfMono i) 0 = Subcomplex.range i

Tactic:
by

Goal state after: