awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.castSucc).op = 𝟙 (X _⦋n⦌)

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_self, op_id, X.map_id]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_id, SimplexCategory.δ_comp_σ_self, CategoryTheory.Functor.map_comp, CategoryTheory.op_id
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
subst : X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)
⊢ X.σ i ≫ X.δ j = 𝟙 (X _⦋n⦌)

Tactic:
subst H
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
rw rw₁ : Eq.{v + 1} (α := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌)) (𝟙 (X _⦋n⦌))
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)

Tactic:
rw [δ_comp_σ_self]

Premises used: CategoryTheory.SimplicialObject.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
dsimp : X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.succ).op = 𝟙 (X _⦋n⦌)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)

Tactic:
dsimp [δ, σ]

Premises used: CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.succ).op = 𝟙 (X _⦋n⦌)

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_succ, op_id, X.map_id]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, SimplexCategory.δ_comp_σ_succ, CategoryTheory.op_id
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
subst : X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)
⊢ X.σ i ≫ X.δ j = 𝟙 (X _⦋n⦌)

Tactic:
subst H
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
rw rw₁ : Eq.{v + 1} (α := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌)) (𝟙 (X _⦋n⦌))
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)

Tactic:
rw [δ_comp_σ_succ]

Premises used: CategoryTheory.SimplicialObject.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
dsimp :
  X.map (SimplexCategory.σ j.castSucc).op ≫ X.map (SimplexCategory.δ i.succ).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
⊢ X.σ j.castSucc ≫ X.δ i.succ = X.δ i ≫ X.σ j

Tactic:
dsimp [δ, σ]

Premises used: CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.σ j.castSucc).op ≫ X.map (SimplexCategory.δ i.succ).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt H]

Premises used: CategoryTheory.op_comp, SimplexCategory.δ_comp_σ_of_gt, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
dsimp :
  X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (i.pred ⋯)).op ≫ X.map (Quiver.Hom.op (SimplexCategory.σ (j.castLT ⋯)))
⊢ X.σ j ≫ X.δ i = X.δ (i.pred ⋯) ≫ X.σ (j.castLT ⋯)

Tactic:
dsimp [δ, σ]

Premises used: CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (i.pred ⋯)).op ≫ X.map (Quiver.Hom.op (SimplexCategory.σ (j.castLT ⋯)))

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]

Premises used: CategoryTheory.op_comp, SimplexCategory.δ_comp_σ_of_gt', CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
dsimp :
  X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ i.castSucc).op =
    X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ j.succ).op
⊢ X.σ j ≫ X.σ i.castSucc = X.σ i ≫ X.σ j.succ

Tactic:
dsimp [δ, σ]

Premises used: CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ i.castSucc).op =
    X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ j.succ).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.σ_comp_σ H]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, SimplexCategory.σ_comp_σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X' X : SimplicialObject.{v, u} C
f : X ⟶ X'
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ f.app (op ⦋n⦌) = f.app (op ⦋n + 1⦌) ≫ X'.δ i

Tactic:
f.naturality _

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X' X : SimplicialObject.{v, u} C
f : X ⟶ X'
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ f.app (op ⦋n + 1⦌) = f.app (op ⦋n⦌) ≫ X'.σ i

Tactic:
f.naturality _

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
⊢ ((obj (whiskering C D) F).obj X).δ i = F.map (X.δ i)

Tactic:
rfl

Premises used: CategoryTheory.SimplicialObject.δ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ ((obj (whiskering C D) F).obj X).σ i = F.map (X.σ i)

Tactic:
rfl

Premises used: rfl, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
rw :
  IsLeftKanExtension (obj (Truncated.sk n) (obj (truncation n) X))
    (NatTrans.app (SimplexCategory.Truncated.inclusion n).op.lanUnit (obj (truncation n) X))
⊢ IsLeftKanExtension (obj (Truncated.sk n) (obj (truncation n) X))
    (NatTrans.app (Adjunction.unit ((SimplexCategory.Truncated.inclusion n).op.lanAdjunction C)) (obj (truncation n) X))

Tactic:
rw [lanAdjunction_unit]

Premises used: CategoryTheory.Functor.lanAdjunction_unit
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension (obj (Truncated.sk n) (obj (truncation n) X))
    (NatTrans.app (SimplexCategory.Truncated.inclusion n).op.lanUnit (obj (truncation n) X))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
rw :
  IsRightKanExtension (obj (Truncated.cosk n) (obj (truncation n) X))
    (NatTrans.app (SimplexCategory.Truncated.inclusion n).op.ranCounit (obj (truncation n) X))
⊢ IsRightKanExtension (obj (Truncated.cosk n) (obj (truncation n) X))
    (NatTrans.app (Adjunction.counit ((SimplexCategory.Truncated.inclusion n).op.ranAdjunction C))
      (obj (truncation n) X))

Tactic:
rw [ranAdjunction_counit]

Premises used: CategoryTheory.Functor.ranAdjunction_counit
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsRightKanExtension (obj (Truncated.cosk n) (obj (truncation n) X))
    (NatTrans.app (SimplexCategory.Truncated.inclusion n).op.ranCounit (obj (truncation n) X))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst_3 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst_4 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ IsIso (C := Truncated.{v, u} C n ⥤ Truncated.{v, u} C n) (X := Truncated.cosk n ⋙ truncation n)
    (Adjunction.counit (coskAdj n))

Tactic:
reflective' (SimplexCategory.Truncated.inclusion n).op

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.reflective', SimplexCategory.Truncated.inclusion, CategoryTheory.SimplicialObject.truncation
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst_3 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst_4 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ IsIso (C := Truncated.{v, u} C n ⥤ Truncated.{v, u} C n) (Y := Truncated.sk n ⋙ truncation n)
    (Adjunction.unit (skAdj n))

Tactic:
coreflective' (SimplexCategory.Truncated.inclusion n).op

Premises used: CategoryTheory.Functor.op, SimplexCategory.Truncated.inclusion, CategoryTheory.Functor.coreflective', CategoryTheory.SimplicialObject.truncation
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst_3 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst_4 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ FullyFaithful (C := Truncated.{v, u} C n) (Truncated.cosk n)

Tactic:
apply Adjunction.fullyFaithfulROfIsIsoCounit (coskAdj n)

Premises used: CategoryTheory.SimplicialObject.coskAdj, CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst_3 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst_4 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ Full (C := Truncated.{v, u} C n) (Truncated.cosk n)

Tactic:
FullyFaithful.full (cosk.fullyFaithful _)

Premises used: CategoryTheory.SimplicialObject.Truncated.cosk.fullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst_3 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst_4 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ Faithful (C := Truncated.{v, u} C n) (Truncated.cosk n)

Tactic:
FullyFaithful.faithful (cosk.fullyFaithful _)

Premises used: CategoryTheory.SimplicialObject.Truncated.cosk.fullyFaithful, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst_3 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst_4 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ Full (C := Truncated.{v, u} C n) (Truncated.sk n)

Tactic:
FullyFaithful.full (sk.fullyFaithful _)

Premises used: CategoryTheory.SimplicialObject.Truncated.sk.fullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst_3 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst_4 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ Faithful (C := Truncated.{v, u} C n) (Truncated.sk n)

Tactic:
FullyFaithful.faithful (sk.fullyFaithful _)

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.SimplicialObject.Truncated.sk.fullyFaithful
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Augmented.{v, u} C
f g : X ⟶ Y
h₁ : f.left = g.left
h₂ : f.right = g.right
⊢ f = g

Tactic:
Comma.hom_ext _ _ h₁ h₂

Premises used: CategoryTheory.Comma.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Augmented.{v, u} C
f : X ⟶ Y
n : SimplexCategoryᵒᵖ
⊢ f.left.app n ≫ Y.hom.app n = X.hom.app n ≫ f.right

