mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = ⨆ g, orderOf g

Tactic:
by
  rw [iSup]
  by_cases ExponentExists G
  case neg he =>
    rw [← exponent_eq_zero_iff] at he
    rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
  case pos he =>
    rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]
    · simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
      exact orderOf_le_exponent he
    intro x hx
    obtain ⟨g, hg⟩ := exists_orderOf_eq_exponent he
    rw [← hg] at hx
    simp_rw [Set.mem_range, exists_exists_eq_and]
    exact ⟨g, hx⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
⊢ IsLocalHom f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R

Tactic:
by
  -- Porting note: inline `this` does **not** work
  have := (local_hom_TFAE f).out 0 4
  rw [this, PrimeSpectrum.ext_iff]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case mk
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
g✝ : G ⧸ torsion G
g : G
hne : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ≠ 1
hfin : IsOfFinOrder (Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g)
⊢ Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g = 1

Tactic:
obtain ⟨m, mpos, hm⟩ := hfin.exists_pow_eq_one

Goal state after:
case mk
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
g✝ : G ⧸ torsion G
g : G
hne : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ≠ 1
hfin : IsOfFinOrder (Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g)
m : ℕ
mpos : 0 < m
hm : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ^ m = 1
⊢ Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ x ^ 0 = ↑⟨y, ⋯⟩

Tactic:
zpow_zero,

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ 1 = ↑⟨y, ⋯⟩
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
t : Finset ι
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this✝ : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
i : ι
hi : i ∈ t
i✝ : i ≠ Exists.choose h
hat : i ∉ t
μ : (i_1 : ι) → ↥(⨅ j ∈ Finset.cons i t hat, ⨅ (_ : j ≠ i_1), I j)
hμ : ↑(μ i) + ∑ x ∈ t, ↑(μ x) = 1
this : i ∈ Finset.cons i t hat → i ≠ i → ↑(μ i) ∈ I i
⊢ False

Tactic:
exact hat hi

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
h : torsionBySet R M s = ⊤
x : M
⊢ ∀ ⦃a : ↑s⦄, ↑a • x = 0

Tactic:
rw [← mem_torsionBySet_iff, h]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
h : torsionBySet R M s = ⊤
x : M
⊢ x ∈ ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
e : F.N 0 ≤ F'.N 0
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n

Tactic:
obtain ⟨n₀, hF⟩ := h

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n

Tactic:
refine ⟨(F.antitone ?_).trans (h₁ n), (F'.antitone ?_).trans (h₂ n)⟩

Goal state after:
case h.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ n + n₁ ≤ n + max n₁ n₂

case h.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ n + n₂ ≤ n + max n₁ n₂
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (ε F).app ((F.obj n).obj X) =
    (𝟙 ((F.obj n).obj X) ≫ (ε F).app ((F.obj n).obj X) ≫ (μ F n (𝟙_ M)).app X) ≫ (δ F n (𝟙_ M)).app X

Tactic:
simp only [Category.id_comp, Category.assoc, μ_δ_app,
    endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.add 0 n).inv.app X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯

Tactic:
by
  rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]

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

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1 + 2) (n + 1 + 1) =
    (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁} ↦ succ') (n + 1)).hom ≫
      (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1 + 1) (n + 1))).snd.fst

Tactic:
apply mk_d

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
a b : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_rw [← Finsupp.smul_single_one _ (1 * _ : S)]; dsimp; simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q' : ℤ
hpq : p + 0 = p
⊢ (ofHoms ψ).v p p hpq ≫ G.d p q' = ψ p ≫ G.d p q'

Tactic:
ofHoms_v

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q' : ℤ
hpq : p + 0 = p
⊢ ψ p ≫ G.d p q' = ψ p ≫ G.d p q'
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p : ℤ
hpq : p + 0 = p
⊢ F.d p' p ≫ (ofHoms ψ).v p p hpq = F.d p' p ≫ ψ p

Tactic:
ofHoms_v

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p : ℤ
hpq : p + 0 = p
⊢ F.d p' p ≫ ψ p = F.d p' p ≫ ψ p
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i j : ι
w : ¬c.Rel j i
⊢ e.f i ≫ h.hom i j = 0

Tactic:
rw [h.zero i j w, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ 0 + e = d

Tactic:
simp only [← he, zero_add]

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

Goal state before:
pp: case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)

Tactic:
ChainComplex.next_nat_zero

Goal state after:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.down ℕ).Rel 0 0
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case h₁
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
⊢ inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

pp: case h₂
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inrX ((H.mapHomologicalComplex c).map φ) i ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

Tactic:
· by_cases hj : c.Rel j (c.next j)
        · simp [← Functor.map_comp, inlX_d _ _ _ _ _ hj, inlX_d_assoc _ _ _ _ _ hj]
        · simp [← Functor.map_comp, inlX_d' _ _ _ _ hj, inlX_d'_assoc _ _ _ _ hj]

Goal state after:
case h₂
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inrX ((H.mapHomologicalComplex c).map φ) i ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q ⋯).inv =
    (xNextIso P ⋯).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.up ℕ).prev (n✝ + 1))).snd.fst

Tactic:
mkCoinductiveAux₃ e zero comm_zero one comm_one succ

Goal state after:
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q ⋯).inv =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n✝ + 1)).fst ≫ (xPrevIso Q ⋯).hom
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ nullHomotopicMap K = π K ≫ ι₀ K - 𝟙 K.cylinder

Tactic:
ext i
  by_cases hi : c.Rel i (c.next i)
  · exact homotopyCofiber.ext_from_X (biprod.lift (𝟙 K) (-𝟙 K)) (c.next i) i hi
      (inlX_nullHomotopy_f _ _ _ _) (inrX_nullHomotopy_f _ hc _)
  · exact homotopyCofiber.ext_from_X' (biprod.lift (𝟙 K) (-𝟙 K)) _ hi (inrX_nullHomotopy_f _ hc _)

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ -Quot.mk (HomRel.CompClosure r) a✝ + Quot.mk (HomRel.CompClosure r) a✝ = 0

Tactic:
exact congr_arg (functor r).map (neg_add_cancel _)

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map
      ((shiftFunctorAdd' C (m₁ + m₂) m₃ (m₁ + m₂ + m₃) ⋯).hom.app X ≫
        (shiftFunctor C m₃).map ((shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) ⋯).hom.app X)) =
    F.map
      ((shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app X ≫
        (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯).hom.app ((shiftFunctor C m₁).obj X))
⊢ (Induced.add F s i (m₁ + m₂) m₃).hom.app (F.obj X) ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (Induced.add F s i m₁ (m₂ + m₃)).hom.app (F.obj X) ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at eq

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X ≫ (shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map
      ((shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app X ≫
        (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (Induced.add F s i (m₁ + m₂) m₃).hom.app (F.obj X) ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (Induced.add F s i m₁ (m₂ + m₃)).hom.app (F.obj X) ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ₁ γ₂ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn

Tactic:
change (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ₁ γ₂ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ (𝟙 A).hom₂ = 𝟙 A.obj₂

Tactic:
id_hom₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ 𝟙 A.obj₂ = 𝟙 A.obj₂
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ (𝟙 B).hom₂ = 𝟙 B.obj₂

Tactic:
id_hom₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ 𝟙 B.obj₂ = 𝟙 B.obj₂
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ F.map ((shiftFunctorCompIsoId C a b h).inv.app X) =
    (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).inv.app X) ≫ (commShiftIso F b).inv.app ((shiftFunctor C a).obj X)

Tactic:
by
  rw [← cancel_epi (F.map ((shiftFunctorCompIsoId C a b h).hom.app X)), ← F.map_comp,
    Iso.hom_inv_id_app, F.map_id, map_shiftFunctorCompIsoId_hom_app]
  simp only [comp_obj, id_obj, Category.assoc, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, Category.id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq =
    a.negOnePow • (δ n m γ).v p (p + m) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + m) ⋯).inv

Tactic:
δ_v n m hnm _ p (p + m) rfl (p + n) (p + 1) (by lia) rfl,

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq =
    a.negOnePow •
      (γ.v p (p + n) ⋯ ≫ L.d (p + n) (p + m) + m.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯) ≫
        (L.shiftFunctorObjXIso a q (p + m) ⋯).inv
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
⊢ ∀ (s : Fan T) (m : s.pt ⟶ (fan T).pt), (∀ (j : J), m ≫ (fan T).proj j = s.proj j) → m = lift T s.proj

Tactic:
intro s m hm

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m = lift T s.proj
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} E
inst✝¹² : Category.{v_4, u_4} J
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : D ⥤ E
τ'' : G ⟶ G'
H : E ⥤ J
A : Type u_5
inst✝¹¹ : AddMonoid A
inst✝¹⁰ : HasShift C A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
inst✝⁷ : HasShift J A
inst✝⁶ : F₁.CommShift A
inst✝⁵ : F₂.CommShift A
inst✝⁴ : F₃.CommShift A
inst✝³ : G.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : H.CommShift A
inst✝ : CommShift e.hom A
a : A
⊢ (Functor.commShiftIso F₂ a).hom ≫ Functor.whiskerRight e.inv (shiftFunctor D a) =
    (shiftFunctor C a).whiskerLeft e.inv ≫ (Functor.commShiftIso F₁ a).hom

Tactic:
by
  ext X
  dsimp
  rw [← cancel_epi (e.hom.app (X⟦a⟧)), e.hom_inv_id_app_assoc, ← shift_app_comm_assoc,
    ← Functor.map_comp, e.hom_inv_id_app, Functor.map_id, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
this : G.CommShift A := ofIso e A
⊢ NatTrans.CommShift e.hom A

Tactic:
exact ⟨fun a => by ext; simp [ofIso_commShiftIso_hom_app]⟩

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n' a : ℤ
γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ δ n (n + 1) ((↑γ).rightUnshift n hn) = 0

Tactic:
rw [Cochain.δ_rightUnshift _ n hn (n + 1) (n + 1 - a) (by lia),
      δ_eq_zero, Cochain.rightUnshift_zero, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n + a = n'
⊢ δ n' (n' + 1) ((↑γ).leftShift a n' hn') = 0

Tactic:
by
    simp only [Cochain.δ_leftShift _ a n' (n' + 1) hn' (n + 1) (by lia),
      δ_eq_zero, Cochain.leftShift_zero, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
K' : CochainComplex C ℤ
g : K' ⟶ K
⊢ equivHomShift (equivHomShift.symm (z.precomp g)) = equivHomShift (g ≫ equivHomShift.symm z)

Tactic:
by simp [equivHomShift_comp]

Goal state after: