mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _
      (Fin.castSucc_le_castSucc_iff.mpr hjk), Fin.castPred_castSucc,
      Fin.predAbove_of_le_castSucc _ _ hjk, Fin.succAbove_of_castSucc_lt, Fin.castSucc_castPred]

Goal state after:
case inl.inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc < i
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g.unop.op ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀

Tactic:
simpa only [← X.map_comp, ← Category.assoc, Category.comp_id, ← op_comp] using w _ _ _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
⊢ δ₀Iter (i + 1) h = δ 0 ≫ δ₀Iter i ⋯

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  rw [dsimp% ConcreteCategory.comp_apply (δ 0) (δ₀Iter i), coe_δ,
    δ₀Iter_apply .., δ₀Iter_apply ..]
  dsimp
  lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ (Hom.toOrderHom θ) y.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) y)

Tactic:
h''

Goal state after:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ (Hom.toOrderHom θ) i.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : m + j = n
hi' : j < ↑i
hi'' : ↑i = ↑i' + j
⊢ δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'

Tactic:
by
  induction j generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    obtain rfl : i = i' := by lia
    simp
  | succ j hj =>
    rw [σ₀Iter_succ _, σ₀Iter_succ_assoc _,
      reassoc_of% hj _ i'.succ (by lia) (by lia) (by grind),
      dsimp% δ_comp_σ_of_gt (i := i') (j := 0)
        (by rw [Fin.lt_def]; dsimp; lia)]

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

Goal state before:
pp: X✝ Y✝ : SSet
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso f

Tactic:
by
    rw [NatTrans.isIso_iff_isIso_app]
    intro
    rw [isIso_iff_bijective]
    constructor
    · rw [← mono_iff_injective]
      infer_instance
    · rw [← epi_iff_surjective]
      infer_instance

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

Goal state before:
pp: X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
y : X _⦋d⦌
hy : y ∈ X.nonDegenerate d
h : mk ↑⟨x, hx⟩ ⋯ < mk ↑⟨y, hy⟩ ⋯
w✝ : Mono (𝟙 ⦋(mk ↑⟨x, hx⟩ ⋯).dim⦌)
hf : (ConcreteCategory.hom (X.map (𝟙 ⦋(mk ↑⟨x, hx⟩ ⋯).dim⦌).op)) (mk ↑⟨y, hy⟩ ⋯).simplex = (mk ↑⟨x, hx⟩ ⋯).simplex
⊢ y = x

Tactic:
simpa using hf

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

Goal state before:
pp: X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h : ∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) (mk ↑⟨x₂, hx₂⟩ ⋯).simplex = (mk ↑⟨x₁, hx₁⟩ ⋯).simplex
h' : mk ↑⟨x₂, hx₂⟩ ⋯ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = mk ↑⟨x₂, hx₂⟩ ⋯

Tactic:
obtain ⟨f, hf, h⟩ := h

Goal state after:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h' : mk ↑⟨x₂, hx₂⟩ ⋯ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
f : ⦋(mk ↑⟨x₁, hx₁⟩ ⋯).dim⦌ ⟶ ⦋(mk ↑⟨x₂, hx₂⟩ ⋯).dim⦌
hf : Mono f
h : (ConcreteCategory.hom (X.map f.op)) (mk ↑⟨x₂, hx₂⟩ ⋯).simplex = (mk ↑⟨x₁, hx₁⟩ ⋯).simplex
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = mk ↑⟨x₂, hx₂⟩ ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite (Y _⦋i⦌)

Tactic:
rw [NatTrans.epi_iff_epi_app] at hf

Goal state after:
X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite (Y _⦋i⦌)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter ↑i ⋯ ≫ X.left.δ 0 ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑i + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter ↑i ⋯ ≫ X.left.δ 0 ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑i ⋯

Tactic:
X.left.σ₀Iter_δ _ _ (by grind)

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter ↑i ⋯ ≫ X.left.δ 0 ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑i ⋯ =
    X.left.δ₀Iter ↑i ⋯ ≫ X.left.δ 0 ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑i ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
⊢ objEquiv.symm (𝟙 (unop (op ⦋n⦌))) ∈ Δ[n].nonDegenerate n

Tactic:
rw [mem_nonDegenerate_iff_strictMono]

Goal state after:
n : ℕ
⊢ StrictMono ⇑(objEquiv.symm (𝟙 (unop (op ⦋n⦌))))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_1
n : ℕ
x : Δ[n] _⦋n⦌
h : x ∈ Δ[n].nonDegenerate n
⊢ x = objEquiv.symm (𝟙 ⦋n⦌)

Tactic:
obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x
    have : Mono f := by simpa using (mem_nonDegenerate_iff_mono _).mp h
    simpa only [EmbeddingLike.apply_eq_iff_eq] using SimplexCategory.eq_id_of_mono f

Goal state after:
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p : ℤ
⊢ (p + 1).negOnePow = -p.negOnePow

Tactic:
rw [Int.negOnePow_succ]

Goal state after:
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q + p).negOnePow = (p * (q + 1)).negOnePow

