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

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k

Tactic:
simp_rw [isPGroup_iff_orderOf_dvd_pow, Nat.dvd_prime_pow Fact.out]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ (∀ (g : G), ∃ k, ∃ k_1 ≤ k, orderOf g = p ^ k_1) ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ g, orderOf g

Tactic:
· have := not_exists.mp h
    exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

Goal state after:
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
⊢ Module (ZMod n) M

Tactic:
have h_mod (c : ℕ) (x : M) : (c % n) • x = c • x := by
    suffices (c % n + c / n * n) • x = c • x by rwa [add_nsmul, mul_nsmul, h, add_zero] at this
    rw [Nat.mod_add_div']

Goal state after:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
h_mod : ∀ (c : ℕ) (x : M), (c % n) • x = c • x
⊢ Module (ZMod n) M
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : ↑{p | p.IsPrime ∧ ⊥ ≤ p} ≃o PrimeSpectrum R :=
  { toFun := fun x ↦ { asIdeal := ↑x, isPrime := ⋯ }, invFun := fun x ↦ ⟨x.asIdeal, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
    map_rel_iff' := ⋯ }
⊢ ↑(minimalPrimes R) ≃o (↑{s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s})ᵒᵈ

Tactic:
exact OrderIso.setOfPredMinimalIsoSetOfPredMaximal
    (e.trans ((PrimeSpectrum.pointsEquivIrreducibleCloseds R).trans
    (TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' (PrimeSpectrum R)).dual))

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm : m ≠ d ∧ m ∣ c ∧ c ≠ 0
⊢ m ∣ c

Tactic:
tauto

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : fixedPoints (↥↑P) (Sylow p G) = {P}
⊢ Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1

Tactic:
simp [this]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
⊢ orderOf g ∣ n ∨ n.Coprime (orderOf g)

Tactic:
refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
⊢ Subgroup.zpowers (g ^ n) = ⊥ → orderOf g ∣ n

case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
tG : IsMulTorsion G
x✝ : G
⊢ x✝ ∈ torsion G ↔ x✝ ∈ ⊤

Tactic:
tauto

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
⊢ StrictMono ⇑(intEquivOfZPowersEqTop g hg)

Tactic:
by
  intro x y hxy
  simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]
  exact zpow_lt_zpow_right hg1 hxy

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
by
  have hM := isCyclic_left_of_prod M N
  have hN := isCyclic_right_of_prod M N
  let _ := cyc.commGroup; let _ := hM.commGroup; let _ := hN.commGroup
  rw [IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, Nat.card_prod, lcm_eq_nat_lcm] at *
  simpa only [hM, hN, Nat.lcm_eq_mul_iff, Nat.card_pos.ne', false_or] using cyc

Goal state after:
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
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 : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
this : ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i
⊢ ↑(μ a) ∈ ⨅ (_ : i ∈ t), ⨅ (_ : i ≠ Exists.choose h), I i

Tactic:
mem_iInf,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
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 : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
this : i ∈ Finset.cons a t hat → ↑(μ a) ∈ ⨅ (_ : i ≠ a), I i
⊢ i ∈ t → ↑(μ a) ∈ ⨅ (_ : i ≠ Exists.choose h), I i
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
this : I a ⊔ ⨅ i ∈ t, I i = ⊤
⊢ ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1

Tactic:
rw [eq_top_iff_one, Submodule.mem_sup] at this

Goal state after:
case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
this : ∃ y ∈ I a, ∃ z ∈ ⨅ i ∈ t, I i, y + z = 1
⊢ ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: S : Type u_3
inst✝⁶ : Ring S
M : Type u_4
inst✝⁵ : AddCommGroup M
R : Type u_6
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
⊢ IsSimpleModule R M ↔ IsSimpleModule S M

Tactic:
by
  rw [isSimpleModule_iff, isSimpleModule_iff,
    (Submodule.orderIsoOfAlgebraMapSurjective h).isSimpleOrder_iff]

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
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : ↥m ≃ₗ[R] N := (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
⊢ ∃ h, f ∘ₗ h = g

Tactic:
refine ⟨Submodule.subtype _ ∘ₗ e.symm.toLinearMap ∘ₗ g, LinearMap.ext fun x ↦ ?_⟩

Goal state after:
R : Type u_2
inst✝⁷ : Ring R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : ↥m ≃ₗ[R] N := (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
x : P
⊢ (f ∘ₗ m.subtype ∘ₗ ↑e.symm ∘ₗ g) x = g x
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : torsionOf R M 0 = ⊥
contra : m = 0
⊢ False

Tactic:
torsionOf_zero

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : ⊤ = ⊥
contra : m = 0
⊢ False
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
⊢ r = 0

Tactic:
tauto

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
x✝ : M
h : 1 • x✝ = 0
⊢ x✝ ∈ ⊥

Tactic:
one_smul

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ ⊥
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ 1 • n ∈ I • N

Tactic:
one_smul

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ n ∈ I • N
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : x ∈ torsionBySet R M ↑(⨅ i ∈ S, p i)
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
⊢ 1 • x = x

Tactic:
one_smul

Goal state after:
case a.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : x ∈ torsionBySet R M ↑(⨅ i ∈ S, p i)
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
⊢ x = x
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
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ Disjoint ((fun i ↦ torsionBySet R M ↑(p i)) i) (T.sup fun i ↦ torsionBySet R M ↑(p i))

Tactic:
by
  rw [disjoint_iff, Finset.sup_eq_iSup,
    iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij]
  have := GaloisConnection.u_inf
    (b₁ := OrderDual.toDual (p i)) (b₂ := OrderDual.toDual (⨅ i ∈ T, p i)) (torsion_gc R M)
  dsimp at this ⊢
  rw [← this, Ideal.sup_iInf_eq_top, top_coe, torsionBySet_univ]
  intro j hj; apply hp hi (hT hj); rintro rfl; exact hiT hj

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
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = torsionBySet R M ↑(R ∙ ∏ i ∈ S, q i)

Tactic:
Ideal.submodule_span_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = torsionBySet R M ↑(Ideal.span {∏ i ∈ S, q i})
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M ↑(R ∙ ∏ i ∈ S, q i)
⊢ DirectSum.IsInternal fun i ↦ torsionBy R M (q ↑i)

Tactic:
Ideal.submodule_span_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M ↑(Ideal.span {∏ i ∈ S, q i})
⊢ DirectSum.IsInternal fun i ↦ torsionBy R M (q ↑i)
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ map N.mkQ N' ≤ I • map N.mkQ N'

Tactic:
by rw [← map_smul'', this]

Goal state after:
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.map (ρ_ n).inv).app X ≫ (δ F n (𝟙_ M)).app X

Tactic:
rw [map_rightUnitor_inv]

Goal state after:
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)).inv ≫ F.obj n ◁ ε F ≫ μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M)).app X
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : ↑(r ⁻¹' {q (p i)})), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ c'.inj ⟨p i, ⋯⟩ ≫ m =
    Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫
      c'.inj ⟨p i, ⋯⟩ ≫ Cofan.IsColimit.desc hc' fun x ↦ Cofan.IsColimit.desc (hc ↑x ⋯) fun x_1 ↦ s.inj ⟨↑x_1, ⋯⟩

Tactic:
rw [Cofan.IsColimit.fac, Cofan.IsColimit.fac, ← hm]

Goal state after:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : ↑(r ⁻¹' {q (p i)})), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ c'.inj ⟨p i, ⋯⟩ ≫ m =
    Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') ⟨↑⟨i, ⋯⟩, ⋯⟩ ≫ m
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i = j
⊢ ((single V c j).obj A).X i = A

Tactic:
by subst hi; simp [single]

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
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd C a 0).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X) ≫ eqToHom ⋯

Tactic:
simp [← shiftFunctorAdd'_add_zero_inv_app, shiftFunctorAdd']

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✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' + m = n'

Tactic:
rw [add_assoc, hm, add_zero]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
⊢ ((Functor.const J).obj
            { X := fun n ↦ limit (F ⋙ eval C c n),
              d := fun n m ↦ limMap { app := fun j ↦ (F.obj j).d n m, naturality := ⋯ }, shape := ⋯,
              d_comp_d' := ⋯ }).map
        φ ≫
      { f := fun x ↦ limit.π (F ⋙ eval C c x) j, comm' := ⋯ } =
    { f := fun x ↦ limit.π (F ⋙ eval C c x) i, comm' := ⋯ } ≫ F.map φ

Tactic:
by
        ext n
        dsimp
        simp only [Category.id_comp]
        rw [← eval_map, ← Functor.comp_map, limit.w]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : Epi (φ.f i)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ ¬c.Rel i (c.next i)

Tactic:
tauto

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
j : ι
inst✝² : K.HasHomology j
inst✝¹ : L.HasHomology j
inst✝ : Mono (φ.f j)
hj : ∀ (i : ι), ¬c.Rel i j
⊢ ¬c.Rel (c.prev j) j

Tactic:
tauto

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 : 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:
by
  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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ d φ i j ≫ fstX φ j k hjk = -fstX φ i j hij ≫ F.d j k

Tactic:
obtain rfl := c.next_eq' hjk

Goal state after:
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 i j
hjk : c.Rel j (c.next j)
⊢ d φ i j ≫ fstX φ j (c.next j) hjk = -fstX φ i j hij ≫ F.d j (c.next j)
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✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ ((dNext i) hom + (prevD i) hom) ≫ D.d i j = C.d i j ≫ ((dNext j) hom + (prevD j) hom)

Tactic:
dNext_eq hom hij,

Goal state after:
ι : 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✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ (C.d i j ≫ hom j i + (prevD i) hom) ≫ D.d i j = C.d i j ≫ ((dNext j) hom + (prevD j) 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 ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j k : ι
hjk : c.Rel j k
⊢ (if hj : c.Rel j (c.next j) then fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j
      else sndX φ j ≫ α.f j) ≫
      K.d j k =
    (homotopyCofiber φ).d j k ≫
      if hj : c.Rel k (c.next k) then fstX φ k (c.next k) hj ≫ hα.hom (c.next k) k + sndX φ k ≫ α.f k
      else sndX φ k ≫ α.f k

Tactic:
obtain rfl := c.next_eq' hjk

Goal state after:
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)
⊢ (if hj : c.Rel j (c.next j) then fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j
      else sndX φ j ≫ α.f j) ≫
      K.d j (c.next j) =
    (homotopyCofiber φ).d j (c.next j) ≫
      if hj : c.Rel (c.next j) (c.next (c.next j)) then
        fstX φ (c.next j) (c.next (c.next j)) hj ≫ 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)
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 : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
by
  simp only [nullHomotopicMap']
  rw [nullHomotopicMap_f r₂₁ r₁₀]
  split_ifs
  rfl

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

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
A : C
f : A ⟶ (mappingCone φ).X i
⊢ f ≫ (↑(fst φ)).v i j hij = f ≫ (↑(fst φ)).v i j hij ∧ f ≫ (snd φ).v i i ⋯ = f ≫ (snd φ).v i i ⋯

Tactic:
tauto

Goal state after:
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 : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₀ = 0

Tactic:
by
  dsimp [nullHomotopicMap, dNext, prevD]
  rw [C.shape, D.shape, zero_comp, comp_zero, add_zero] <;> apply_assumption

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

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : j + 1 = i
A : C
f : (mappingCone φ).X j ⟶ A
⊢ (inl φ).v i j ⋯ ≫ f = (inl φ).v i j ⋯ ≫ f ∧ (inr φ).f j ≫ f = (inr φ).f j ≫ f

Tactic:
tauto

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 k : ι
hjk : c.Rel j k
⊢ (desc φ α hα).f j = fstX φ j k hjk ≫ hα.hom k j + sndX φ j ≫ α.f j

Tactic:
obtain rfl := c.next_eq' hjk

Goal state after:
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)
⊢ (desc φ α hα).f j = fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j