mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.inl.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux (n + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
          contsAux_stable_step_of_terminated terminated

Goal state after:
case succ.inl.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux (n + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
this : g.contsAux (n + 2) = g.contsAux (n + 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ 0 ≤ ((of v).contsAux n).b

Tactic:
by
  let g := of v
  induction n with
  | zero => rfl
  | succ n IH =>
    rcases Decidable.em <| g.TerminatedAt (n - 1) with terminated | not_terminated
    · -- terminating case
      rcases n with - | n
      · simp
      · have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
          contsAux_stable_step_of_terminated terminated
        simp only [g, this, IH]
    · -- non-terminating case
      calc
        (0 : K) ≤ fib (n + 1) := mod_cast (n + 1).fib.zero_le
        _ ≤ ((of v).contsAux (n + 1)).b := fib_le_of_contsAux_b (Or.inr not_terminated)

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : n ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      n =
    (↑f).coeff n

Tactic:
interval_cases n <;> simp only <;> ring_nf

Goal state after:
case inl.«0»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 0 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 0 = (↑f).coeff 0

case inl.«1»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 1 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 1 = (↑f).coeff 1

case inl.«2»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 2 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 2 = (↑f).coeff 2

case inl.«3»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 3 = (↑f).coeff 3
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inr.ha
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ 0 < b * (of v).dens n * (of v).dens n

Tactic:
have : 0 < b := zero_lt_one.trans_le (of_one_le_get?_partDen nth_partDen_eq)

Goal state after:
case inr.ha
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
this : 0 < b
⊢ 0 < b * (of v).dens n * (of v).dens n
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f.genEigenspace (b⁻¹ * a)) 1 = (f - (b⁻¹ * a) • 1).ker

Tactic:
rw [genEigenspace_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c b) id * ((toMatrix c c) f * (toMatrix b c) id)).trace =
    ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace

Tactic:
Matrix.trace_mul_comm

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace =
    ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
μ : R
x✝ : μ ∈ s
⊢ Submodule.map (g ^ l) ((f.genEigenspace μ) k) ≤ (f.genEigenspace μ) k

Tactic:
rintro - ⟨u, hu, rfl⟩

Goal state after:
case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
μ : R
x✝ : μ ∈ s
u : M
hu : u ∈ ↑((f.genEigenspace μ) k)
⊢ (g ^ l) u ∈ (f.genEigenspace μ) k
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (trace R (Dual R M)) (Dual.transpose f) = (trace R M) f

Tactic:
by
  rw [← comp_apply, trace_transpose]

Goal state after:
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : DivisionSemiring α
inst✝ : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic (fun x ↦ f (x / a)) (c * a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const_inv ha

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ IsUnit (C ((algebraMap R K) f.leadingCoeff))

Tactic:
· simp_all

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nonempty
⊢ ↑(s • univ) = ↑univ

Tactic:
push_cast
    exact Set.smul_univ hs

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = ∏ i, f i ^ a i

Tactic:
rw [Finsupp.equivFunOnFinite.symm.exists_congr_left, mem_closure_range_iff]

Goal state after:
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = ∏ i, f i ^ a i

Tactic:
rw [Finsupp.equivFunOnFinite.symm.exists_congr_left, mem_closure_range_iff]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a : A
H : f a = 0
⊢ 0 = 1 ↔ f a = 1

Tactic:
simp [H, ← WithZero.coe_one, ← Units.mk0_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a : A
H : ¬f a = 0
⊢ ↑⟨Units.mk0 (f a) H, ⋯⟩ = 1 ↔ f a = 1

Tactic:
simp [H, ← WithZero.coe_one, ← Units.mk0_one]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ P.p ≫ (-f.f) ≫ Q.p = -f.f

Tactic:
simpa only [neg_comp, comp_neg, neg_inj] using f.comm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ X.eqToIso h = Iso.refl (X _⦋n⦌)

Tactic:
by
  simp [eqToIso]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
h : n = n
⊢ X.eqToIso h = Iso.refl (X ^⦋n⦌)

Tactic:
by
  simp [eqToIso]

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

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ y.len ≤ x.len

Tactic:
by
  simpa using Fintype.card_le_of_surjective f.toOrderHom.toFun
    (by dsimp; rwa [← epi_iff_surjective])

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

Goal state before:
pp: case inl
n m : ℕ
j : Fin (m + 1)
hi : n + ↑j = m
hj : ↑j ≤ ↑j
⊢ ↑((ConcreteCategory.hom (σ₀Iter (↑j) hi)) j) = 0

pp: case inr
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj✝ : ↑j ≤ i
hj : ↑j < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = 0

Tactic:
· rw [σ₀Iter_coe_eq_of_ge .., tsub_self]

Goal state after:
case inr
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj✝ : ↑j ≤ i
hj : ↑j < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
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 θ) (i.succ.succAbove y)

Tactic:
Fin.succAbove_of_le_castSucc i.succ _

Goal state after:
case neg
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 θ) y.succ

case neg
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
⊢ i.succ ≤ y.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ 0 % (n + 1 + 1) < ↑k - i

Tactic:
Nat.zero_mod

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ 0 < ↑k - i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
⊢ ∃ i, θ = σ i

Tactic:
obtain ⟨i, θ', h⟩ := eq_σ_comp_of_not_injective θ (by
    rw [← mono_iff_injective]
    grind [→ le_of_mono])
  use i
  have : Epi (σ i ≫ θ') := by
    rw [← h]
    infer_instance
  have := CategoryTheory.epi_of_epi (σ i) θ'
  rw [h, eq_id_of_epi θ', Category.comp_id]

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

Goal state before:
pp: case mpr
X : SSet
n m : ℕ
x✝ : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X.op _⦋m⦌
⊢ ∃ f_1,
    ∃ (_ : Epi f_1),
      opObjEquiv ((ConcreteCategory.hom (X.op.map f.op)) y) ∈ Set.range ⇑(ConcreteCategory.hom (X.map f_1.op))

Tactic:
exact ⟨SimplexCategory.rev.map f, inferInstance, opObjEquiv y, by simp [op_map]⟩

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

Goal state before:
pp: case neg
X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, Finite ↑(X.nonDegenerate i)
this✝ : ∀ (i : Fin d), Finite ↑(X.nonDegenerate ↑i)
x : X.N
hj : ¬x.dim < d
this : x.simplex ∈ X.nonDegenerate x.dim
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => N.mk ↑x ⋯)
        a =
      x

Tactic:
simp [X.nonDegenerate_eq_empty_of_hasDimensionLT d x.dim (by simpa using hj)] at this

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
⊢ ((ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))
          ((ConcreteCategory.hom (SimplicialObject.δ (nerve X) i.castSucc)) s)).obj
      j =
    s.obj j

