awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
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), (inclusion n).op.HasRightKanExtension F
rw :
  IsRightKanExtension X (𝟙 ((inclusion n).op ⋙ X)) ↔
    IsIso (Y := obj (truncation n ⋙ Truncated.cosk n) X) (NatTrans.app (Adjunction.unit (coskAdj n)) X)
⊢ X.IsCoskeletal n ↔ IsIso (Y := obj (truncation n ⋙ Truncated.cosk n) X) (NatTrans.app (Adjunction.unit (coskAdj n)) X)

Tactic:
rw [isCoskeletal_iff]

Premises used: CategoryTheory.SimplicialObject.isCoskeletal_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
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), (inclusion n).op.HasRightKanExtension F
⊢ IsRightKanExtension X (𝟙 ((inclusion n).op ⋙ X)) ↔
    IsIso (Y := obj (truncation n ⋙ Truncated.cosk n) X) (NatTrans.app (Adjunction.unit (coskAdj n)) X)

Tactic:
isRightKanExtension_iff_isIso ((coskAdj n).unit.app X)
    ((coskAdj n).counit.app _) (𝟙 _) ((coskAdj n).left_triangle_components X)

Premises used: CategoryTheory.SimplicialObject.coskAdj, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.unit, CategoryTheory.CategoryStruct.id, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.isRightKanExtension_iff_isIso, CategoryTheory.NatTrans.app, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
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), (inclusion n).op.HasRightKanExtension F
⊢ IsRightKanExtension X (𝟙 ((inclusion n).op ⋙ X)) ↔
    IsIso (Y := obj (truncation n ⋙ Truncated.cosk n) X) (NatTrans.app (Adjunction.unit (coskAdj n)) X)

Tactic:
exact isRightKanExtension_iff_isIso ((coskAdj n).unit.app X)
    ((coskAdj n).counit.app _) (𝟙 _) ((coskAdj n).left_triangle_components X)

Premises used: CategoryTheory.SimplicialObject.coskAdj, CategoryTheory.Adjunction.unit, CategoryTheory.CategoryStruct.id, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.isRightKanExtension_iff_isIso, CategoryTheory.NatTrans.app, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
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), (inclusion n).op.HasRightKanExtension F
inst_2 rw : X.IsCoskeletal n
⊢ IsIso (Y := obj (truncation n ⋙ Truncated.cosk n) X) (NatTrans.app (Adjunction.unit (coskAdj n)) X)

Tactic:
rw [← isCoskeletal_iff_isIso]

Premises used: CategoryTheory.SimplicialObject.isCoskeletal_iff_isIso
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
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), (inclusion n).op.HasRightKanExtension F
inst_2 : X.IsCoskeletal n
⊢ X.IsCoskeletal n

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
⊢ Y.σ 0 ≫ Y.δ (Fin.castSucc 0) = 𝟙 (Y _⦋n⦌)

Tactic:
have := Y.δ_comp_σ_self (n := n) (i := 0)
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
this : Y.σ 0 ≫ Y.δ 0 = 𝟙 (Y _⦋n⦌)
⊢ Eq (α := X _⦋n⦌ ⟶ Y _⦋n⦌) ((X.σ 0 ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ 0) (f.app (op ⦋n⦌))

Tactic:
simp only [SimplicialObject.σ_naturality, Category.assoc, this, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.σ_naturality, CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
⊢ Y.σ (Fin.last n) ≫ Y.δ (Fin.last n).succ = 𝟙 (Y _⦋n⦌)

Tactic:
have := Y.δ_comp_σ_succ (i := Fin.last n)
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
this : Y.σ (Fin.last n) ≫ Y.δ (Fin.last (n + 1)) = 𝟙 (Y _⦋n⦌)
⊢ (X.σ (Fin.last n) ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ (Fin.last (n + 1)) = f.app (op ⦋n⦌)

Tactic:
simp only [SimplicialObject.σ_naturality, Category.assoc, this, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.σ_naturality, CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
⊢ (X.σ j.succ ≫ f.app (op ⦋n + 1 + 1⦌)) ≫ Y.δ i.castSucc = X.δ i ≫ X.σ j ≫ f.app (op ⦋n + 1⦌)

Tactic:
simp [Y.δ_comp_σ_of_le hij]

Premises used: CategoryTheory.SimplicialObject.δ_comp_σ_of_le
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
j : Fin (n + 1)
⊢ Y.σ j.succ ≫ Y.δ j.succ.castSucc = 𝟙 (Y _⦋n + 1⦌)

Tactic:
have h₁ := Y.δ_comp_σ_self (i := j.succ)
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
j : Fin (n + 1)
h₁ : Y.σ j.succ ≫ Y.δ j.succ.castSucc = 𝟙 (Y _⦋n + 1⦌)
⊢ Y.σ j.castSucc ≫ Y.δ j.castSucc.succ = 𝟙 (Y _⦋n + 1⦌)

Tactic:
have h₂ := Y.δ_comp_σ_succ (i := j.castSucc)
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
j : Fin (n + 1)
h₁ : Y.σ j.succ ≫ Y.δ j.castSucc.succ = 𝟙 (Y _⦋n + 1⦌)
h₂ : Y.σ j.castSucc ≫ Y.δ j.castSucc.succ = 𝟙 (Y _⦋n + 1⦌)
⊢ (X.σ j.succ ≫ f.app (op ⦋n + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ =
    (X.σ j.castSucc ≫ f.app (op ⦋n + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ

Tactic:
simp only [SimplicialObject.σ_naturality, Category.assoc, h₁, Category.comp_id, h₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.σ_naturality, CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hji : j.castSucc < i
⊢ (X.σ j.castSucc ≫ f.app (op ⦋n + 1 + 1⦌)) ≫ Y.δ i.succ = X.δ i ≫ X.σ j ≫ f.app (op ⦋n + 1⦌)

Tactic:
simp [Y.δ_comp_σ_of_gt hji]

Premises used: CategoryTheory.SimplicialObject.δ_comp_σ_of_gt
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ (X.σ j ≫ f.app (op ⦋n + 1⦌)) ≫ Y.σ i.castSucc = X.σ i ≫ X.σ j.succ ≫ f.app (op ⦋n + 1 + 1⦌)

Tactic:
simp [Y.σ_comp_σ hij]

Premises used: CategoryTheory.SimplicialObject.σ_comp_σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
i j : Fin (n + 1)
hji : j ≤ i
⊢ (X.σ j ≫ f.app (op ⦋n + 1⦌)) ≫ Y.σ i.succ = X.σ i ≫ X.σ j.castSucc ≫ f.app (op ⦋n + 1 + 1⦌)

Tactic:
simp [Y.σ_comp_σ hji]

Premises used: CategoryTheory.SimplicialObject.σ_comp_σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
n : ℕ
⊢ Eq (α := (Functor.obj (whiskering C D) F).obj X _⦋n⦌ ⟶ (Functor.obj (whiskering C D) F).obj Y _⦋n⦌)
    (F.map (H.h 0) ≫ ((Functor.obj (whiskering C D) F).obj Y).δ 0)
    (((Functor.obj (whiskering C D) F).map g).app (op ⦋n⦌))

Tactic:
simpa [SimplicialObject.δ] using
      congrArg (fun k => F.map k) (H.h_zero_comp_δ_zero n)

Premises used: congrArg, CategoryTheory.Functor.map, CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.Homotopy.h_zero_comp_δ_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
n : ℕ
⊢ F.map (H.h (Fin.last n)) ≫ ((Functor.obj (whiskering C D) F).obj Y).δ (Fin.last (n + 1)) =
    ((Functor.obj (whiskering C D) F).map f).app (op ⦋n⦌)

Tactic:
simpa [SimplicialObject.δ] using
      congrArg (fun k => F.map k) (H.h_last_comp_δ_last n)

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_last_comp_δ_last, congrArg, CategoryTheory.Functor.map, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
⊢ F.map (H.h j.succ) ≫ ((Functor.obj (whiskering C D) F).obj Y).δ i.castSucc =
    ((Functor.obj (whiskering C D) F).obj X).δ i ≫ F.map (H.h j)

Tactic:
simpa [SimplicialObject.δ] using
      congrArg (fun k => F.map k) (H.h_succ_comp_δ_castSucc_of_lt i j hij)

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_of_lt, congrArg, CategoryTheory.Functor.map, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
n : ℕ
j : Fin (n + 1)
⊢ F.map (H.h j.succ) ≫ ((Functor.obj (whiskering C D) F).obj Y).δ j.castSucc.succ =
    F.map (H.h j.castSucc) ≫ ((Functor.obj (whiskering C D) F).obj Y).δ j.castSucc.succ

Tactic:
simpa [SimplicialObject.δ] using
      congrArg (fun k => F.map k) (H.h_succ_comp_δ_castSucc_succ j)

Premises used: congrArg, CategoryTheory.Functor.map, CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hji : j.castSucc < i
⊢ F.map (H.h j.castSucc) ≫ ((Functor.obj (whiskering C D) F).obj Y).δ i.succ =
    ((Functor.obj (whiskering C D) F).obj X).δ i ≫ F.map (H.h j)

Tactic:
simpa [SimplicialObject.δ] using
      congrArg (fun k => F.map k) (H.h_castSucc_comp_δ_succ_of_lt i j hji)

Premises used: congrArg, CategoryTheory.Functor.map, CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.Homotopy.h_castSucc_comp_δ_succ_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ F.map (H.h j) ≫ ((Functor.obj (whiskering C D) F).obj Y).σ i.castSucc =
    ((Functor.obj (whiskering C D) F).obj X).σ i ≫ F.map (H.h j.succ)

Tactic:
simpa [SimplicialObject.σ] using
      congrArg (fun k => F.map k) (H.h_comp_σ_castSucc_of_le i j hij)

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_castSucc_of_le, congrArg, CategoryTheory.Functor.map, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
n : ℕ
i j : Fin (n + 1)
hji : j ≤ i
⊢ F.map (H.h j) ≫ ((Functor.obj (whiskering C D) F).obj Y).σ i.succ =
    ((Functor.obj (whiskering C D) F).obj X).σ i ≫ F.map (H.h j.castSucc)

Tactic:
simpa [SimplicialObject.σ] using
      congrArg (fun k => F.map k) (H.h_comp_σ_succ_of_lt i j hji)

Premises used: congrArg, CategoryTheory.Functor.map, CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_succ_of_lt, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject.{v, u} C
p : Y ⟶ Y'
n : ℕ
⊢ Eq (α := X _⦋n⦌ ⟶ Y' _⦋n⦌) ((H.h 0 ≫ p.app (op ⦋n + 1⦌)) ≫ Y'.δ 0) ((g ≫ p).app (op ⦋n⦌))

Tactic:
simpa [-h_zero_comp_δ_zero] using H.h_zero_comp_δ_zero n =≫ p.app _

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_zero_comp_δ_zero, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject.{v, u} C
p : Y ⟶ Y'
n : ℕ
⊢ (H.h (Fin.last n) ≫ p.app (op ⦋n + 1⦌)) ≫ Y'.δ (Fin.last (n + 1)) = (f ≫ p).app (op ⦋n⦌)

Tactic:
simpa [-h_last_comp_δ_last] using H.h_last_comp_δ_last n =≫ p.app _

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_last_comp_δ_last, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject.{v, u} C
p : Y ⟶ Y'
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
⊢ (H.h j.succ ≫ p.app (op ⦋n + 1 + 1⦌)) ≫ Y'.δ i.castSucc = X.δ i ≫ H.h j ≫ p.app (op ⦋n + 1⦌)

Tactic:
simpa using H.h_succ_comp_δ_castSucc_of_lt i j hij =≫ p.app _

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_of_lt, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject.{v, u} C
p : Y ⟶ Y'
n : ℕ
j : Fin (n + 1)
⊢ (H.h j.succ ≫ p.app (op ⦋n + 1 + 1⦌)) ≫ Y'.δ j.castSucc.succ =
    (H.h j.castSucc ≫ p.app (op ⦋n + 1 + 1⦌)) ≫ Y'.δ j.castSucc.succ

Tactic:
simpa using H.h_succ_comp_δ_castSucc_succ j =≫ p.app _

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_succ, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject.{v, u} C
p : Y ⟶ Y'
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hji : j.castSucc < i
⊢ (H.h j.castSucc ≫ p.app (op ⦋n + 1 + 1⦌)) ≫ Y'.δ i.succ = X.δ i ≫ H.h j ≫ p.app (op ⦋n + 1⦌)

Tactic:
simpa using H.h_castSucc_comp_δ_succ_of_lt i j hji =≫ p.app _

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_castSucc_comp_δ_succ_of_lt, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject.{v, u} C
p : Y ⟶ Y'
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ (H.h j ≫ p.app (op ⦋n + 1⦌)) ≫ Y'.σ i.castSucc = X.σ i ≫ H.h j.succ ≫ p.app (op ⦋n + 1 + 1⦌)

Tactic:
simpa using H.h_comp_σ_castSucc_of_le i j hij =≫ p.app _

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_castSucc_of_le, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject.{v, u} C
p : Y ⟶ Y'
n : ℕ
i j : Fin (n + 1)
hji : j ≤ i
⊢ (H.h j ≫ p.app (op ⦋n + 1⦌)) ≫ Y'.σ i.succ = X.σ i ≫ H.h j.castSucc ≫ p.app (op ⦋n + 1 + 1⦌)

Tactic:
simpa using H.h_comp_σ_succ_of_lt i j hji =≫ p.app _

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_succ_of_lt, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject.{v, u} C
p : X' ⟶ X
n : ℕ
⊢ Eq (α := X' _⦋n⦌ ⟶ Y _⦋n⦌) ((p.app (op ⦋n⦌) ≫ H.h 0) ≫ Y.δ 0) ((p ≫ g).app (op ⦋n⦌))

Tactic:
simpa [-h_zero_comp_δ_zero] using p.app _ ≫= H.h_zero_comp_δ_zero n

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_zero_comp_δ_zero, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject.{v, u} C
p : X' ⟶ X
n : ℕ
⊢ (p.app (op ⦋n⦌) ≫ H.h (Fin.last n)) ≫ Y.δ (Fin.last (n + 1)) = (p ≫ f).app (op ⦋n⦌)

Tactic:
simpa [-h_last_comp_δ_last] using p.app _ ≫= H.h_last_comp_δ_last n

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_last_comp_δ_last, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject.{v, u} C
p : X' ⟶ X
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
⊢ (p.app (op ⦋n + 1⦌) ≫ H.h j.succ) ≫ Y.δ i.castSucc = X'.δ i ≫ p.app (op ⦋n⦌) ≫ H.h j

Tactic:
simpa using p.app _ ≫= H.h_succ_comp_δ_castSucc_of_lt i j hij

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_of_lt, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject.{v, u} C
p : X' ⟶ X
n : ℕ
j : Fin (n + 1)
⊢ (p.app (op ⦋n + 1⦌) ≫ H.h j.succ) ≫ Y.δ j.castSucc.succ = (p.app (op ⦋n + 1⦌) ≫ H.h j.castSucc) ≫ Y.δ j.castSucc.succ

Tactic:
simpa using p.app _ ≫= H.h_succ_comp_δ_castSucc_succ j

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_succ, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject.{v, u} C
p : X' ⟶ X
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hji : j.castSucc < i
⊢ (p.app (op ⦋n + 1⦌) ≫ H.h j.castSucc) ≫ Y.δ i.succ = X'.δ i ≫ p.app (op ⦋n⦌) ≫ H.h j

Tactic:
simpa using p.app _ ≫= H.h_castSucc_comp_δ_succ_of_lt i j hji

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_castSucc_comp_δ_succ_of_lt, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject.{v, u} C
p : X' ⟶ X
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ (p.app (op ⦋n⦌) ≫ H.h j) ≫ Y.σ i.castSucc = X'.σ i ≫ p.app (op ⦋n + 1⦌) ≫ H.h j.succ

Tactic:
simpa using p.app _ ≫= H.h_comp_σ_castSucc_of_le i j hij

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_castSucc_of_le, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject.{v, u} C
p : X' ⟶ X
n : ℕ
i j : Fin (n + 1)
hji : j ≤ i
⊢ (p.app (op ⦋n⦌) ≫ H.h j) ≫ Y.σ i.succ = X'.σ i ≫ p.app (op ⦋n + 1⦌) ≫ H.h j.castSucc

Tactic:
simpa using p.app _ ≫= H.h_comp_σ_succ_of_lt i j hji

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_succ_of_lt, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
i : Fin (n + 2)
⊢ i ∈ finset f x ↔
    i = Fin.last (n + 1) ∨
      ∃ (h : i ≠ Fin.last (n + 1)), x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) (i.castPred h))

Tactic:
simp [finset]

Premises used: SimplexCategory.II.finset
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ Fin.last (n + 1) ∈ finset f x

Tactic:
simp [mem_finset_iff]

Premises used: SimplexCategory.II.mem_finset_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
i : Fin (n + 1)
⊢ i.castSucc ∈ finset f x ↔ x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)

Tactic:
simp [mem_finset_iff, Fin.castPred_castSucc]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, SimplexCategory.II.mem_finset_iff, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
simp :
  (∀ b ∈ finset f x, b = Fin.last (n + 1)) ↔
    ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
⊢ map' f x = Fin.last (n + 1) ↔ ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x

Tactic:
simp only [map', Finset.min'_eq_iff, last_mem_finset, Fin.last_le_iff, true_and]

Premises used: SimplexCategory.II.map', SimplexCategory.II.last_mem_finset, Finset.min'_eq_iff, Fin.last_le_iff, true_and
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
mp :
  (∀ b ∈ finset f x, b = Fin.last (n + 1)) →
    ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
mpr :
  (∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x) →
    ∀ b ∈ finset f x, b = Fin.last (n + 1)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) ↔
    ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
i : Fin (n + 1)
mp : ∀ (this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)), False
⊢ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x

Tactic:
by_contra!
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
i : Fin (n + 1)
this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)
⊢ i.castSucc ∈ finset f x

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
i : Fin (n + 1)
this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)
⊢ False

Tactic:
exact i.castSucc_ne_last (h i.castSucc (by simpa))

Premises used: Fin.castSucc_ne_last, Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 2)
hi : i ∈ finset f x
mpr : ∀ (this : i ≠ Fin.last (n + 1)), False
⊢ i = Fin.last (n + 1)

Tactic:
by_contra!
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 2)
hi : i ∈ finset f x
this : i ≠ Fin.last (n + 1)
mpr : ∀ (i : Fin (n + 1)) (hi : i.castSucc ∈ finset f x) (this : i.castSucc ≠ Fin.last (n + 1)), False
⊢ False

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last this

Premises used: Fin.eq_castSucc_of_ne_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
this : i.castSucc ≠ Fin.last (n + 1)
⊢ x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)

Tactic:
simp only [castSucc_mem_finset_iff] at hi

Premises used: SimplexCategory.II.castSucc_mem_finset_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 1)
this : i.castSucc ≠ Fin.last (n + 1)
hi : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)
⊢ False

Tactic:
hi.not_gt (h i)

Premises used: LE.le.not_gt