mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ I ∈ (RingHom.ker f).minimalPrimes

Tactic:
denseRange_comap_iff_ker_le_nilRadical

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
H : RingHom.ker f ≤ nilradical R
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ I ∈ (RingHom.ker f).minimalPrimes
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ ↑n) ≤ zpowers g
⊢ zpowers (g ^ ↑n) = zpowers (g ^ n)

Tactic:
zpow_natCast

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ ↑n) ≤ zpowers g
⊢ zpowers (g ^ n) = zpowers (g ^ n)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Nat.card α / (Nat.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n

Tactic:
Nat.card_eq_fintype_card

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / (Fintype.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Tactic:
Nat.card_eq_fintype_card

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
x : α
⊢ card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)

Tactic:
by simp only [Quotient.eq'']; congr

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : Nat.card ↑(orbit G b) = p ^ k
⊢ ∃ a, ∃ (_ : a ∈ Finset.univ) (_ : ↑1 ≠ 0), Quotient.mk'' ↑a = Quotient.mk'' b

Tactic:
Nat.card_eq_fintype_card

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
⊢ ∃ a, ∃ (_ : a ∈ Finset.univ) (_ : ↑1 ≠ 0), Quotient.mk'' ↑a = Quotient.mk'' b
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : H = ⊤
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
rw [h_cop]

Goal state after:
case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : H = ⊤
h1 : Nat.card ↥H = 0
⊢ P ≤ ⊤ ∨ Disjoint ⊤ P
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : H = ⊥
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
rw [h_cop]

Goal state after:
case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : H = ⊥
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ ⊥ ∨ Disjoint ⊥ P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (↑i).cast • g = i • g

Tactic:
ZMod.coe_intCast,

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (i % ↑n) • g = i • g
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf (normalizer ↑H)) ≃ ↥H
⊢ Nat.card ↥(normalizer ↑H) ≡ Nat.card G [MOD p ^ (n + 1)]

Tactic:
rw [card_eq_card_quotient_mul_card_subgroup H,
    card_eq_card_quotient_mul_card_subgroup (H.subgroupOf (normalizer H)), Nat.card_congr this,
    hH, pow_succ']

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf (normalizer ↑H)) ≃ ↥H
⊢ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) * p ^ n ≡ Nat.card (G ⧸ H) * p ^ n [MOD p * p ^ n]
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : 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)
⊢ s * (p * p ^ n) = s * (p * p ^ n)

Tactic:
mul_comm p

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : 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)
⊢ s * (p ^ n * p) = s * (p ^ n * p)
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)
⊢ s * (p * p ^ n) = s * (p * p ^ n)

Tactic:
mul_comm p

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)
⊢ s * (p ^ n * p) = s * (p ^ n * p)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
⊢ p ∣ Nat.card ↥↑P

Tactic:
rw [← pow_one p] at hdvd

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Nat.card G
⊢ p ∣ Nat.card ↥↑P
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h : ϕ • ↑P = Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G) ϕ) ↑P
⊢ Subgroup.map ϕ.toMonoidHom ↑P = ↑P

Tactic:
rwa [← pointwise_smul_def, Subsingleton.elim (ϕ • P) P, eq_comm] at h

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ normalizer ↑↑P = ⊤

Tactic:
by
      rcases eq_top_or_exists_le_coatom (normalizer (P : Set G))
        with (heq | ⟨K, hK, hNK⟩)
      · exact heq
      · have := hnc _ hK
        have hPK : P ≤ K := le_trans le_normalizer hNK
        refine (hK.1 ?_).elim
        rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK]

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Ideal.IsMaximal (toSpanSingleton R M m).ker

Tactic:
Ideal.isMaximal_def,

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ IsCoatom (toSpanSingleton R M m).ker
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : sSupIndep s
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m

Tactic:
sSupIndep_iff

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • single R i m).coeff n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • single R i m).coeff n = if i ≤ n then q.coeff (n - i) • m else 0
⊢ ((p + q) • single R i m).coeff n = if i ≤ n then (p + q).coeff (n - i) • m else 0

Tactic:
simp [add_smul, hp, hq, ite_add_ite]

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
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | (R ∙ x).annihilator ≠ ⊥}

Tactic:
simp_rw [Submodule.ne_bot_iff, mem_annihilator, mem_span_singleton]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}
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 : I.Filtration M
i j k : ℕ
⊢ I ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
exact smul_mono_right _ (F.pow_smul_le i j)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), 0 + a = a

Tactic:
intros; ext1; simp only [add_app, zero_app, zero_add]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
hf : ∀ (i : β), IsIso (f i)
⊢ IsIso f

Tactic:
by
  change IsIso (isoMk X Y (fun i => asIso (f i))).hom
  infer_instance

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
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ 1 ⊗ₜ[R] (a * b) - (a * b) ⊗ₜ[R] 1 - (a ⊗ₜ[R] b - (a * b) ⊗ₜ[R] 1 + ((1 * b) ⊗ₜ[R] a - (a * b) ⊗ₜ[R] 1)) =
    1 ⊗ₜ[R] (a * b) - a ⊗ₜ[R] (1 * b) - ((1 * b) ⊗ₜ[R] a - (a * b) ⊗ₜ[R] 1)

Tactic:
ring_nf

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ HasLimit (pair K L ⋙ eval C c i)

Tactic:
have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)
⊢ HasLimit (pair K L ⋙ eval C c i)
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ HasColimit (pair K L ⋙ eval C c i)

Tactic:
have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)
⊢ HasColimit (pair K L ⋙ eval C c i)
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 ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ inlX φ i j hij ≫ (XIsoBiprod φ j i hij).hom = biprod.inl

Tactic:
have := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
  simp [inlX]

Goal state after:
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 ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
H : φ.f (c.next j) ≫ α.f (c.next j) = (dNext (c.next j)) hα.hom + hα.hom (c.next j) j ≫ K.d j (c.next j)
⊢ fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j) + sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j) =
    d φ j (c.next j) ≫
      if h : c.Rel (c.next j) (c.next (c.next j)) then
        fstX φ (c.next j) (c.next (c.next j)) ⋯ ≫ hα.hom (c.next (c.next j)) (c.next j) +
          sndX φ (c.next j) ≫ α.f (c.next j)
      else sndX φ (c.next j) ≫ α.f (c.next j)

Tactic:
split_ifs with hj

Goal state after:
case pos
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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
H : φ.f (c.next j) ≫ α.f (c.next j) = (dNext (c.next j)) hα.hom + hα.hom (c.next j) j ≫ K.d j (c.next j)
hj : c.Rel (c.next j) (c.next (c.next j))
⊢ fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j) + sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j) =
    d φ j (c.next j) ≫
      (fstX φ (c.next j) (c.next (c.next j)) ⋯ ≫ hα.hom (c.next (c.next j)) (c.next j) +
        sndX φ (c.next j) ≫ α.f (c.next j))

case neg
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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
H : φ.f (c.next j) ≫ α.f (c.next j) = (dNext (c.next j)) hα.hom + hα.hom (c.next j) j ≫ K.d j (c.next j)
hj : ¬c.Rel (c.next j) (c.next (c.next j))
⊢ fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j) + sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j) =
    d φ j (c.next j) ≫ sndX φ (c.next j) ≫ α.f (c.next j)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i j : ℕ
h : i + 1 = j
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom =
    (xNextIso P h).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst

Tactic:
subst j
  rcases i with (_ | _ | i) <;> simp [mkInductiveAux₂]

Goal state after:
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 ι
F G K✝ : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
K : HomologicalComplex C c
hc : ∀ (j : ι), ∃ i, c.Rel i j
x✝ : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
⊢ (fun f ↦ ⟨inr φ ≫ f, (Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯))⟩)
      ((fun x ↦
          match x with
          | ⟨α, hα⟩ => desc φ α hα)
        ⟨α, hα⟩) =
    ⟨α, hα⟩

Tactic:
rw [descSigma_ext_iff]
    cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ δ 0 1 (snd φ) = -(↑(fst φ)).comp (Cochain.ofHom φ) ⋯

Tactic:
ext p q hpq
  simp [d_snd_v φ p q hpq]

Goal state after:
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

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:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q n p' q' : ℤ
hpq' : p' + n = q'
hp : p' = p
⊢ (single 0 n).v p' q' hpq' = v 0 p' q' hpq'

Tactic:
subst hp

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
⊢ (single 0 n).v p' q' hpq' = v 0 p' q' hpq'
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b : C
f₁ f₂ : a ⟶ b
h : r f₁ f₂
⊢ (functor r).map f₁ = (functor r).map f₂

Tactic:
simpa using! Quot.sound (HomRel.CompClosure.intro _ _ (𝟙 a) f₁ f₂ (𝟙 b) h)

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

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ 0 • f = 0

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f
      dsimp [smul]
      rw [zero_smul, Functor.map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
W : Type u_3
inst✝⁴ : Category.{v_1, u_3} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : F.Additive
inst✝¹ : F.Full
inst✝ : F.Faithful
K L : HomologicalComplex V c
f₁ f₂ : K ⟶ L
H : Homotopy ((F.mapHomologicalComplex c).map f₁) ((F.mapHomologicalComplex c).map f₂)
i : ι
⊢ F.map (f₁.f i) =
    F.map ((((dNext i) fun i j ↦ F.preimage (H.hom i j)) + (prevD i) fun i j ↦ F.preimage (H.hom i j)) + f₂.f i)

Tactic:
simp [dsimp% H.comm i, dNext, prevD]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
K : CochainComplex C ℤ
⊢ ∀ (i j k : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (ComplexShape.up ℤ).Rel j k → (n.negOnePow • K.d (i + n) (j + n)) ≫ (n.negOnePow • K.d (j + n) (k + n)) = 0

Tactic:
intros
        simp only [Linear.comp_units_smul, Linear.units_smul_comp, d_comp_d, 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 a n' : ℤ
hn' : n' + a = n
⊢ rightShift 0 a n' hn' = 0

Tactic:
change rightShiftAddEquiv K L n a n' hn' 0 = 0
  apply map_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 : ℤ
γ : Cochain K L n
a : ℤ
⊢ (-γ).shift a = -γ.shift a

Tactic:
by
  change shiftAddHom K L n a (-γ) = _
  apply map_neg

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 : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
⊢ (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

Tactic:
ext p q hpq
  dsimp
  simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by lia), smul_v, Linear.comp_smul,
    smul_comm x]

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:
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.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : Mono f
X : C
g : X ⟶ X✝
h : Y✝ ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk g f h ∈ distinguishedTriangles
⊢ (Triangle.mk g f h).mor₁ ≫ 𝟙 (Triangle.mk g f h).obj₂ = 0

Tactic:
by
      rw [Triangle.mor₁_eq_zero_of_mono₂ _ hT hf, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
⊢ x₃ ≫ T.mor₃ = 0

Tactic:
← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'),

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
⊢ (x₃ ≫ T.mor₃) ≫ (shiftFunctor C 1).map φ.hom₁ = 0 ≫ (shiftFunctor C 1).map φ.hom₁