Tactic:
rw [nerve.σ_obj, nerve.δ_obj]

Goal state after:
case mpr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ s ∈ (nerve X).nonDegenerate n ↔ Function.Injective s.obj

Tactic:
rw [mem_nerve_nonDegenerate_iff_strictMono]
  refine ⟨fun h ↦ h.injective, fun h i j hij ↦ ?_⟩
  obtain h' | h' := (s.monotone hij.le).lt_or_eq
  · exact h'
  · exact ((h h').not_lt hij).elim

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ (alternatingConst A hOdd hEven hc).iCycles j ≫ φ = 0

Tactic:
rw [← cancel_epi (ShortComplex.cyclesMapIso
    (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv]
  simpa [HomologicalComplex.iCycles, -Preadditive.IsIso.comp_left_eq_zero, HomologicalComplex.sc,
    HomologicalComplex.shortComplexFunctor, alternatingConstScIsoEven,
    Category.id_comp (X := (alternatingConst A hOdd hEven hc).X _)]
    using (ShortComplex.mk ψ φ hEven).iCycles_g

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case neg
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
j₁ : Fin ⦋n + 1⦌.len
hj₁ : i₁ = j₁.succ
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂

Tactic:
obtain ⟨j₂, hj₂⟩ := Fin.eq_succ_of_ne_zero h₂

Goal state after:
case neg
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
j₁ : Fin ⦋n + 1⦌.len
hj₁ : i₁ = j₁.succ
j₂ : Fin ⦋n + 1⦌.len
hj₂ : i₂ = j₂.succ
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) * 1 = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Tactic:
rw [← Int.units_mul_self (ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂')), mul_assoc]

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
⊢ ∀ (i j : I₂),
    c₂.Rel i j →
      d₁ i₁ i₁' i ≫ { X := fun i₂ ↦ X (i₁', i₂), d := fun i₂ i₂' ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ }.d i j =
        { X := fun i₂ ↦ X (i₁, i₂), d := fun i₂ i₂' ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ }.d i j ≫ d₁ i₁ i₁' j

Tactic:
by intros; apply comm

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
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun i₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) →
  Cocone
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i).1) ⋙ G.flip.obj (X₃ (↑i).2)) :=
  fun i ↦ (G.flip.obj (X₃ (↑i).2)).mapCocone (c₁₂ (↑i).1)
hc₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) → IsColimit (c₁₂' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → ρ₁₂.I₁₂ × I₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (ρ₁₂.p (i₁, i₂), i₃)
e : (i₁₂ : ρ₁₂.I₁₂) → (i₃ : I₃) → ↑(p' ⁻¹' {(i₁₂, i₃)}) ≃ ↑(ρ₁₂.p ⁻¹' {i₁₂}) :=
  fun i₁₂ i₃ ↦
    {
      toFun := fun x ↦
        match x with
        | ⟨(i₁, i₂, i₃'), hi⟩ => ⟨(i₁, i₂), ⋯⟩,
      invFun := fun x ↦
        match x with
        | ⟨(i₁, i₂), hi⟩ => ⟨(i₁, i₂, i₃), ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
x✝ : ↑(ρ₁₂.q ⁻¹' {j})
i₁₂ : ρ₁₂.I₁₂
i₃ : I₃
hi : (i₁₂, i₃) ∈ ρ₁₂.q ⁻¹' {j}
⊢ Z.CofanMapObjFun p' ((↑⟨(i₁₂, i₃), hi⟩).1, (↑⟨(i₁₂, i₃), hi⟩).2)

Tactic:
refine (Cocone.precompose (Iso.hom ?_)).obj ((Cocone.whiskeringEquivalence
        (Discrete.equivalence (e i₁₂ i₃))).functor.obj (c₁₂' ⟨⟨i₁₂, i₃⟩, hi⟩))
      refine (Discrete.natIso (fun ⟨⟨i₁, i₂, i₃'⟩, hi⟩ =>
        (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).mapIso (eqToIso ?_)))
      obtain rfl : i₃' = i₃ := congr_arg _root_.Prod.snd hi
      rfl

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

Goal state before:
pp: case neg
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'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom

Tactic:
· rw [K.D₂_shape _ _ _ h₀, K.flip.D₁_shape c _ _ h₀, zero_comp, comp_zero]

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₀
⊢ (((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q) •
        (((shiftFunctor₁ C x).obj K).d p (p + 1)).f q ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow • K.d₁ (up ℤ) (p + x) q n₁'

Tactic:
K.d₁_eq _ (show p + x + 1 = p + 1 + x by lia) _ _ (by dsimp; lia)

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₀
⊢ (((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q) •
        (((shiftFunctor₁ C x).obj K).d p (p + 1)).f q ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      (up ℤ).ε₁ (up ℤ) (up ℤ) (p + x, q) • (K.d (p + x) (p + 1 + x)).f q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