Tactic:
mul_add,

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q + p).negOnePow = (p * q + p * 1).negOnePow
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0

Tactic:
by exact ed.s'

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = r (i₁, i₂, i₃)

Tactic:
← ρ₁₂.hpq

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = ρ₁₂.q (ρ₁₂.p ((i₁, i₂, i₃).1, (i₁, i₂, i₃).2.1), (i₁, i₂, i₃).2.2)
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
⊢ ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = r (i₁, i₂, i₃)

Tactic:
← ρ₁₂.hpq

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
⊢ ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = ρ₁₂.q (ρ₁₂.p ((i₁, i₂, i₃).1, (i₁, i₂, i₃).2.1), (i₁, i₂, i₃).2.2)
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
have h₄ : ComplexShape.π c₁ c₂ c (i₁, ComplexShape.next c₂ i₂) = j' := by
        rw [← h₃, ComplexShape.π_symm c₁ c₂ c]

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

pp: case neg
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

Tactic:
· simp [totalAux.d₁_eq' _ c₁₂ h]

Goal state after:
case neg
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁶ : TotalComplexShape c₁ c₂ c
inst✝⁵ : TotalComplexShape c₂ c₁ c
inst✝⁴ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝³ : K.HasTotal c
inst✝² : DecidableEq J
inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c
inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ c₂.σ c₁ c i₂ i₁ • K.flip.ιTotal c i₂ i₁ j ⋯ = c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯

Tactic:
ComplexShape.σ_symm

Goal state after:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁶ : TotalComplexShape c₁ c₂ c
inst✝⁵ : TotalComplexShape c₂ c₁ c
inst✝⁴ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝³ : K.HasTotal c
inst✝² : DecidableEq J
inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c
inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯ = c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
x✝ : c₁₂.Rel i₁₂ i₁₂'
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ (L.D₁ c₁₂ i₁₂ i₁₂' + L.D₂ c₁₂ i₁₂ i₁₂') =
    (K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂') ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'

Tactic:
rw [comp_add, add_comp, mapAux.mapMap_D₁, mapAux.mapMap_D₂]

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
⊢ ((shiftFunctor₂ C y ⋙ shiftFunctor₁ C x).obj K).HasTotal (up ℤ)

Tactic:
dsimp
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
⊢ ((shiftFunctor₁ C x ⋙ shiftFunctor₂ C y).obj K).HasTotal (up ℤ)

Tactic:
dsimp
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫
        ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow •
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₁ (up ℤ) n₀' n₁')

Tactic:
ι_D₁_assoc,

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₁ C x).obj K).d₁ (up ℤ) p q n₁ ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow •
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₁ (up ℤ) n₀' n₁')
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

Tactic:
rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]

Goal state after:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ¬(up ℤ).Rel n₀' n₁'
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₂ C y).obj K).D₁ (up ℤ) n₀ n₁ ≫
        ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (y.negOnePow •
        (((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₀' ⋯) ≫
          K.D₁ (up ℤ) n₀' n₁')

Tactic:
ι_D₁_assoc,

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₂ C y).obj K).d₁ (up ℤ) p q n₁ ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (y.negOnePow •
        (((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₀' ⋯) ≫
          K.D₁ (up ℤ) n₀' n₁')
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₂ C y).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

Tactic:
rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]

Goal state after:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ¬(up ℤ).Rel n₀' n₁'
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ :
  (e.extendHomotopyFunctor C).obj ((HomotopyCategory.quotient C c).obj K) ⟶
    (e.extendHomotopyFunctor C).obj ((HomotopyCategory.quotient C c).obj L)
⊢ ∃ a, (e.extendHomotopyFunctor C).map a = φ

Tactic:
obtain ⟨φ : K.extend e ⟶ L.extend e, rfl⟩ :=
      (HomotopyCategory.quotient C c').map_surjective φ

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ : K.extend e ⟶ L.extend e
⊢ ∃ a, (e.extendHomotopyFunctor C).map a = (HomotopyCategory.quotient C c').map φ
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
G : C ⥤ D
inst✝ : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ (MorphismProperty.ofHoms fun x ↦ i).rlp (G.asEquivalence.inverse.map (G.asEquivalence.functor.map p)) ↔
    (MorphismProperty.ofHoms fun x ↦ i).rlp p

Tactic:
exact MorphismProperty.arrow_mk_iso_iff _
    (Arrow.isoMk (G.asEquivalence.unitIso.symm.app _)
      (G.asEquivalence.unitIso.symm.app _)
      (G.asEquivalence.unitIso.inv.naturality p).symm)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (P.ι.map f)

Tactic:
dsimp
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
inst✝¹ : (fibrations C).IsStableUnderComposition
X Y : C
p : X ⟶ Y
inst✝ : Fibration p
hY : IsFibrant Y
⊢ IsFibrant X

Tactic:
by
  rw [isFibrant_iff] at hY ⊢
  rw [Subsingleton.elim (terminal.from X) (p ≫ terminal.from Y)]
  infer_instance

Goal state after: