mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
hs : s = ∅ ∨ s = {0}
⊢ #s ≤ #(s * s)

Tactic:
obtain rfl | rfl := hs

Goal state after:
case inl.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
inst✝ : IsLeftCancelMulZero α
⊢ #∅ ≤ #(∅ * ∅)

case inl.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
inst✝ : IsLeftCancelMulZero α
⊢ #{0} ≤ #({0} * {0})
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬s ⊆ 0
⊢ ↑(s • univ) = ↑univ

Tactic:
← coe_subset

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
s : Set ι
hst : s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}
hv_one : ∀ (i : ι), v i ≠ 1
⊢ s.Pairwise fun i j ↦ v i / v j ∉ range v

Tactic:
apply pairwise_div_notMem_range v hv_one hv_inv s {i | 1 < f (v i)} hst fun i ↦ ?_

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
s : Set ι
hst : s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}
hv_one : ∀ (i : ι), v i ≠ 1
i : ι
⊢ i ∈ {i | 1 < f (v i)} ∨ i⁻¹ ∈ {i | 1 < f (v i)}
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
⊢ f (v i) ≠ 1

Tactic:
rcases hsp with hi' | hi'

Goal state after:
case inr.inl
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : v i ∈ closure (v '' s)
⊢ f (v i) ≠ 1

case inr.inr
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ f (v i) ≠ 1
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X : FintypeCat
f : X.obj → X.obj
⊢ homMk f = 𝟙 X ↔ f = id

Tactic:
constructor
  · intro h
    ext x
    exact ConcreteCategory.congr_hom h x
  · rintro rfl
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
⊢ homMk h = homMk f ≫ homMk g ↔ h = g ∘ f

Tactic:
constructor
  · intro h
    ext x
    exact ConcreteCategory.congr_hom h x
  · rintro rfl
    rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 C).map ((drop.map η).app (op ⦋0⦌)) ≫
      { left := drop.obj Y✝ _⦋0⦌, right := point.obj Y✝, hom := Y✝.hom.app (op ⦋0⦌) }.hom =
    { left := drop.obj X✝ _⦋0⦌, right := point.obj X✝, hom := X✝.hom.app (op ⦋0⦌) }.hom ≫ (𝟭 C).map (point.map η)

Tactic:
by simp [w_app]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 C).map (point.map η) ≫ { left := point.obj Y✝, right := drop.obj Y✝ ^⦋0⦌, hom := Y✝.hom.app ⦋0⦌ }.hom =
    { left := point.obj X✝, right := drop.obj X✝ ^⦋0⦌, hom := X✝.hom.app ⦋0⦌ }.hom ≫ (𝟭 C).map ((drop.map η).app ⦋0⦌)

Tactic:
by simp [w_app]

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

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter (i + 1) h)) k) =
    ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) ((ConcreteCategory.hom (δ 0)) k))

Tactic:
coe_δ,

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter (i + 1) h)) k) = ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) (Fin.succAbove 0 k))
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ j)) ((ConcreteCategory.hom (δ₀Iter i hi)) k)) =
    ↑((ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k)

Tactic:
coe_δ,

Goal state after:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑(j.succAbove ((ConcreteCategory.hom (δ₀Iter i hi)) k)) = ↑((ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) h).op = X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i ⋯).op

Tactic:
SimplexCategory.δ₀Iter_succ' _ h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i ⋯).op =
    X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i ⋯).op
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this✝ : Epi (σ i ≫ θ')
this : Epi θ'
⊢ σ i ≫ 𝟙 ⦋n⦌ = σ i

Tactic:
Category.comp_id

Goal state after:
case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this✝ : Epi (σ i ≫ θ')
this : Epi θ'
⊢ σ i = σ i
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case succ
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m),
    ↑j = ↑j' + i → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ σ₀Iter i ⋯ ≫ σ (Fin.castSucc 0) ≫ σ j' = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'

Tactic:
Fin.castSucc_zero

Goal state after:
case succ
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m),
    ↑j = ↑j' + i → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ σ₀Iter i ⋯ ≫ σ 0 ≫ σ j' = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (ofSection x).image f ≤ ofSection ((ConcreteCategory.hom (f.app X)) x)

pp: case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ ofSection ((ConcreteCategory.hom (f.app X)) x) ≤ (ofSection x).image f

Tactic:
· rw [image_le_iff, ofSection_le_iff, preimage_obj, Set.mem_preimage]
    exact ⟨𝟙 X, by simp⟩

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ ofSection ((ConcreteCategory.hom (f.app X)) x) ≤ (ofSection x).image f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ (ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x ∈ (Subcomplex.range f).toSSet.degenerate n ↔ x ∈ ⊤

Tactic:
Subcomplex.mem_degenerate_iff,

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ ↑((ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x) ∈ Y.degenerate n ↔ x ∈ ⊤
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j : ι
⊢ (limitIsoPi ι X).hom ≫ Pi.π (fun x ↦ X) j = WidePullback.π (fun x ↦ terminal.from X) j

Tactic:
← wideCospan.limitIsoPi_inv_comp_pi,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j : ι
⊢ (limitIsoPi ι X).hom ≫ (limitIsoPi ι X).inv ≫ WidePullback.π (fun x ↦ terminal.from X) j =
    WidePullback.π (fun x ↦ terminal.from X) j
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
y : X.N
⊢ opObjEquiv.symm y.simplex ∈ X.op.nonDegenerate y.dim

Tactic:
by simpa [← opObjEquiv_mem_nonDegenerate_iff] using y.nonDegenerate

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

Goal state before:
pp: case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝¹ ≤ x✝

Tactic:
N.le_iff,

Goal state after:
case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝¹.subcomplex ≤ x✝.subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝ ≤ x✝¹

Tactic:
N.le_iff,

Goal state after:
case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝.subcomplex ≤ x✝¹.subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, s⟩ => N.mk ((ConcreteCategory.hom ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌))) s.simplex) ⋯)
        a =
      N.mk ↑⟨⟨s, h₁⟩, h₂⟩ ⋯

Tactic:
Subcomplex.mem_nonDegenerate_iff

Goal state after:
X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂✝ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
h₂ : ↑⟨s, h₁⟩ ∈ X.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, s⟩ => N.mk ((ConcreteCategory.hom ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌))) s.simplex) ⋯)
        a =
      N.mk ↑⟨⟨s, h₁⟩, h₂✝⟩ ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂✝ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
h₂ : ↑⟨s, h₁⟩ ∈ X.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ⟨s, hi⟩ ∈ (A i).toSSet.nonDegenerate d

Tactic:
Subcomplex.mem_nonDegenerate_iff

Goal state after:
X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂✝ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
h₂ : ↑⟨s, h₁⟩ ∈ X.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ↑⟨s, hi⟩ ∈ X.nonDegenerate d
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this✝ : IsSplitEpi f
this : Function.Injective ⇑(ConcreteCategory.hom (X.map f.op))
⊢ (ConcreteCategory.hom (X.map (f ≫ 𝟙 ⦋m⦌).op)) ↑y = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
Category.comp_id

Goal state after:
case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this✝ : IsSplitEpi f
this : Function.Injective ⇑(ConcreteCategory.hom (X.map f.op))
⊢ (ConcreteCategory.hom (X.map f.op)) ↑y = (ConcreteCategory.hom (X.map f.op)) ↑y
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
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ

Tactic:
rw [h_eq_assoc _ _ k, h_eq_assoc _ _ (k + 1)]

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.succ ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑i.succ ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter ↑i.castSucc ⋯ ≫ ed.s (↑k + 1) ≫ X.left.σ₀Iter ↑i.castSucc ⋯ ≫ X.left.δ i.castSucc.succ
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 ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n})
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (a + x, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}

Tactic:
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢

Goal state after:
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 ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n})
a b : ℤ
h : a + b = n
⊢ a + x + b = n + x
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 ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x})
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
⊢ (a - x, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}

Tactic:
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢

Goal state after:
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 ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x})
a b : ℤ
h : a + b = n + x
⊢ a - x + b = n
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 ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n})
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (a, b + y) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}

Tactic:
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢

Goal state after:
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 ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n})
a b : ℤ
h : a + b = n
⊢ a + (b + y) = n + y
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 ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y})
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}
⊢ (a, b - y) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}

Tactic:
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢

Goal state after:
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 ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y})
a b : ℤ
h : a + b = n + y
⊢ a + (b - y) = n
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 ℤ)
n n' : ℤ
h : n + x = n'
i₁✝ i₂✝ : ℤ
hi✝ : (up ℤ).π (up ℤ) (up ℤ) (i₁✝, i₂✝) = n'
⊢ (K.ιTotal (up ℤ) i₁✝ i₂✝ n' hi✝ ≫
      (K.totalDesc fun p q hpq ↦
          (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n ⋯) ≫
        ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n' ⋯) =
    K.ιTotal (up ℤ) i₁✝ i₂✝ n' hi✝ ≫ 𝟙 ((K.total (up ℤ)).X n')

Tactic:
simp only [ι_totalDesc_assoc, Category.assoc, ι_totalDesc, XXIsoOfEq_inv_ιTotal, comp_id]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroMorphisms C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ L₂ : CochainComplex C₂ ℤ
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (Hom.isoOfComponents
              (fun x ↦
                Iso.refl
                  (((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                            ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).X
                        i).X
                    x))
              ⋯).hom ≫
          ((HomologicalComplex₂.shiftFunctor₂ D y).obj
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).d
            i j =
        (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).d
            i j ≫
          (Hom.isoOfComponents
              (fun x ↦
                Iso.refl
                  (((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                            ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).X
                        j).X
                    x))
              ⋯).hom

Tactic:
by
      intros
      ext
      dsimp
      simp only [id_comp, comp_id]

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

Goal state before:
pp: case e_a
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ ((K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x).hom ≫
        (HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom) ≫
      (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
        (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂) =
    (((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
          y).hom ≫
      (HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom

Tactic:
ext a b

Goal state after:
case e_a
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
a b : ℤ
⊢ ((((K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F
                    x).hom ≫
                (HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom) ≫
              (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).f
          a).f
      b =
    (((((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
                  y).hom ≫
              (HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom).f
          a).f
      b
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case neg.h
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : ¬c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
⊢ ¬c₁.Rel i₁ (c₁.next i₁)

Tactic:
· intro h₂
      apply h₁
      have := ComplexShape.rel_π₁ c₂ c₁₂ h₂ i₂
      rw [c₁₂.next_eq' this]
      exact this

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
X✝ Y✝ Z W : C
f✝ : X✝ ⟶ Y✝
s : X✝ ⟶ Z
g : Z ⟶ W
t✝ : Y✝ ⟶ W
J : Type u_2
A B : J → C
inst✝² : HasCoproduct A
inst✝¹ : HasCoproduct B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst✝ : ∀ (j : J), HasLiftingProperty (f j) p
t : ∐ A ⟶ X
b : ∐ B ⟶ Y
sq : CommSq t (Limits.Sigma.map f) p b
⊢ sq.HasLift

Tactic:
by
    have sq' (j : J) :
        CommSq (Sigma.ι _ j ≫ t) (f j) p (Sigma.ι _ j ≫ b) :=
      ⟨by simp [sq.w]⟩
    exact ⟨⟨{ l := Sigma.desc (fun j ↦ (sq' j).lift) }⟩⟩

Goal state after: