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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝² : CommGroup M
inst✝¹ : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card N)
inst✝ : IsCyclic ↥f.ker
hN : IsCyclic N
hf : Function.Surjective ⇑f
⊢ IsCyclic M

Tactic:
rw [← Subgroup.topEquiv.isCyclic, ← f.range_eq_top.mpr hf] at hN

Goal state after:
M : Type u_4
N : Type u_5
inst✝² : CommGroup M
inst✝¹ : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card N)
inst✝ : IsCyclic ↥f.ker
hN : IsCyclic ↥f.range
hf : Function.Surjective ⇑f
⊢ IsCyclic M
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ sSup u ≤ sSup {a | IsAtom a}

Tactic:
exact sSup_le_sSup hu₁

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ Nat.card G

Tactic:
hm

Goal state after:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hn : p ^ n ≤ p ^ m
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ p ^ m
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
⊢ IsUnit x

Tactic:
obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1

Goal state after:
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
⊢ IsUnit x
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
hp' : ⨆ i ∈ s, p i = ⊤
⊢ IsSemisimpleModule R M

Tactic:
simp_rw [isSemisimpleModule_iff] at hp ⊢
  refine complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'
  simpa only [← (p i).mapIic.complementedLattice_iff] using hp i hi

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ IsTorsionBySet R M s ↔ s ⊆ ↑(annihilator R M)

Tactic:
IsTorsionBySet,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0) ↔ s ⊆ ↑(annihilator R M)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_5
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
x y : PolynomialModule R M✝
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
⊢ IsScalarTower S R[X] (PolynomialModule R M)

Tactic:
by
  have : IsScalarTower R R[X] (PolynomialModule R M) :=
    inferInstanceAs <| IsScalarTower R R[X] <| Module.AEval' <| (coeffLinearEquiv R R).symm.comp <|
    (Finsupp.lmapDomain M R Nat.succ).comp (coeffLinearEquiv R R).toLinearMap
  constructor
  intro x y z
  rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : ↥((Algebra.lsmul R R M) a).invtSubmodule
⊢ ∀ (c : R[X]) {x : AEval R M a},
    x ∈ (AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid).carrier →
      c • x ∈ (AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid).carrier

Tactic:
rintro f - ⟨m : M, h : m ∈ (p : Submodule R M), rfl⟩
        simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
          AddSubmonoid.mem_map, Submodule.mem_toAddSubmonoid]
        exact ⟨aeval a f • m, aeval_apply_smul_mem_of_le_comap' h f a p.2, of_aeval_smul a f m⟩

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : Submodule R M
hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule
x : ↥p
⊢ (equiv_mapSubmodule a p hp) (LinearMap.restrict ((Algebra.lsmul R R M) a) hp • x) = X • (equiv_mapSubmodule a p hp) x

Tactic:
simp [equiv_mapSubmodule, X_smul_of]

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i

Tactic:
apply forall_congr'

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ∀ (a : ℕ), f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial (n + 1)) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
add_comm n 1,

Goal state after:
case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial (1 + n)) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
⊢ (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)

Tactic:
induction f using induction_linear with

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
a : ↑A
b : ↑B
⊢ d (a • b) = a • d b

Tactic:
rw [RingHom.smul_toAlgebra, d_mul, d_map, smul_zero, add_zero]

Goal state after:
A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
a : ↑A
b : ↑B
⊢ (CommRingCat.Hom.hom f) a • d b = a • d b
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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG ↔ F.Stable

Tactic:
by
  classical
  delta Ideal.Filtration.Stable
  simp_rw [← F.submodule_eq_span_le_iff_stable_ge]
  constructor
  · rintro H
    refine H.stabilizes_of_iSup_eq
        ⟨fun n₀ => Submodule.span _ (⋃ (i : ℕ) (_ : i ≤ n₀), single R i '' ↑(F.N i)), ?_⟩ ?_
    · intro n m e
      rw [Submodule.span_le, Set.iUnion₂_subset_iff]
      intro i hi
      refine Set.Subset.trans ?_ Submodule.subset_span
      refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_
      exact hi.trans e
    · dsimp
      rw [← Submodule.span_iUnion, ← submodule_span_single]
      simp [Set.biUnion_le_eq_iUnion]
  · rintro ⟨n, hn⟩
    rw [hn]
    simp_rw [Submodule.span_iUnion₂, ← Finset.mem_range_succ_iff, iSup_subtype']
    apply Submodule.fg_iSup
    rintro ⟨i, hi⟩
    obtain ⟨s, hs⟩ := hF' i
    have : Submodule.span (reesAlgebra I) (s.image (lsingle R i) : Set (PolynomialModule R M)) =
        Submodule.span _ (single R i '' (F.N i : Set M)) := by
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]; rfl
    rw [Subtype.coe_mk, ← this]
    exact ⟨_, rfl⟩

Goal state after:
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG

Tactic:
have := isNoetherian_of_fg_of_noetherian _ hF

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 : I.Filtration M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : IsNoetherian ↥(reesAlgebra I) ↥F.submodule
⊢ F'.submodule.FG
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j) = kernelSubobject (C.d i j')

Tactic:
← d_comp_eqToHom C r r'

Goal state after:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j' ≫ eqToHom ⋯) = kernelSubobject (C.d i j')
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
X Y : C
f : X ⟶ Y
⊢ (shiftFunctor C 0).map f = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv

Tactic:
symm
  rw [Iso.app_inv, Iso.app_hom]
  apply NatIso.naturality_2

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : Preadditive V
W : Type u_2
inst✝⁶ : Category.{v_1, u_2} W
inst✝⁵ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁴ : Category.{v_2, u_3} W₁
inst✝³ : Category.{v_3, u_4} W₂
inst✝² : HasZeroMorphisms W₁
inst✝¹ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C✝ D : HomologicalComplex V c✝
f : C✝ ⟶ D
i✝ : ι
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex W₁ c
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ F.map (C.d i j) ≫ F.map (C.d j k) = 0

Tactic:
by rw [← F.map_comp, C.d_comp_d, F.map_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
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
j : J
⊢ { f := fun i ↦ (hs i).lift ((eval C c i).mapCone t), comm' := ⋯ } ≫ s.π.app j = t.π.app j

Tactic:
by
    ext i
    apply (hs i).fac

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
n : ι
⊢ limit.π (F ⋙ eval C c n) j = limit.π (F ⋙ eval C c n) i ≫ (eval C c n).map (F.map φ)

Tactic:
← Functor.comp_map,

Goal state after:
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
n : ι
⊢ limit.π (F ⋙ eval C c n) j = limit.π (F ⋙ eval C c n) i ≫ (F ⋙ eval C c n).map φ
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
s : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
j : J
⊢ s.ι.app j ≫ { f := fun i ↦ (hs i).desc ((eval C c i).mapCocone t), comm' := ⋯ } = t.ι.app j

Tactic:
by
    ext i
    apply (hs i).fac

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
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
⊢ (∀ (x : S),
      ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
        (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x) ↔
    ∀ (x : S), ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x

Tactic:
apply forall_congr'

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
⊢ ∀ (a : S),
    ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) a =
        (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) a ↔
      ((TensorProduct.lmul' R).kerSquareLift.comp f) a = (AlgHom.id R S) a
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    ((shiftFunctorAdd' C n 0 n ⋯).inv.app X ≫ (shiftFunctorAdd' C 0 n n ⋯).hom.app X) ≫
      (shiftFunctorAdd' C 0 n n ⋯).inv.app X

Tactic:
rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]

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 : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
⊢ (eval C c n).map (F.map φ) ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i

Tactic:
← Functor.comp_map,

Goal state after:
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 : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
⊢ (F ⋙ eval C c n).map φ ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ m₂ + m₁ + m₃ = m₁ + (m₂ + m₃)

Tactic:
rw [add_comm m₂ m₁, add_assoc]

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 M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i k : ι
inst✝ : K.HasHomology i
⊢ IsLimit (KernelFork.ofι (K.iCycles i) ⋯)

Tactic:
exact (K.sc i).cyclesIsKernel

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 : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0

Tactic:
rw [K.shape _ _ h, comp_zero] at hx

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx✝ : k = x ≫ K.d i' i
hx : k = 0
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0
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 M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
hi : c.prev j = i
inst✝ : K.HasHomology j
⊢ IsColimit (CokernelCofork.ofπ (K.homologyπ j) ⋯)

Tactic:
by
  subst hi
  exact (K.sc j).homologyIsCokernel

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
j : ι
hij : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hij ≫ sndX φ j = 0

Tactic:
simp [inlX, sndX, dif_pos hij]

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 i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f = g

Tactic:
rw [← cancel_mono (XIsoBiprod φ i j hij).hom]

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
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f ≫ (XIsoBiprod φ i j hij).hom = g ≫ (XIsoBiprod φ i j hij).hom
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✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ ((dNext i) h.hom + (prevD i) h.hom + f.f i) ≫ g.f i =
    (((dNext i) fun i j ↦ h.hom i j ≫ g.f j) + (prevD i) fun i j ↦ h.hom i j ≫ g.f j) + (f ≫ g).f i

Tactic:
dNext_comp_right,

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✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ ((dNext i) h.hom + (prevD i) h.hom + f.f i) ≫ g.f i =
    ((dNext i) h.hom ≫ g.f i + (prevD i) fun i j ↦ h.hom i j ≫ g.f j) + (f ≫ g).f i
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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
F G K L : CochainComplex C ℤ
n m n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
⊢ n₁ + n₂₃ = n₁₂₃

Tactic:
by rw [← h₂₃, ← h₁₂₃, add_assoc]

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 E : HomologicalComplex V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
⊢ nullHomotopicMap hom ≫ g = nullHomotopicMap fun i j ↦ hom i j ≫ g.f j

Tactic:
by
  ext n
  dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
  simp only [Preadditive.add_comp, assoc, g.comm]

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

Goal state before:
pp: case pos
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
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

Tactic:
by_cases hj : c.Rel j (c.next j)

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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

case neg
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
hj : ¬c.Rel j (c.next j)
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j
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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
⊢ (φ ≫ inr φ).f j =
    ((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) + inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j

Tactic:
by_cases hj : c.Rel j (c.next j)

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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j =
    ((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) + inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j =
    ((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) + inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
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 φ
p : ℤ
⊢ (inr φ).f p ≫ (snd φ).v p p ⋯ = 𝟙 (G.X p)

Tactic:
simp [inr, snd]

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 φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
⊢ f = (↑(fst φ)).v j i hij ≫ (inl φ).v i j ⋯ ≫ f + (snd φ).v j j ⋯ ≫ (inr φ).f j ≫ f

Tactic:
apply ext_from φ i j hij

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

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