mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      (PInfty.f n ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      (PInfty.f n ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ x⁻¹.valuation = -x.valuation

Tactic:
have h_norm : ‖x⁻¹‖ = ‖x‖⁻¹ := norm_inv x

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
⊢ x⁻¹.valuation = -x.valuation
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq : Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f = (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌)
⊢ Y.p.app (op ⦋n⦌) ≫ Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f

Tactic:
app_idem_assoc Y (op ⦋n⦌)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq : Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f = (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌)
⊢ Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ j ≠ 0

pp: case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ⟨b, ⋯⟩.succ < j.succ

Tactic:
· intro hj'
    simp only [hnbq, add_comm b, add_assoc, hj', Fin.val_zero, zero_add, add_le_iff_nonpos_right,
      nonpos_iff_eq_zero, add_eq_zero, false_and, reduceCtorEq] at hj

Goal state after:
case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ⟨b, ⋯⟩.succ < j.succ
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ 𝟙 (X _⦋1⦌) +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (∑ i, (-1) ^ ↑i • X.δ i) ≫ (1 • X.σ 0) +
        X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (-1 • X.σ 1) ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0

Tactic:
comp_id,

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (∑ i, (-1) ^ ↑i • X.δ i) ≫ (1 • X.σ 0) +
        X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (-1 • X.σ 1) ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 + (X.σ 0 + -X.σ 0 ≫ X.δ 1 ≫ X.σ 0 + (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 + (X.σ 0 ≫ 𝟙 (X _⦋1⦌) + -X.σ 0 ≫ 𝟙 (X _⦋1⦌)))) = 0

Tactic:
comp_id,

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 + (X.σ 0 + -X.σ 0 ≫ X.δ 1 ≫ X.σ 0 + (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 + (X.σ 0 + -X.σ 0))) = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
by
  by_cases hx : x = 0
  · simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl]
  · rw [norm_eq_zpow_neg_valuation hx, ← zpow_zero (p : ℝ), zpow_le_zpow_iff_right₀, neg_nonpos]
    exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ ((P q).f n.succ ≫ X.σ i) ≫ 𝟙 (X _⦋n + 1 + 1⦌) + ((P q).f n.succ ≫ X.σ i) ≫ (Hσ q).f (n + 1 + 1) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Tactic:
comp_id,

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ (P q).f n.succ ≫ X.σ i + ((P q).f n.succ ≫ X.σ i) ≫ (Hσ q).f (n + 1 + 1) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
⊢ f = g

Tactic:
by
  ext ⟨Δ⟩
  apply s.hom_ext'
  intro A
  induction Δ using SimplexCategory.rec with | _ n
  dsimp
  simp only [s.cofan_inj_comp_app, h]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q
⊢ X.σ i ≫ (P q).f (n + 1) = 0

Tactic:
induction q generalizing i with
  | zero => lia
  | succ q hq =>
    by_cases h : n + 1 ≤ (i : ℕ) + q
    · rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
    · replace hi : n = i + q := by lia
      rcases n with _ | n
      · fin_cases i
        dsimp at h hi
        rw [show q = 0 by lia]
        change X.σ 0 ≫ (P 1).f 1 = 0
        simp only [P_succ, HomologicalComplex.add_f_apply, comp_add,
          AlternatingFaceMapComplex.obj_d_eq, Hσ,
          HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl),
          comp_id]
        rw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm]
        dsimp [P_zero]
        rw [comp_id, Fin.sum_univ_two,
          Fin.sum_univ_succ, Fin.sum_univ_two]
        simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.val_succ,
          Fin.val_one, mul_neg, one_mul, neg_mul, neg_neg, id_comp, add_comp, comp_add, neg_comp,
          comp_neg, Fin.succ_zero_eq_one]
        rw [← Fin.castSucc_one, SimplicialObject.δ_comp_σ_self, ← Fin.castSucc_zero (n := 1),
          SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ, comp_id, ← Fin.castSucc_zero (n := 2),
          ← Fin.succ_zero_eq_one,
          SimplicialObject.δ_comp_σ_of_le X
            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
          ← Fin.castSucc_zero (n := 1), SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ_assoc]
        simp only [add_neg_cancel, add_zero, zero_add]
      · rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
          P_succ]
        have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) :=
          (HigherFacesVanish.of_P q n).comp_σ hi
        dsimp only [AlternatingFaceMapComplex.obj_X, Nat.succ_eq_add_one, HomologicalComplex.comp_f,
          HomologicalComplex.add_f_apply, HomologicalComplex.id_f]
        rw [← assoc, v.comp_P_eq_self, Preadditive.comp_add,
          comp_id, v.comp_Hσ_eq hi, assoc, ← Fin.succ_mk _ _ i.2,
          SimplicialObject.δ_comp_σ_succ_assoc,
          Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
          add_neg_eq_zero]
        intro j hj
        simp only [Finset.mem_univ, Finset.mem_filter] at hj
        obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
        rw [add_comm] at hk
        have hi' : i = Fin.castSucc ⟨i, by lia⟩ := by
          ext
          simp only [Fin.castSucc_mk, Fin.eta]
        have eq := hq j.rev.succ (by
          simp only [← hk, Fin.rev_eq j hk.symm, Fin.succ_mk, Fin.val_mk]
          lia)
        rw [assoc, assoc, assoc, hi',
          SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp, comp_zero, comp_zero,
          comp_zero]
        simp only [Fin.rev_eq j hk.symm, Fin.le_iff_val_le_val]
        lia

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e ≫ 𝟙 (unop A.fst) = 𝟙 (unop Δ) ≫ A.e

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e = 𝟙 (unop Δ) ≫ A.e
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
hij : ¬c.Rel i j
⊢ { f := P.p.f i ≫ P.X.d i j, comm := ⋯ } = 0

Tactic:
simp only [hom_eq_zero_iff]; cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A ≫
      𝟙 (colimit (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) =
    Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K A.e.op

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A =
    Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K A.e.op
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ i = (A.e.op ≫ θ).unop ≫ 𝟙 (unop (op (unop A.fst)))

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ i = (A.e.op ≫ θ).unop
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A, s.πSummand A ≫ (s.cofan Δ).inj A

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A = (s.cofan Δ).inj A ≫ ∑ A, s.πSummand A ≫ (s.cofan Δ).inj A
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: case e'_2.e'_7
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌))

Tactic:
comp_id,

Goal state after:
case e'_2.e'_7
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A = ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ (PInfty.f (n + 1) + QInfty.f (n + 1)) = f ≫ 𝟙 (X _⦋n + 1⦌)
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
comp_id,

Goal state after:
case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ (PInfty.f (n + 1) + QInfty.f (n + 1)) = f
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ α.inv ≫ 𝟙 (N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P)) = β.hom

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ α.inv = β.hom
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: case h_p
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).X n).p ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫
      (((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).X
          n).p

Tactic:
dsimp
        simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫ (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X = Γ₂N₂ToKaroubiIso.inv.app X ≫ Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f j ≫ 𝟙 (S₂.s.N j) =
    (S₁.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
comp_id,

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f j =
    (S₁.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P)))) ≫
      𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) =
    𝟙 (N₂.obj P)

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ N₂Γ₂.inv.app (N₂.obj P) ≫
      𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) =
    𝟙 (N₂.obj P)
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ 𝟭 (SingleObj M) = (e.symm.toMonoidHom.comp e.toMonoidHom).toFunctor

Tactic:
← MonoidHom.id_toFunctor

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ (MonoidHom.id M).toFunctor = (e.symm.toMonoidHom.comp e.toMonoidHom).toFunctor
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ (e.toMonoidHom.comp e.symm.toMonoidHom).toFunctor = 𝟭 (SingleObj N)

Tactic:
← MonoidHom.id_toFunctor

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ (e.toMonoidHom.comp e.symm.toMonoidHom).toFunctor = (MonoidHom.id N).toFunctor
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : ↑I
ht : t ∈ {0, 1}
⊢ {
        toFun := fun x_1 ↦
          if ↑(x, x_1).2 ≤ 1 / 2 then (F.eval (x, x_1).1).extend (2 * ↑(x, x_1).2)
          else (G.eval (x, x_1).1).extend (2 * ↑(x, x_1).2 - 1),
        continuous_toFun := ⋯ }
      t =
    (p₀.trans p₁).toContinuousMap t

Tactic:
by
    rcases ht with ht | ht
    · norm_num [ht]
    · rw [Set.mem_singleton_iff] at ht
      norm_num [ht]

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
by
  /- Let `G` be the continuous map on the unit square sending `(t, s)` to `F(t, p(s))`.
  Then our homotopy is the image under `G` of a homotopy
  between the two paths from `(0, 0)` to `(1, 1)` along the sides of the square. -/
  set G : C(I × I, Y) := F.toContinuousMap.comp (.prodMap (.id _) p)
  set p₁ : Path ((0, 0) : I × I) (1, 1) := .prod (.trans (.refl _) .id) (.trans .id (.refl _))
  set p₂ : Path ((0, 0) : I × I) (1, 1) := .prod (.trans .id (.refl _)) (.trans (.refl _) .id)
  set Fsq : p₁.Homotopy p₂ :=
    Path.Homotopic.prodHomotopy (.trans (.reflTrans _) (.symm <| .transRefl _))
      (.trans (.transRefl _) (.symm <| .reflTrans _))
  refine ⟨((Fsq.map G).pathCast ?H0 ?H1).cast ?hp ?hq⟩
  all_goals aesop (add simp Path.trans_apply)

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ ∀ (t : ↑I), ((fun q ↦ q.map ⋯) p) t = ((fun q ↦ q.map ⋯) q) t

Tactic:
exact hfg

Goal state after: