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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ n + 1 = 0 + q

Tactic:
lia

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

Goal state before:
pp: 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 : n < q
⊢ n + 1 ≤ q

Tactic:
lia

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

Goal state before:
pp: case pos.e_s
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 : n < q
x : ℕ
hx : x < n + 1
⊢ x < q ↔ x < q + 1

Tactic:
lia

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

Goal state before:
pp: case neg
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
⊢ (Q (q + 1)).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
obtain ⟨a, ha⟩ := Nat.le.dest hqn

Goal state after:
case neg
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 (q + 1)).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.h.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ ↑j + 1 + q

Tactic:
lia

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if 0 * y = 0 then ⊤ else ↑(0 * y).valuation) = ⊤ + if y = 0 then ⊤ else ↑y.valuation

Tactic:
zero_mul,

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if 0 = 0 then ⊤ else ↑(valuation 0)) = ⊤ + if y = 0 then ⊤ else ↑y.valuation
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

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

Tactic:
lia

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

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : q ≤ n
⊢ φ ≫ X.δ j.succ + (φ ≫ (Hσ q).f (n + 1)) ≫ X.δ j.succ = 0

Tactic:
obtain ⟨a, ha⟩ := Nat.le.dest hqn

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ + (φ ≫ (Hσ q).f (n + 1)) ≫ X.δ j.succ = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

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

Tactic:
lia

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

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

Tactic:
lia

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

Goal state before:
pp: 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, ⋯⟩
⊢ n = a + q

Tactic:
lia

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 : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + (q + 1)
h : ¬n + 1 ≤ ↑i + q
⊢ n = ↑i + q

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
⊢ a ≤ ↑j

Tactic:
lia

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
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
⊢ q = 0

Tactic:
lia

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

Goal state before:
pp: case neg.e_a.e_s
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, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ¬i = q ∧ i < q + 1 ↔ i < q

Tactic:
lia

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

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

Tactic:
by_cases hx0 : x = 0

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.inl.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ a + 1 ≤ ↑j

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ m + 1 + 1 ≤ ↑j + q

Tactic:
lia

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

Goal state before:
pp: case neg.inr.H.mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
hqn : q ≤ m + 1
ha : q + a = m + 1
ham : a ≤ m
ham'' : a = m
val✝ : ℕ
isLt✝ : val✝ < m + 1 + 1
hj₁ : m + 1 + 1 ≤ val✝ + (q + 1)
hj₂ : ¬a = val✝
haj : a < val✝
⊢ a + 1 = val✝

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
ham'' : a = m
⊢ m + 1 + 1 ≤ ↑j + q

Tactic:
lia

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

Goal state before:
pp: j : ℕ
⊢ ¬(Hom.toOrderHom (SimplexCategory.δ 0)) 0 = 0

Tactic:
exact Fin.succ_ne_zero (0 : Fin (j + 1))

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
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)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ ↑i < n + 1

Tactic:
lia

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
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)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = ⟨↑i, ⋯⟩.castSucc
⊢ k + ↑j + 1 + 1 ≤ k + 1 + q

Tactic:
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 : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
⊢ Δ.len = Δ''.len + (k + k' + 2)

Tactic:
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 : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
h : Isδ₀ (i' ≫ i)
eq : 1 = k + k' + 2
⊢ False

Tactic:
lia

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

Goal state before:
pp: case neg.succ.H
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)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = ⟨↑i, ⋯⟩.castSucc
eq : X.σ j.rev.succ ≫ (P q).f (n + 1 + 1) = 0
⊢ ↑i ≤ k

Tactic:
lia

Goal state after:
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
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ (kernelSubobject (X.δ j.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ j.succ)).arrow ≫ X.δ j.succ =
    0

Tactic:
kernelSubobject_arrow_comp,

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ (kernelSubobject (X.δ j.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫ 0 = 0
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 : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ (-1) ^ ↑i •
      Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ i) ≫
        ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
          (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌)) =
    0

Tactic:
Γ₀.Obj.Termwise.mapMono_eq_zero,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ (-1) ^ ↑i •
      0 ≫
        ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
          (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌)) =
    0

case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ⦋n + 1⦌ ≠ ⦋n⦌

case h₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ i)
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : n + 1 = n
⊢ False

Tactic:
lia

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

Goal state before:
pp: case e_a
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⦌)
⊢ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A ↦ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Tactic:
Splitting.ι_desc_assoc,

Goal state after:
case e_a
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) ≫ PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ 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
⊢ (toKaroubi (ChainComplex C ℕ)).whiskerLeft N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom

Tactic:
by
  let e : _ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 _ := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
  have h := ((whiskeringLeft _ _ (Karoubi (ChainComplex C ℕ))).obj
    (toKaroubi (ChainComplex C ℕ))).map_preimage e.hom
  dsimp only [whiskeringLeft, N₂Γ₂, Functor.preimageIso] at h ⊢
  exact h

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

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : (unop A.fst).len ≤ n
⊢ ¬(unop A.fst).len = n + 1

Tactic:
lia

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

Goal state before:
pp: case h
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 : ℕ
hn : IsIso (f.app (op ⦋n⦌))
⊢ f.app (op ⦋n + 1⦌) ≫
        { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1), b := fun i ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i }.φ =
      𝟙 (X _⦋n + 1⦌) ∧
    { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1), b := fun i ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i }.φ ≫
        f.app (op ⦋n + 1⦌) =
      𝟙 (Y _⦋n + 1⦌)

Tactic:
simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
        SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]

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
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ ↑j
⊢ m + 2 ≤ ↑j + (m + 1)

Tactic:
lia

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

Goal state before:
pp: case pos.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ m + k + 1 + 2 ≤ ↑j₂ + 1 + (m + k + 1 + 1)

Tactic:
lia

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
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
this : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ ↑j₁ = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.Basic

Goal state before:
pp: X Y Z : TopCat
f₀ f₁ : X ⟶ Y
g₀ g₁ : Y ⟶ Z
G : Homotopy g₀ g₁
F : Homotopy f₀ f₁
⊢ (G.comp F).h = X ◁ lift (𝟙 I) (𝟙 I) ≫ (α_ X I I).inv ≫ F.h ▷ I ≫ G.h

Tactic:
ext
  simp

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
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      ((Γ₀.splitting (N₂.obj P).X).desc (op ⦋n⦌) fun A ↦
          (PInfty.f (unop A.fst).len ≫ P.p.app A.fst) ≫
            ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).cofan (op ⦋n⦌)).inj A) ≫
        (Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app P.X)).f.app (op ⦋n⦌) ≫
          ((Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫ P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)

Tactic:
Splitting.ι_desc_assoc,

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 : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ((PInfty.f (unop (Splitting.IndexSet.id (op ⦋n⦌)).fst).len ≫ P.p.app (Splitting.IndexSet.id (op ⦋n⦌)).fst) ≫
        ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).cofan (op ⦋n⦌)).inj
          (Splitting.IndexSet.id (op ⦋n⦌))) ≫
      (Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app P.X)).f.app (op ⦋n⦌) ≫
        ((Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫ P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.symm.symm = F

Tactic:
ext
  simp

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

Goal state before:
pp: A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    (match X, X, 𝟙 X with
      | (fst, snd), (fst_1, snd_1), (p₀, p₁) => Path.Homotopic.prod p₀ p₁) =
      𝟙 { as := (X.1.as, X.2.as) }

Tactic:
rintro ⟨x₀, x₁⟩
    simp only
    rfl

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

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝ = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝

Tactic:
ext <;> simp

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projLeft A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.1

case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projRight A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.2
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
⊢ p.Homotopic (Path.refl x)

Tactic:
· rcases h x (p.map continuous_subtype_val) (fun t ↦ (p t).2) with ⟨F, hF⟩
    exact ⟨{
      toFun t := ⟨F t, hF t⟩
      map_zero_left := by simp
      map_one_left := by simp
      prop' := by simp
    }⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (trivialCofibrations (Over S)).HasFactorization (fibrations C).over

Tactic:
trivialCofibrations_over_eq

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (trivialCofibrations C).over.HasFactorization (fibrations C).over
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : S = Finset.univ
this✝ : n + 3 ≤ {i, j 0}.card
this : n + 3 ≤ 2
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this✝² : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
this✝¹ : Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} = ⊤
this✝ : n ≤ (Finset.image (⇑(SimplexCategory.Hom.toOrderHom f)) Finset.univ).card
this : n ≤ m + 1
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : stdSimplex.face {i}ᶜ ≤ Λ[n + 1, i]
⊢ False

Tactic:
stdSimplex.face_singleton_compl,

Goal state after:
case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) ≤ Λ[n + 1, i]
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd✝ : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
⊢ n + 1 + 1 ≤ S.card

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
this : Sᶜ.card + S.card = n + 1 + 1
⊢ Sᶜ.card = 1

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : Epi f
this : n + 1 ≤ m
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm (q ≫ SimplexCategory.δ i) ∈ (stdSimplex.face {i}ᶜ).obj (op ⦋m⦌)

Tactic:
stdSimplex.face_singleton_compl,

Goal state after:
case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm (q ≫ SimplexCategory.δ i) ∈
    (Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i))).obj (op ⦋m⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : {j}ᶜ ⊆ S
⊢ S = Finset.univ ∨ S = {j}ᶜ

Tactic:
← Finset.compl_subset_compl,

Goal state after:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : Sᶜ ⊆ {j}ᶜᶜ
⊢ S = Finset.univ ∨ S = {j}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : {i, a, b} = univ
this : n + 1 ≤ #{i, a, b}
⊢ False

Tactic:
lia

Goal state after: