mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
⊢ Presheaf.IsLocallySurjective J f

Tactic:
by
  wlog hF₂ : ∃ (U : C), F₂ = shrinkYoneda.obj U generalizing F₁ F₂
  · refine ⟨fun {U} s ↦ ?_⟩
    let f' := pullback.snd f (shrinkYonedaEquiv.{w}.symm s)
    have hf' (Φ : P.FullSubcategory) :
        Function.Surjective (Φ.obj.presheafFiber.map f') := by
      replace hf := hf Φ
      rw [← CategoryTheory.epi_iff_surjective] at hf ⊢
      exact (MorphismProperty.epimorphisms _).of_isPullback
        ((IsPullback.of_hasPullback f (shrinkYonedaEquiv.{w}.symm s)).map
          Φ.obj.presheafFiber) (.infer_property _)
    have := this f' hf' ⟨_, rfl⟩
    refine J.superset_covering ?_
      (Presheaf.imageSieve_mem J f' (shrinkYonedaObjObjEquiv.symm (𝟙 U)))
    rintro V g ⟨v, hv⟩
    refine ⟨(pullback.fst f (shrinkYonedaEquiv.{w}.symm s)).app _ v, ?_⟩
    refine (ConcreteCategory.congr_hom (NatTrans.congr_app
      (pullback.condition (f := f)) (op V)) _).trans ?_
    dsimp at hv ⊢
    refine (congr_arg _ hv).trans ?_
    refine (congr_arg _ (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _))).trans ?_
    simpa using shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm s g
  obtain ⟨U, rfl⟩ := hF₂
  suffices Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U from ⟨by
    intro V g
    obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
    replace this := J.pullback_stable g this
    rw [Presheaf.pullback_imageSieve] at this
    have hg := shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _)
    simp only [Quiver.Hom.unop_op, Category.comp_id] at hg
    simpa [← hg]⟩
  refine hP _ (fun Φ u ↦ ?_)
  obtain ⟨x₁, hx₁⟩ := hf Φ (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app _ u)
  obtain ⟨V, v, y, rfl⟩ := Φ.obj.toPresheafFiber_jointly_surjective (A := Type w) x₁
  obtain ⟨t, ht⟩ := shrinkYonedaObjObjEquiv.symm.surjective (f.app _ y)
  refine ⟨V, t, ⟨y, ht.symm.trans ?_⟩, v, ?_⟩
  · simpa using (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm t.op (𝟙 _)).symm
  · refine (Φ.obj.shrinkYonedaCompPresheafFiberIso.symm.app U).toEquiv.injective ?_
    dsimp [-Functor.comp_obj]
    trans (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w}.obj U)) (shrinkYonedaObjObjEquiv.symm t)
    · rw [← Φ.obj.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app]
      exact Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality_apply t v
    · rw [← hx₁]
      refine Eq.trans (congr_arg _ ht)
        (Φ.obj.toPresheafFiber_naturality_apply f _ v y).symm

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
⊢ ∃ N, ∀ i ≥ N, padicNormE (lim f - ↑f i) < ε

Tactic:
obtain ⟨N2, hN2⟩ := padicNormE.defn (lim' f) (half_pos hε)

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (lim' f) - ↑(↑(lim' f) i)) < ε / 2
⊢ ∃ N, ∀ i ≥ N, padicNormE (lim f - ↑f i) < ε
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
pbIso : Limits.pullback ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
    ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
  F.obj (limit (pair a a)) :=
  pullback.congrHom ⋯ ⋯ ≪≫
    (prodIsoPullback (F.obj a) (F.obj a)).symm ≪≫
      (HasLimit.isoOfNatIso (pairComp a a F)).symm ≪≫ (preservesLimitIso F (pair a a)).symm
⊢ F.relativelyRepresentable ((pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫ pbIso.hom) ≫ pbIso.inv)

Tactic:
apply (respectsIso F).toRespectsRight.postcomp _ (inferInstance : IsIso _) _

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
pbIso : Limits.pullback ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
    ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
  F.obj (limit (pair a a)) := ⋯
⊢ F.relativelyRepresentable (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫ pbIso.hom)
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0

Tactic:
have eq := v ⟨a, by lia⟩ (by
        simp only [hnaq, add_assoc]
        rfl)

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ X.δ ⟨a, ⋯⟩.succ = 0
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q ≫ P q = P q

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q ≫ P q).f n = (P q).f n
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q q ≫ Q q = Q q

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (Q q ≫ Q q).f n = (Q q).f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z1‖ = ‖z2‖

Tactic:
by
  rw [eq_comm]
  apply norm_eq_of_norm_sub_lt_right
  simpa [← norm_neg (z1 - _)] using h

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ PInfty = PInfty

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (PInfty ≫ PInfty).f n = PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ QInfty ≫ QInfty = QInfty

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (QInfty ≫ QInfty).f n = QInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ QInfty = 0

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (PInfty ≫ QInfty).f n = HomologicalComplex.Hom.f 0 n
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ QInfty ≫ PInfty = 0

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (QInfty ≫ PInfty).f n = HomologicalComplex.Hom.f 0 n
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X✝ X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C).map f ≫ PInfty = PInfty ≫ (alternatingFaceMapComplex C).map f

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X✝ X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ ((alternatingFaceMapComplex C).map f ≫ PInfty).f n = (PInfty ≫ (alternatingFaceMapComplex C).map f).f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
⊢ ‖f.lim‖ ≤ a

Tactic:
obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ ha
  calc
    ‖f.lim‖ = ‖f.lim - f N + f N‖ := by simp
    _ ≤ max ‖f.lim - f N‖ ‖f N‖ := nonarchimedean _ _
    _ ≤ a := max_le (le_of_lt (hN _ le_rfl)) (hf _)

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (x * y).addValuationDef = x.addValuationDef + y.addValuationDef

Tactic:
by
  simp only [addValuationDef]
  by_cases hx : x = 0
  · rw [hx, if_pos rfl, zero_mul, if_pos rfl, WithTop.top_add]
  · by_cases hy : y = 0
    · rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]
    · rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
        valuation_mul hx hy]

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

Goal state before:
pp: case neg.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev = -(P q).f (n + 1) ≫ (Hσ q).f (n + 1)

Tactic:
have hnaq' : n = a + q := by lia

Goal state after:
case neg.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
hnaq' : n = a + q
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev = -(P q).f (n + 1) ≫ (Hσ q).f (n + 1)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
· by_cases hx : x = 0
    · rw [hx, if_pos rfl, min_eq_right, zero_add]
      exact le_top
    · by_cases hy : y = 0
      · rw [hy, if_pos rfl, min_eq_left, add_zero]
        exact le_top
      · rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]
        exact le_valuation_add hxy

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
have aux (n : ℤ) : 0 < ((p : ℝ) ^ n) := zpow_pos (mod_cast hp.1.pos) _
  by_cases hx0 : x = 0
  · simp [hx0, norm_zero, aux, le_of_lt (aux _)]
  rw [norm_eq_zpow_neg_valuation hx0]
  have h1p : 1 < (p : ℝ) := mod_cast hp.1.one_lt
  have H := zpow_right_strictMono₀ h1p
  rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Function.Injective fun A ↦ ⟨⟨(unop A.fst).len, ⋯⟩, ⇑(Hom.toOrderHom A.e)⟩

Tactic:
by
      rintro ⟨⟨Δ₁⟩, α₁⟩ ⟨⟨Δ₂⟩, α₂⟩ h₁
      simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁
      have h₂ : Δ₁ = Δ₂ := by
        ext1
        simpa only [Fin.mk_eq_mk] using h₁.1
      subst h₂
      refine ext _ _ rfl ?_
      ext : 2
      exact eq_of_heq h₁.2

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 : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ PInfty.f (n + 1) = 0

Tactic:
rw [PInfty_f, σ_comp_P_eq_zero X i]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ n + 1 ≤ ↑i + (n + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
⊢ x✝¹ = x✝

Tactic:
ext n

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ x✝¹.f n = x✝.f n
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)
⊢ ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p ≫
      { f := fun n ↦ P.p.f n, comm' := ⋯ } ≫ ((functor ⋙ inverse).obj P).p =
    { f := fun n ↦ P.p.f n, comm' := ⋯ }

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ (((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p ≫
          { f := fun n ↦ P.p.f n, comm' := ⋯ } ≫ ((functor ⋙ inverse).obj P).p).f
      n =
    { f := fun n ↦ P.p.f n, comm' := ⋯ }.f n
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)
⊢ ((functor ⋙ inverse).obj P).p ≫
      { f := fun n ↦ P.p.f n, comm' := ⋯ } ≫ ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p =
    { f := fun n ↦ P.p.f n, comm' := ⋯ }

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ (((functor ⋙ inverse).obj P).p ≫
          { f := fun n ↦ P.p.f n, comm' := ⋯ } ≫ ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p).f
      n =
    { f := fun n ↦ P.p.f n, comm' := ⋯ }.f n
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.app K =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫ (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)

Tactic:
ext
  simp [N₁Γ₀, Γ₀'CompNondegComplexFunctor]

Goal state after:
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✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
⊢ s.N (unop B.fst).len ⟶ s.N (unop A.fst).len

Tactic:
by_cases h : B = A
    · exact eqToHom (by subst h; rfl)
    · exact 0

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
⊢ (N₂Γ₂ToKaroubiIso.hom.app X).f = PInfty

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (N₂Γ₂ToKaroubiIso.hom.app X).f.f n = PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
⊢ (N₂Γ₂ToKaroubiIso.inv.app X).f = PInfty

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (N₂Γ₂ToKaroubiIso.inv.app X).f.f n = PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ : ∀ (i : ℕ), (inv (N₁.map f)).f.f i ≫ PInfty.f i ≫ f.app (op ⦋i⦌) = PInfty.f i
h₃ :
  ∀ (n : ℕ), PInfty.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) = (inv (N₁.map f)).f.f n ≫ PInfty.f n ≫ f.app (op ⦋n⦌)
h₁ : ∀ (i : ℕ), PInfty.f i ≫ f.app (op ⦋i⦌) ≫ (inv (N₁.map f)).f.f i = PInfty.f i
n : ℕ
⊢ IsIso (f.app (op ⦋n⦌))

Tactic:
induction n with

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

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

Tactic:
ext n

Goal state after:
case refine_1.refine_1.h_X
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).X =
    (((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                N₁ ⋙
                  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                    (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
            P).X
        n).X

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 ?refine_1.refine_1.h_X =
    eqToHom ?refine_1.refine_1.h_X ≫
      (((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).X
          n).p
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

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

Tactic:
ext n

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi (SimplicialObject C)
f : P ⟶ Q
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).map f).f n).f =
    ((eqToHom ⋯ ≫
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).map
                f ≫
              eqToHom ⋯).f
        n).f
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ F₂ ⋙ F₃ ⋙ F₄).map f)

Tactic:
rw [← compatibility_N₂_N₁_karoubi, Functor.comp_map]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso ((karoubiChainComplexEquivalence C ℕ).functor.map (N₂.map f))
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
X X' : V
hX : X = X'
⊢ Quiver.homOfEq (𝟙rq X) hX hX = 𝟙rq X'

Tactic:
subst hX

Goal state after:
V : Type u_1
inst✝ : ReflQuiver V
X : V
⊢ Quiver.homOfEq (𝟙rq X) ⋯ ⋯ = 𝟙rq X
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
⊢ ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex).p ≫
      { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ } ≫ (N₁.obj X).p =
    { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ (((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex).p ≫
          { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ } ≫ (N₁.obj X).p).f
      n =
    { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }.f n
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
⊢ (N₁.obj X).p ≫
      { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ } ≫
        ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex).p =
    { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ ((N₁.obj X).p ≫
          { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ } ≫
            ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex).p).f
      n =
    { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }.f n