mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 = 0

Tactic:
have : a * 0 = a * 0 + a * 0 :=
      calc a * 0 = a * (0 + 0) := by rw [zero_add]
      _ = a * 0 + a * 0 := by rw [left_distrib]

Goal state after:
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = a * 0 + a * 0
⊢ a * 0 = 0
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
⊢ DivisionRing α

Tactic:
apply e.injective.divisionRing _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ (mk L₂).toWord)

Tactic:
toWord_mk

Goal state after:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ reduce L₂)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ ↑((algebraMap S R) 0) = 0

Tactic:
simp only [map_zero, coe_zero]

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0

Tactic:
rw [fwdDiff_iter_pow_eq_zero_of_lt (mem_range.mp hi), smul_zero, Pi.zero_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ #↑s⁻¹ = #↑s

Tactic:
← image_inv_eq_inv,

Goal state after:
G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ #↑((fun x ↦ x⁻¹) '' s) = #↑s
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Submonoid M
p : (x : M) → x ∈ s.saturation → Prop
mem : ∀ (x : M) (hx : x ∈ s), p x ⋯
mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯
of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯
x : M
hx : x ∈ s.saturation
⊢ p x hx

Tactic:
let s' : SaturatedSubmonoid M :=
  { carrier := { x | ∃ hx, p x hx }
    one_mem' := ⟨_ , mem 1 <| one_mem s⟩
    mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
    mulSaturated := fun x y ⟨_, hpxy⟩ ↦ ⟨⟨_, (of_mul _ _ _ hpxy).1⟩, ⟨_, (of_mul _ _ _ hpxy).2⟩⟩ }

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
s : Submonoid M
p : (x : M) → x ∈ s.saturation → Prop
mem : ∀ (x : M) (hx : x ∈ s), p x ⋯
mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯
of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯
x : M
hx : x ∈ s.saturation
s' : SaturatedSubmonoid M :=
  { carrier := {x | ∃ (hx : x ∈ s.saturation), p x hx}, mul_mem' := ⋯, one_mem' := ⋯, mulSaturated := ⋯ }
⊢ p x hx
Module: Mathlib.Algebra.GroupWithZero.Action.Center

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
⊢ r * ↑↑u = ↑↑u * r

Tactic:
obtain rfl | hr := eq_or_ne r 0

Goal state after:
case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
⊢ 0 * ↑↑u = ↑↑u * 0

case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
hr : r ≠ 0
⊢ r * ↑↑u = ↑↑u * r
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}
⊢ s.Pairwise fun i j ↦ v i / v j ∉ range v

Tactic:
have hv_one : ∀ i, v i ≠ 1 := fun i ↦ by contrapose! hf; exact ⟨i, by simp [hf]⟩

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
⊢ s.Pairwise fun i j ↦ v i / v j ∉ range v
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

pp: case neg
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : ¬y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

Tactic:
· by_contra h''
                  apply not_le.mpr h'
                  convert! f.toOrderHom.monotone (le_of_not_ge h'')
                  all_goals
                    exact (ConcreteCategory.congr_hom (Iso.inv_hom_id
                      (asIso ((forget SimplexCategory).map f))) _).symm

Goal state after:
case neg
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : ¬y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ (p.app (op ⦋n✝⦌) ≫ H.h j) ≫ Y.σ i.castSucc = X'.σ i ≫ p.app (op ⦋n✝ + 1⦌) ≫ H.h j.succ

Tactic:
by
    simpa using p.app _ ≫= H.h_comp_σ_castSucc_of_le i j hij

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

Goal state before:
pp: n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
⊢ ¬Function.Injective ⇑(Hom.toOrderHom θ)

Tactic:
rw [← mono_iff_injective]

Goal state after:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
⊢ ¬Mono θ
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

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

Tactic:
rw [σ₀Iter_coe_eq_of_lt (i + 1) ..]

Goal state after:
case neg
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : ↑k ≤ i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) (j.predAbove k)) = 0
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ F.hom ≫ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j) = Arrow.Hom.left G ≫ X.hom.app x

Tactic:
rw [← Arrow.w_assoc G]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ Arrow.Hom.left G ≫ (Augmented.toArrow.obj X).hom ≫ X.right.map (⦋0⦌.const x j) = Arrow.Hom.left G ≫ X.hom.app x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: case left
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X✝))

Tactic:
rw [← mono_iff_injective]

Goal state after:
case left
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Mono (f.app X✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ ∃ x_1, x_1.subcomplex = { dim := n, simplex := x }.subcomplex

Tactic:
obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x

Goal state after:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ ∃ x, x.subcomplex = { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
⊢ f₁ = f₂

Tactic:
ext x : 3
  suffices ∃ (hf₁ : SplitEpi f₁), hf₁.section_.toOrderHom (f₁.toOrderHom x) = x by
    obtain ⟨hf₁, hf₁'⟩ := this
    dsimp at hf₁'
    simpa [g, hf₁'] using (SimplexCategory.congr_toOrderHom_apply (g_eq_id hy₁ hy₂ hf₁)
      (f₁.toOrderHom x)).symm
  obtain ⟨⟨hf⟩⟩ := isSplitEpi_of_epi f₁
  let α (y : Fin (m + 1)) : Fin (n + 1) :=
    if y = f₁.toOrderHom x then x else hf.section_.toOrderHom y
  have hα₁ (y : Fin (m + 1)) : f₁.toOrderHom (α y) = y := by
    dsimp [α]
    split_ifs with hy
    · rw [hy]
    · apply SimplexCategory.congr_toOrderHom_apply hf.id
  have hα₂ : Monotone α := by
    rintro y₁ y₂ h
    by_contra! h'
    suffices y₂ ≤ y₁ by simp [show y₁ = y₂ by lia] at h'
    simpa only [hα₁] using f₁.toOrderHom.monotone h'.le
  exact ⟨{ section_ := SimplexCategory.Hom.mk ⟨α, hα₂⟩, id := by ext : 3; apply hα₁ },
    by simp [α]⟩

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

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

Tactic:
rw [← mono_iff_injective]

Goal state after:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this : IsSplitEpi f
⊢ Mono (X.map f.op)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.toN = y
⊢ ∃! f_1,
    Epi f_1 ∧
      (ConcreteCategory.hom (X.map f_1.op)) y.simplex =
        { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.simplex

Tactic:
obtain rfl : y = N.mk _ z.2 := by
    rw [toN_eq_iff] at hy
    rw [← N.subcomplex_injective_iff, hy]
    exact subcomplex_eq_of_epi _ _ f rfl

Goal state after:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.toN = N.mk ↑z ⋯
⊢ ∃! f_1,
    Epi f_1 ∧
      (ConcreteCategory.hom (X.map f_1.op)) (N.mk ↑z ⋯).simplex =
        { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.simplex
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 F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
x : I₁ × I₂ × I₃
⊢ ((F.obj (X₁ x.1)).map (ψ x.2.1)).app (X₃ x.2.2) ≫ ((F.map (φ x.1)).app (Y₂ x.2.1)).app (X₃ x.2.2) =
    ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2) ≫ ((F.obj (Y₁ x.1)).map (ψ x.2.1)).app (X₃ x.2.2)

Tactic:
simp only [← NatTrans.comp_app]

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 F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
x : I₁ × I₂ × I₃
⊢ ((F.obj (X₁ x.1)).map (ψ x.2.1) ≫ (F.map (φ x.1)).app (Y₂ x.2.1)).app (X₃ x.2.2) =
    ((F.map (φ x.1)).app (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1)).app (X₃ x.2.2)
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0

Tactic:
rw [← comp_f, d_comp_d, zero_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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
⊢ ∀ (i₁ : ℤ) {i₂ i₂' : ℤ},
    (up ℤ).Rel i₂ i₂' →
      (i₁ * i₂).negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (i₁, i₂) = (up ℤ).ε₁ (up ℤ) (up ℤ) (i₂, i₁) * (i₁ * i₂').negOnePow

Tactic:
rintro p q _ rfl
    dsimp
    rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]

Goal state after:
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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ 0

Tactic:
simp only [totalAux.ιMapObj_D₁_assoc, comp_zero]

Goal state after:
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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0
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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ f =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ g

Tactic:
exact h i₁ i₂ hi

Goal state after:
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
j j' : J
⊢ (K.totalFlipIso c).hom.f j ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIso c).hom.f j'

Tactic:
by
  apply totalFlipIsoX_hom_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 ℤ)
n n' : ℤ
h : n + x = n'
⊢ ((((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n' ⋯) ≫
      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).total (up ℤ)).X n)

Tactic:
ext p q 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 n' : ℤ
h✝ : n + x = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
⊢ (((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n h ≫
      (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n' ⋯) ≫
        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).ιTotal (up ℤ) p q n h ≫ 𝟙 ((((shiftFunctor₁ C x).obj K).total (up ℤ)).X n)
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: 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₄
i₁ i₁' : ι₁
h₁ : c₁.Rel i₁ i₁'
i₂ : ι₂
i₃ : ι₃
j : ι₄
⊢ d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) •
      (G.map ((F₁₂.map (K₁.d i₁ i₁')).app (K₂.X i₂))).app (K₃.X i₃) ≫ ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁' i₂ i₃ j

Tactic:
by
  obtain rfl := c₁.next_eq' h₁
  rfl

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 : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
⊢ total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom =
    (K.totalShift₁Iso x).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) x).map (total.map f (up ℤ))

Tactic:
ext n i₁ i₂ 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 : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom).f n =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      ((K.totalShift₁Iso x).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) x).map (total.map f (up ℤ))).f 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 + y = n'
⊢ ((((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' ⋯) ≫
      K.totalDesc fun p q hpq ↦
        (p * y).negOnePow •
          (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) =
    𝟙 ((((shiftFunctor₂ C y).obj K).total (up ℤ)).X n)

Tactic:
ext p q 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 n' : ℤ
h✝ : n + y = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
⊢ (((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n h ≫
      (((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' ⋯) ≫
        K.totalDesc fun p q hpq ↦
          (p * y).negOnePow •
            (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n h ≫ 𝟙 ((((shiftFunctor₂ C y).obj K).total (up ℤ)).X 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 + y = n'
⊢ ((K.totalDesc fun p q hpq ↦
        (p * y).negOnePow •
          (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' ⋯) =
    𝟙 ((K.total (up ℤ)).X n')

Tactic:
ext
    dsimp
    simp only [ι_totalDesc_assoc, Linear.units_smul_comp, Category.assoc, ι_totalDesc,
      Linear.comp_units_smul, XXIsoOfEq_inv_ιTotal, smul_smul, Int.units_mul_self, one_smul,
      comp_id]

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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
⊢ total.map ((shiftFunctor₂ C y).map f) (up ℤ) ≫ (L.totalShift₂Iso y).hom =
    (K.totalShift₂Iso y).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) y).map (total.map f (up ℤ))

Tactic:
ext n i₁ i₂ 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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₂ C y).map f) (up ℤ) ≫ (L.totalShift₂Iso y).hom).f n =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      ((K.totalShift₂Iso y).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) y).map (total.map f (up ℤ))).f n