awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin n
j : Fin (n + 1)
hj : i.castSucc.succ < j.succ
zero :
  ∀ (f : X.PtSimplex 0 x) (i : Fin 0) (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hj : i.castSucc.succ < j.succ),
    stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
succ :
  ∀ (n : ℕ) (f : X.PtSimplex (n + 1) x) (i : Fin (n + 1)) (j : Fin (n + 1 + 1)) (hj : i.castSucc.succ < j.succ),
    stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
x : X _⦋0⦌
f : X.PtSimplex 0 x
i : Fin 0
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
hj : i.castSucc.succ < j.succ
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : i.castSucc.succ < j.succ
⊢ i.castSucc < j

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : i.castSucc.succ < j.succ
succ : stdSimplex.σ i ≫ stdSimplex.δ j ≫ f.map = const x
succ₁ : stdSimplex.σ i ≫ const x = const x
succ₂ succ₃ : Eq (α := Δ[n + 1] ⟶ X) (const x) (const x)
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x

Tactic:
rw [stdSimplex.δ_comp_σ_of_gt_assoc (by grind), δ_map, comp_const]

Premises used: CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt_assoc, SSet.stdSimplex, SSet.comp_const, SSet.PtSimplex.δ_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
rw : f.map = f'.map
rw₁ rw₂ : f'.map = f'.map
⊢ stdSimplex.δ i.castSucc ≫ r.map = f'.map

Tactic:
rw [δ_castSucc_map, hf]

Premises used: SSet.PtSimplex.RelStruct.δ_castSucc_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
rw : g.map = g'.map
rw₁ rw₂ : g'.map = g'.map
⊢ stdSimplex.δ i.succ ≫ r.map = g'.map

Tactic:
rw [δ_succ_map, hg]

Premises used: SSet.PtSimplex.RelStruct.δ_succ_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : j < i.castSucc
rw rw₁ : Eq (α := Δ[n] ⟶ X) (const x) (const x)
⊢ stdSimplex.δ j ≫ r.map = const x

Tactic:
rw [δ_map_of_lt _ j hj]

Premises used: SSet.PtSimplex.RelStruct.δ_map_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : i.succ < j
rw rw₁ : Eq (α := Δ[n] ⟶ X) (const x) (const x)
⊢ stdSimplex.δ j ≫ r.map = const x

Tactic:
rw [δ_map_of_gt _ j hj]

Premises used: SSet.PtSimplex.RelStruct.δ_map_of_gt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.castSucc
j : Fin (n + 2)
hj : i.succ.succ < j
⊢ i.castSucc.succ < i.succ.succ

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.castSucc.succ < j
⊢ i.succ.succ ≤ j

Tactic:
rw [Fin.succ_castSucc, Fin.castSucc_lt_iff_succ_le] at hj

Premises used: Fin.succ_castSucc, Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.succ.succ ≤ j
inl : ∀ (hj : i.succ.succ ≤ i.succ.succ), stdSimplex.δ i.succ.succ ≫ h.map = const x
inr : ∀ (hj : i.succ.succ < j), stdSimplex.δ j ≫ h.map = const x
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
obtain rfl | hj := hj.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
hj : i.succ.succ ≤ i.succ.succ
⊢ stdSimplex.δ i.succ.succ ≫ h.map = const x

Tactic:
h.δ_succ_succ_map

Premises used: SSet.const, SSet.PtSimplex.MulStruct.δ_succ_succ_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj_1 : i.succ.succ ≤ j
hj : i.succ.succ < j
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
h.δ_map_of_gt j hj

Premises used: SSet.PtSimplex.MulStruct.δ_map_of_gt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
hj : i.succ.succ ≤ i.succ.succ
⊢ stdSimplex.δ i.succ.succ ≫ h.map = const x

Tactic:
exacts [h.δ_succ_succ_map, h.δ_map_of_gt j hj]

Premises used: SSet.PtSimplex.MulStruct.δ_succ_succ_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.succ
rw : stdSimplex.δ i.succ.castSucc ≫ h.map = f.map
rw₁ rw₂ : f.map = f.map
⊢ stdSimplex.δ i.castSucc.succ ≫ h.map = f.map

Tactic:
rw [← Fin.castSucc_succ, h.δ_castSucc_map]

Premises used: SSet.PtSimplex.RelStruct.δ_castSucc_map, Fin.castSucc_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.succ
j : Fin (n + 2)
hj : j < i.castSucc.castSucc
⊢ i.castSucc.castSucc < i.succ.castSucc

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.succ.castSucc
⊢ j < i.castSucc.succ

Tactic:
rw [← Fin.succ_castSucc] at hj

Premises used: Fin.succ_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.castSucc.succ
inl : ∀ (hj : i.castSucc.castSucc < i.castSucc.succ), stdSimplex.δ i.castSucc.castSucc ≫ h.map = const x
inr : ∀ (hj : j < i.castSucc.castSucc), stdSimplex.δ j ≫ h.map = const x
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
obtain rfl | hj := (Fin.le_castSucc_iff.mpr hj).eq_or_lt

Premises used: Iff.mpr, LE.le.eq_or_lt, Fin.le_castSucc_iff, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
hj : i.castSucc.castSucc < i.castSucc.succ
⊢ stdSimplex.δ i.castSucc.castSucc ≫ h.map = const x

Tactic:
h.δ_castSucc_castSucc_map

Premises used: SSet.const, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj_1 : j < i.castSucc.succ
hj : j < i.castSucc.castSucc
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
h.δ_map_of_lt j hj

Premises used: SSet.PtSimplex.MulStruct.δ_map_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
hj : i.castSucc.castSucc < i.castSucc.succ
⊢ stdSimplex.δ i.castSucc.castSucc ≫ h.map = const x

Tactic:
exacts [h.δ_castSucc_castSucc_map, h.δ_map_of_lt j hj]

Premises used: SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
S : SSet
inst : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
⊢ Eq (α := Λ[n + 1, i].toSSet ⟶ ⊤_ SSet) (σ₀ ≫ terminal.from S) (Λ[n + 1, i].ι ≫ terminal.from Δ[n + 1])

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
S : SSet
inst : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
⊢ CommSq (Z := ⊤_ SSet) σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from Δ[n + 1])

Tactic:
have sq' : CommSq σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from _) := ⟨by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
S : SSet
inst : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
sq' : CommSq (Z := ⊤_ SSet) σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from Δ[n + 1])
⊢ σ₀ = Λ[n + 1, i].ι ≫ sq'.lift

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
S : SSet
inst : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
sq' : CommSq (Z := ⊤_ SSet) σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from Δ[n + 1])
⊢ ∃ (σ : Δ[n + 1] ⟶ S), σ₀ = Λ[n + 1, i].ι ≫ σ

Tactic:
exact ⟨sq'.lift, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
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),
    Eq (α := Δ[n] ⟶ ⊤_ SSet) (f j hj ≫ terminal.from X) (stdSimplex.δ j ≫ terminal.from Δ[n + 1])

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst : X.KanComplex
hf : horn.IsCompatible f
obtain :
  ∀ (φ : Δ[n + 1] ⟶ X) (hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj),
    Eq (α := Δ[n + 1] ⟶ ⊤_ SSet) (φ ≫ terminal.from X) (terminal.from Δ[n + 1]) →
      ∃ (φ : Δ[n + 1] ⟶ X), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
⊢ ∃ (φ : Δ[n + 1] ⟶ X), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj

Tactic:
obtain ⟨φ, hφ, _⟩ := hf.exists_lift (terminal.from _) (terminal.from _) (by simp)

Premises used: CategoryTheory.Limits.terminal.from, SSet.horn.IsCompatible.exists_lift
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst : X.KanComplex
hf : horn.IsCompatible f
φ : Δ[n + 1] ⟶ X
hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
right : Eq (α := Δ[n + 1] ⟶ ⊤_ SSet) (φ ≫ terminal.from X) (terminal.from Δ[n + 1])
⊢ ∃ (φ : Δ[n + 1] ⟶ X), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj

Tactic:
⟨φ, hφ⟩

Premises used: Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst : X.KanComplex
hf : horn.IsCompatible f
φ : Δ[n + 1] ⟶ X
hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
right : Eq (α := Δ[n + 1] ⟶ ⊤_ SSet) (φ ≫ terminal.from X) (terminal.from Δ[n + 1])
⊢ ∃ (φ : Δ[n + 1] ⟶ X), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj

Tactic:
exact ⟨φ, hφ⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
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 ≫ hf.liftOfKanComplex = f j hj

Tactic:
hf.exists_lift_of_kanComplex.choose_spec j hj

Premises used: Exists.choose_spec, SSet.horn.IsCompatible.exists_lift_of_kanComplex, SSet.horn.IsCompatible.liftOfKanComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
⊢ Z.KanComplex ↔
    ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
      horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj

Tactic:
⟨fun _ n i f hf ↦ hf.exists_lift_of_kanComplex,
    fun h ↦ (isFibrant_iff _).2 ⟨?_⟩⟩

Premises used: Iff.mpr, Iff.intro, SSet.horn.IsCompatible.exists_lift_of_kanComplex, HomotopicalAlgebra.isFibrant_iff, HomotopicalAlgebra.Fibration.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
refine :
  ∀
    (h :
      ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
        horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj),
    fibrations SSet (Y := ⊤_ SSet) (terminal.from Z)
⊢ Z.KanComplex ↔
    ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
      horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj

Tactic:
refine ⟨fun _ n i f hf ↦ hf.exists_lift_of_kanComplex,
    fun h ↦ (isFibrant_iff _).2 ⟨?_⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X : SSet
_ : ∀ ⦃Y : SSet.{u}⦄ (g : X ⟶ Y), J g → HasLiftingProperty (Y := ⊤_ SSet) g (terminal.from Z)
⊢ ∀ ⦃Y : SSet.{u}⦄ (g : X ⟶ Y), J g → HasLiftingProperty (Y := ⊤_ SSet) g (terminal.from Z)

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X Y : SSet
_ : ∀ (g : X ⟶ Y), J g → HasLiftingProperty (Y := ⊤_ SSet) g (terminal.from Z)
⊢ ∀ (g : X ⟶ Y), J g → HasLiftingProperty (Y := ⊤_ SSet) g (terminal.from Z)

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X Y : SSet
g : X ⟶ Y
hf : J g
⊢ ∃ (i : ℕ),
    MorphismProperty.ofHoms (X := fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].toSSet) (Y := fun (i_1 : Fin (i + 2)) ↦
      Δ[i + 1]) (fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].ι) g

Tactic:
simp only [J, MorphismProperty.iSup_iff] at hf

Premises used: SSet.modelCategoryQuillen.J, CategoryTheory.MorphismProperty.iSup_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X Y : SSet
g : X ⟶ Y
hf :
  ∃ (i : ℕ),
    MorphismProperty.ofHoms (X := fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].toSSet) (Y := fun (i_1 : Fin (i + 2)) ↦
      Δ[i + 1]) (fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].ι) g
obtain : ∀ (n : ℕ) ⦃X Y : SSet.{u}⦄ (i : Fin (n + 2)), HasLiftingProperty (Y := ⊤_ SSet) Λ[n + 1, i].ι (terminal.from Z)
⊢ HasLiftingProperty (Y := ⊤_ SSet) g (terminal.from Z)

Tactic:
obtain ⟨n, ⟨i⟩⟩ := hf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
⊢ HasLiftingProperty (Y := ⊤_ SSet) Λ[n + 1, i].ι (terminal.from Z)

Tactic:
⟨fun {t _} _ ↦ ?_⟩

Premises used: CategoryTheory.HasLiftingProperty.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
refine :
  ∀ {t : Λ[n + 1, i].toSSet ⟶ Z} {x : Δ[n + 1] ⟶ ⊤_ SSet} (x_1 : CommSq t Λ[n + 1, i].ι (terminal.from Z) x),
    x_1.HasLift
⊢ HasLiftingProperty (Y := ⊤_ SSet) Λ[n + 1, i].ι (terminal.from Z)

Tactic:
refine ⟨fun {t _} _ ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (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
h_1 : CommSq t Λ[n + 1, i].ι (terminal.from Z) x
obtain :
  ∀ (φ : Δ[n + 1] ⟶ Z) (hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = horn.ι i j hj ≫ t), h_1.HasLift
⊢ h_1.HasLift

Tactic:
obtain ⟨φ, hφ⟩ := h _ (horn.IsCompatible.of_hom t)

Premises used: SSet.horn.IsCompatible.of_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (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
h_1 : 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:
simpa using hφ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (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
h_1 : 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:
subsingleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (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
h_1 : 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
⊢ h_1.HasLift

Tactic:
exact ⟨⟨{
    l := φ
    fac_left := horn.hom_ext' (by simpa using hφ)
    fac_right := by subsingleton }⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
Goal:
inst : HasCoproducts (Type u)
⊢ IsStableUnderCoproducts.{v', u, u + 1} (monomorphisms SSet)

Tactic:
inferInstanceAs (IsStableUnderCoproducts.{v'} (monomorphisms (_ ⥤ _)))

Premises used: _private.0.SSet.instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
Goal:
rw :
  IsStableUnderCobaseChange (C := SimplexCategoryᵒᵖ ⥤ Type u_1)
    (functorCategory (monomorphisms (Type u_1)) SimplexCategoryᵒᵖ)
⊢ IsStableUnderCobaseChange.{u_1, u_1 + 1} (C := SimplexCategoryᵒᵖ ⥤ Type u_1)
    (monomorphisms (SimplexCategoryᵒᵖ ⥤ Type u_1))

Tactic:
rw [← functorCategory_monomorphisms]

Premises used: CategoryTheory.MorphismProperty.functorCategory_monomorphisms
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
Goal:
⊢ IsStableUnderCobaseChange (C := SimplexCategoryᵒᵖ ⥤ Type u_1)
    (functorCategory (monomorphisms (Type u_1)) SimplexCategoryᵒᵖ)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
Goal:
J : Type u
x : Category.{u, u} J
h : IsFiltered J
rw :
  IsStableUnderColimitsOfShape (C := SimplexCategoryᵒᵖ ⥤ Type u)
    (functorCategory (monomorphisms (Type u)) SimplexCategoryᵒᵖ) J
⊢ IsStableUnderColimitsOfShape (C := SimplexCategoryᵒᵖ ⥤ Type u) (monomorphisms (SimplexCategoryᵒᵖ ⥤ Type u)) J

Tactic:
rw [← functorCategory_monomorphisms]

Premises used: CategoryTheory.MorphismProperty.functorCategory_monomorphisms
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
Goal:
J : Type u
x : Category.{u, u} J
h : IsFiltered J
⊢ IsStableUnderColimitsOfShape (C := SimplexCategoryᵒᵖ ⥤ Type u)
    (functorCategory (monomorphisms (Type u)) SimplexCategoryᵒᵖ) J

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
Goal:
K : Type u
inst : LinearOrder K
inst_1 : SuccOrder K
inst_2 : OrderBot K
inst_3 : WellFoundedLT K
⊢ IsStableUnderTransfiniteCompositionOfShape (monomorphisms SSet) K

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C D : Type u
inst : Category.{v, u} C
inst_1 : Category.{v, u} D
F : Functor.{v, v, u, u} C D
x : C
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} D _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((nerveMap F).app (op ⦋0⦌)) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve D _⦋0⦌))
        (ComposableArrows.mk₀ x) :
      (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} D _⦋0⦌))
    (ComposableArrows.mk₀ (F.obj x) : ComposableArrows.{v, u} D 0)

Tactic:
ComposableArrows.ext₀ rfl

Premises used: CategoryTheory.ComposableArrows.ext₀, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C D : Type u
inst : Category.{v, u} C
inst_1 : Category.{v, u} D
F : Functor.{v, v, u, u} C D
x y : C
f : x ⟶ y
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((nerveMap F).app (op ⦋1⦌)) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve D _⦋1⦌))
        (ComposableArrows.mk₁ f)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (F.map f)).hom ≫ eqToHom ⋯

Tactic:
simp [nerveMap_app]

Premises used: CategoryTheory.nerveMap_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
f : ComposableArrows.{v, u} C 0
⊢ 0 < HAdd.hAdd (α := ℕ) 0 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
n : ℕ
α : Type u
inst : Preorder α
e : α ≃o Fin (n + 1)
X : SimplexCategory
F : Fin (X.len + 1) ⥤ Fin (⦋n⦌.len + 1)
x : Fin (X.len + 1)
⊢ Functor.obj
      ((fun (F : (nerve α).obj (op X)) ↦ F ⋙ ⋯.functor)
        ((fun (F : Fin (X.len + 1) ⥤ Fin (⦋n⦌.len + 1)) ↦ F ⋙ ⋯.functor) F))
      x =
    F.obj x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
n : ℕ
α : Type u
inst : Preorder α
e : α ≃o Fin (n + 1)
X : SimplexCategory
F : (nerve α).obj (op X)
x : Fin ((unop (op X)).len + 1)
⊢ Functor.obj
      ((fun (F : Fin (X.len + 1) ⥤ Fin (⦋n⦌.len + 1)) ↦ F ⋙ ⋯.functor)
        ((fun (F : (nerve α).obj (op X)) ↦ F ⋙ ⋯.functor) F))
      x =
    F.obj x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
i : Fin (n + 2)
x : ComposableArrows.{v, u} C (n + 1)
j : Fin (n + 1)
⊢ Functor.obj.{0, v, 0, u}
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) i) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋n + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋n⦌))
        x)
      j =
    x.obj (i.succAbove j)

Tactic:
rfl

Premises used: Fin.succAbove, rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
i : Fin (n + 1)
x : ComposableArrows.{v, u} C n
j : Fin (n + 2)
⊢ Functor.obj.{0, v, 0, u}
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) i) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋n⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋n + 1⦌))
        x)
      j =
    x.obj (i.predAbove j)

Tactic:
rfl

Premises used: Fin.predAbove, dite, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
x : ComposableArrows.{v, u} C (n + 1)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋n + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋n⦌))
      x =
    x.δ₀

Tactic:
rfl

Premises used: Fin.succAbove, Fin.succ, CategoryTheory.Functor.comp, CategoryTheory.ComposableArrows.whiskerLeft, rfl, ite