Tactic:
congr_app f.w n

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.congr_app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (𝟭 C)
        (Comma.left.{v, v, v, u, u, u} (T := C) (L := 𝟭 C) (R := 𝟭 C)
          { left := obj drop X_1 _⦋0⦌, right := obj point X_1, hom := X_1.hom.app (op ⦋0⦌) :
            Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }) ⟶
      obj.{v, v, u, u} (𝟭 C)
        (Comma.right.{v, v, v, u, u, u} (T := C) (L := 𝟭 C) (R := 𝟭 C)
          { left := obj drop Y _⦋0⦌, right := obj point Y, hom := Y.hom.app (op ⦋0⦌) :
            Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }))
    (map (𝟭 C) (NatTrans.app (map drop η) (op ⦋0⦌)) ≫
      Comma.hom { left := obj drop Y _⦋0⦌, right := obj point Y, hom := Y.hom.app (op ⦋0⦌) })
    (Comma.hom
        { left := obj drop X_1 _⦋0⦌, right := obj point X_1, hom := X_1.hom.app (op ⦋0⦌) :
          Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≫
      map (𝟭 C) (map point η))

Tactic:
simp [w_app]

Premises used: CategoryTheory.SimplicialObject.Augmented.w_app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Augmented.{v, u} C
f : X ⟶ Y
⊢ Eq (α := X.left _⦋0⦌ ⟶ Y.right) (f.left.app (op ⦋0⦌) ≫ Y.hom.app (op ⦋0⦌)) (X.hom.app (op ⦋0⦌) ≫ f.right)

Tactic:
congr_app f.w (op ⦋0⦌)

Premises used: CategoryTheory.CommaMorphism.w, SimplexCategory.mk, Opposite.op, OfNat.ofNat, CategoryTheory.congr_app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
h :
  ∀ (n : SimplexCategoryᵒᵖ),
    (map (𝟭 (SimplicialObject.{v_1, u_1} D)) (whiskerRight η.left F) ≫
            { left := (obj (whiskering C D) F).obj (obj drop Y), right := F.obj (obj point Y),
                hom := whiskerRight Y.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ Y.right F) :
                Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom).app
        n =
      ({ left := (obj (whiskering C D) F).obj (obj drop X_1), right := F.obj (obj point X_1),
                hom := whiskerRight X_1.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ X_1.right F) :
                Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom ≫
            map (const D) (F.map η.right)).app
        n
⊢ map (𝟭 (SimplicialObject.{v_1, u_1} D)) (whiskerRight η.left F) ≫
      { left := (obj (whiskering C D) F).obj (obj drop Y), right := F.obj (obj point Y),
          hom := whiskerRight Y.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ Y.right F) :
          Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom =
    { left := (obj (whiskering C D) F).obj (obj drop X_1), right := F.obj (obj point X_1),
          hom := whiskerRight X_1.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ X_1.right F) :
          Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom ≫
      map (const D) (F.map η.right)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
n : SimplexCategoryᵒᵖ
⊢ (map (𝟭 (SimplicialObject.{v_1, u_1} D)) (whiskerRight η.left F) ≫
          { left := (obj (whiskering C D) F).obj (obj drop Y), right := F.obj (obj point Y),
              hom := whiskerRight Y.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ Y.right F) :
              Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom).app
      n =
    ({ left := (obj (whiskering C D) F).obj (obj drop X_1), right := F.obj (obj point X_1),
              hom := whiskerRight X_1.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ X_1.right F) :
              Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom ≫
          map (const D) (F.map η.right)).app
      n

Tactic:
simp [← Functor.map_comp, w_app]

Premises used: CategoryTheory.SimplicialObject.Augmented.w_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
h :
  ∀ (n : SimplexCategoryᵒᵖ),
    (map (𝟭 (SimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η) ≫ ((whiskeringObj C D Y).obj A).hom).app n =
      (((whiskeringObj C D X_1).obj A).hom ≫ map (const D) (η.app (obj point A))).app n
⊢ map (𝟭 (SimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η) ≫ ((whiskeringObj C D Y).obj A).hom =
    ((whiskeringObj C D X_1).obj A).hom ≫ map (const D) (η.app (obj point A))

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
n : SimplexCategoryᵒᵖ
h :
  η.app (A.left.obj n) ≫ Y.map (A.hom.app n) ≫ 𝟙 (Y.obj A.right) =
    (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
⊢ (map (𝟭 (SimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η) ≫ ((whiskeringObj C D Y).obj A).hom).app n =
    (((whiskeringObj C D X_1).obj A).hom ≫ map (const D) (η.app (obj point A))).app n

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
n : SimplexCategoryᵒᵖ
h : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
h₁ : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = X_1.map (A.hom.app n) ≫ η.app A.right
h₂ h₃ : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = η.app (A.left.obj n) ≫ Y.map (A.hom.app n)
⊢ η.app (A.left.obj n) ≫ Y.map (A.hom.app n) ≫ 𝟙 (Y.obj A.right) =
    (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right

Tactic:
rw [Category.comp_id, Category.comp_id, η.naturality]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality