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

Goal state before:
pp: q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
this : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(n + 1)

Tactic:
Int.natCast_succ,

Goal state after:
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
this : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
ppred_conts' : Pair K := g'.contsAux n'
n'th_contsAux_eq' : ppred_conts' = g'.contsAux n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this : g'.convs (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
⊢ g.convs (n' + 1 + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')

Tactic:
have : g.convs (n' + 2) =
          (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) := by
        -- use the recurrence once
        have : g.contsAux (n' + 2) = ⟨pb * pA + pa * ppA, pb * pB + pa * ppB⟩ :=
          contsAux_recurrence s_n'th_eq n'th_contsAux_eq.symm succ_n'th_contsAux_eq.symm
        -- and a second time
        rw [conv_eq_conts_a_div_conts_b,
          conts_recurrenceAux s_nth_eq succ_n'th_contsAux_eq.symm this]

Goal state after:
case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
ppred_conts' : Pair K := g'.contsAux n'
n'th_contsAux_eq' : ppred_conts' = g'.contsAux n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : g'.convs (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : g.convs (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ g.convs (n' + 1 + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
⊢ |v - (of v).convs n| ≤ 1 / ((of v).dens n * (of v).dens (n + 1))

Tactic:
change |v - convs g n| ≤ 1 / (conts.b * nextConts.b)

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂
⊢ e₁ = e₂

Tactic:
two_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂
⊢ e₁ = e₂
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (⁅f, g⁆ * h) = (trace R M) (f * ⁅g, h⁆)

Tactic:
simp only [Ring.lie_def, sub_mul, mul_sub, map_sub, mul_assoc]
  rw [trace_mul_comm R g (f * h), mul_assoc]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inl
α : Type u
h✝ : IsEmpty α
⊢ #(FreeCommRing α) = max #α ℵ₀

Tactic:
simp [FreeCommRing]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inr
α : Type u
h✝ : Nonempty α
⊢ #(FreeCommRing α) = max #α ℵ₀

Tactic:
simp [FreeCommRing]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ (∏ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ has ih =>
    simp_rw [Finset.prod_insert has]
    exact (Rat.mul_den_dvd ..).trans <| mul_dvd_mul_left _ ih

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
⊢ ∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
by
  suffices x ^ (f.map (algebraMap R S)).natDegree ∈ 𝓟.map (algebraMap R S) by
    intro i hi
    obtain ⟨k, hk⟩ := exists_add_of_le hi
    rw [hk, pow_add]
    exact mul_mem_right _ _ this
  rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx
  exact pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a * star a = ↑(normSq a)

Tactic:
rw [mul_star_eq_coe, normSq_def]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[P.natDegree + j + 1] (fun x ↦ eval x P) x = 0 x

Tactic:
rw [add_assoc, add_comm, Function.iterate_add_apply, Function.iterate_succ_apply,
    P.fwdDiff_iter_degree_eq_factorial, Pi.smul_def]

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[j] (Δ_[1] fun i ↦ P.leadingCoeff • ↑P.natDegree ! i) x = 0 x
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
⊢ SemigroupWithZero α

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

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : normalizedFactors (x ^ n) = normalizedFactors (y ^ n)
⊢ Associated x y

Tactic:
rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.LeftInverse (fun x ↦ (h.inv { down := x }).down) fun x ↦ (h.hom { down := x }).down

Tactic:
intro a
            change ULift.down _ = _
            rw [ULift.up_down]
            change ((h.hom ≫ h.inv) _).down = _
            simp
            rfl

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: n : ℕ
⊢ Fintype.card (incl.obj (mk n)).obj = n

Tactic:
by
  convert! Finset.card_fin n
  dsimp [incl, mk, len]
  convert! (Fintype.ofEquiv_card Equiv.ulift).symm

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ i ≫ 𝟙 X = i ≫ p

Tactic:
rw [comp_id, ← h₂, ← assoc, h₁, id_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
⊢ ∑ i ∈ S, ((-1) ^ ↑i.2 • X.δ i.2) ≫ ((-1) ^ ↑i.1 • X.δ i.1) =
    ∑ x ∈ Sᶜ, -((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1)

Tactic:
apply Finset.sum_bij φ

Goal state after:
case hi
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := ⋯
S : Finset P := ⋯
φ : (ij : P) → ij ∈ S → P := ⋯
⊢ ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ

case i_inj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := ⋯
S : Finset P := ⋯
φ : (ij : P) → ij ∈ S → P := ⋯
⊢ ∀ (a₁ : P) (ha₁ : a₁ ∈ S) (a₂ : P) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂

case i_surj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := ⋯
S : Finset P := ⋯
φ : (ij : P) → ij ∈ S → P := ⋯
⊢ ∀ b ∈ Sᶜ, ∃ a, ∃ (ha : a ∈ S), φ a ha = b

case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := ⋯
S : Finset P := ⋯
φ : (ij : P) → ij ∈ S → P := ⋯
⊢ ∀ (a : P) (ha : a ∈ S),
    ((-1) ^ ↑a.2 • X.δ a.2) ≫ ((-1) ^ ↑a.1 • X.δ a.1) =
      -((-1) ^ ↑(φ a ha).2 • X.δ (φ a ha).2) ≫ ((-1) ^ ↑(φ a ha).1 • X.δ (φ a ha).1)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := ⋯
S : Finset P := ⋯
φ : (ij : P) → ij ∈ S → P := ⋯
⊢ ∀ (a : P) (ha : a ∈ S),
    ((-1) ^ ↑a.2 • X.δ a.2) ≫ ((-1) ^ ↑a.1 • X.δ a.1) =
      -((-1) ^ ↑(φ a ha).2 • X.δ (φ a ha).2) ≫ ((-1) ^ ↑(φ a ha).1 • X.δ (φ a ha).1)

Tactic:
rintro ⟨i, j⟩ hij
    dsimp
    simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]
    congr 1
    · simp only [φ, Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
      apply mul_comm
    · rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
      simpa [S] using! hij

Goal state after:
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 : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.δ₀Iter i hi ≫ SimplexCategory.δ j).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op

Tactic:
SimplexCategory.δ₀Iter_δ ..

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst✝ : Mono f
⊢ { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } = { dim := n, simplex := x } ↔ IsIso f

Tactic:
by
  constructor
  · intro h
    obtain rfl := S.dim_eq_of_mk_eq h
    obtain rfl := SimplexCategory.eq_id_of_mono f
    infer_instance
  · intro hf
    obtain rfl := SimplexCategory.eq_of_isIso f
    obtain rfl := SimplexCategory.eq_id_of_isIso f
    simp

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

Goal state before:
pp: case succ
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
by_cases hx : x ∈ X.nonDegenerate (n + 1)

Goal state after:
case pos
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y

case neg
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∉ X.nonDegenerate (n + 1)
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (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 : ℕ
⊢ ed.s' ≫ X.left.σ₀Iter n ⋯ = ed.section_.app (op ⦋n⦌)

Tactic:
by
  dsimp [section_, SimplicialObject.σ₀Iter]
  congr 3
  subsingleton

Goal state after:
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₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
      (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ =
    0

Tactic:
K.shape_f _ _ h,

Goal state after:
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₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • 0 ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ = 0
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₁₂''
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

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 : 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₁₂''
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
· ext ⟨i₁, i₂⟩ h
      simp only [totalAux.ιMapObj_D₁_assoc, comp_zero]
      by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)
      · rw [totalAux.d₁_eq K c₁₂ h₃ i₂ i₁₂']; swap
        · rw [← ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
        by_cases h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
        · rw [totalAux.d₁_eq K c₁₂ h₄ i₂ i₁₂'', Linear.comp_units_smul,
            d_f_comp_d_f_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₁ c₂ c₁₂ h₄, ← ComplexShape.next_π₁ c₂ c₁₂ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
        · rw [K.d₁_eq_zero _ _ _ _ h₄, comp_zero, smul_zero]
      · rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp]

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 : 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₁₂''
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₂' ⥤ C₂
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁ : C₁
X₂' : C₂'
m n : M
⊢ (commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).obj ((shiftFunctor C₁ m).obj X₁)) n).hom.app X₂' ≫
      (shiftFunctor D n).map ((commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).flip.obj X₂') m).hom.app X₁) =
    (commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).flip.obj ((shiftFunctor C₂' n).obj X₂')) m).hom.app X₁ ≫
      (shiftFunctor D m).map ((commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).obj X₁) n).hom.app X₂') ≫
        (shiftComm (((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).obj X₁).obj X₂') m n).inv ≫
          (↑(h.ε m n)).app
            ((shiftFunctor D n).obj ((shiftFunctor D m).obj (((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).obj X₁).obj X₂')))

Tactic:
have := G.commShift₂_comm h X₁ (F.obj X₂') m n
    dsimp [commShiftIso] at this ⊢
    simp only [Category.comp_id, Category.id_comp, Category.assoc, map_comp]
    refine ((G.obj _).map _ ≫= this).trans ?_
    simp only [← Category.assoc]; congr 3
    exact (NatTrans.shift_app_comm (G.flip.map ((F.commShiftIso n).hom.app X₂')) m X₁).symm

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (n₁ * y + x * y).negOnePow • K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ =
    (n₁ * y + x * y).negOnePow •
      (K.shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ (n₂ + y)).hom ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) ⋯).inv ≫
            ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n

Tactic:
CochainComplex.shiftFunctorComm_hom_app_f

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (n₁ * y + x * y).negOnePow • K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ =
    (n₁ * y + x * y).negOnePow •
      (K.shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ (n₂ + y)).hom ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) ⋯).inv ≫
            ((K.total (up ℤ)).XIsoOfEq ⋯).hom
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
hi : ¬c.Rel (c.prev i) i
hi' : c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv = (prevD (e.f i)) (extend.hom e h.hom)

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
hi : ¬c.Rel (c.prev i) i
hi' : ¬c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv = (prevD (e.f i)) (extend.hom e h.hom)

Tactic:
· simp [prevD_eq _ hi', L.extend_d_to_eq_zero _ _ _ _ rfl hi]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
hi : ¬c.Rel (c.prev i) i
hi' : ¬c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv = (prevD (e.f i)) (extend.hom e h.hom)
Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : L.IsKInjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Function.Bijective toSmallShiftedHom

Tactic:
← Function.Bijective.of_comp_iff'
      (SmallShiftedHom.equiv _ DerivedCategory.Q).bijective,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : L.IsKInjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Function.Bijective
    (⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) ∘ toSmallShiftedHom)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case succ
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
ha : H a
⊢ H (a + 1)

Tactic:
| succ a ha =>

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case succ
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
ha : H a
⊢ H (a + 1)

Tactic:
| succ a ha =>

Goal state after: