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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Function.Surjective (mapSurjective hf)

Tactic:
by
  have : Finite G' := Finite.of_surjective f hf
  intro P
  let Q₀ : Sylow p (P.comap f) := Sylow.nonempty.some
  let Q : Subgroup G := Q₀.map (P.comap f).subtype
  have hPQ : Q.map f ≤ P := Subgroup.map_le_iff_le_comap.mpr (Subgroup.map_subtype_le Q₀.1)
  have hpQ : IsPGroup p Q := Q₀.2.map (P.comap f).subtype
  have hQ : ¬ p ∣ Q.index := by
    rw [Subgroup.index_map_subtype Q₀.1, P.index_comap_of_surjective hf]
    exact Nat.Prime.not_dvd_mul Fact.out Q₀.not_dvd_index P.not_dvd_index
  use hpQ.toSylow hQ
  rw [Sylow.ext_iff, Sylow.coe_mapSurjective, eq_comm]
  exact ((hpQ.map f).toSylow (fun h ↦ hQ (h.trans (Q.index_map_dvd hf)))).3 P.2 hPQ

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
m : M
x✝ : m ∈ (AddCommGroup.torsion M).carrier
n : ℕ
hn : n > 0
hn' : n • m = 0
⊢ r • n • m = 0

Tactic:
simp only [hn', smul_zero]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
⊢ ((p : ↥ps) → (P : Sylow (↑p) G) → ↥P) ≃* G

Tactic:
have : ∀ p, Fintype (P p) := fun p ↦ Fintype.ofFinite (P p)

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
⊢ ((p : ↥ps) → (P : Sylow (↑p) G) → ↥P) ≃* G
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ s.toFun i ∈ eraseLast s

Tactic:
have hi : (i : ℕ) < (s.length - 1).succ := by
    conv_rhs => rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
      Nat.add_one_sub_one]
    exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [last, s.inj, Fin.ext_iff] using hx)

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
hi : ↑i < (s.length - 1).succ
⊢ s.toFun i ∈ eraseLast s
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hR : IsSemisimpleRing R
hS : IsSemisimpleRing S
this✝ : Module (R × S) R := Module.compHom R (RingHom.fst R S)
this : Module (R × S) S := Module.compHom S (RingHom.snd R S)
_e₁ : R →ₛₗ[RingHom.fst R S] R :=
  let __src := AddMonoidHom.id R;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing (R × S)

Tactic:
let _e₂ : S →ₛₗ[.snd R S] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hR : IsSemisimpleRing R
hS : IsSemisimpleRing S
this✝ : Module (R × S) R := Module.compHom R (RingHom.fst R S)
this : Module (R × S) S := Module.compHom S (RingHom.snd R S)
_e₁ : R →ₛₗ[RingHom.fst R S] R :=
  let __src := AddMonoidHom.id R;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : S →ₛₗ[RingHom.snd R S] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing (R × S)
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
q : Submodule R[X] (AEval R M a)
x✝ : AEval R M a
⊢ x✝ ∈
      (fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
        ((fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩) q) ↔
    x✝ ∈ q

Tactic:
aesop

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 p' : ↥((Algebra.lsmul R R M) a).invtSubmodule
h : p ≤ p'
x : AEval R M a
hx :
  x ∈
    {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      p
⊢ x ∈
    {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      p'

Tactic:
aesop

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

Goal state before:
pp: case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
⊢ c • Submodule.Quotient.mk (a • b) = 0

Tactic:
(Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _,

Goal state after:
case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
⊢ c • 0 = 0
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
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
n₀ : ℕ
⊢ (∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))) →
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

pp: case mpr
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
n₀ : ℕ
⊢ (∀ n ≥ n₀, I • F.N n = F.N (n + 1)) →
    ∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
· intro H n hn
    refine (F.smul_le n).antisymm ?_
    intro x hx
    obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp (H _ ⟨x, hx, rfl⟩)
    replace hl := congr_arg (fun f : PolynomialModule R M => f.coeff (n + 1)) hl
    rw [PolynomialModule.coeff_single, Finsupp.single_apply, if_pos rfl] at hl
    rw [← hl, Finsupp.linearCombination_apply, PolynomialModule.coeff_finsuppSum, Finsupp.sum_apply]
    apply Submodule.sum_mem _ _
    rintro ⟨_, _, ⟨n', rfl⟩, _, ⟨hn', rfl⟩, m, hm, rfl⟩ -
    dsimp only [Subtype.coe_mk]
    rw [Subalgebra.smul_def, smul_single_apply, if_pos (show n' ≤ n + 1 by lia)]
    have e : n' ≤ n := by lia
    have := F.pow_smul_le_pow_smul (n - n') n' 1
    rw [tsub_add_cancel_of_le e, pow_one, add_comm _ 1, ← add_tsub_assoc_of_le e, add_comm] at this
    exact this (Submodule.smul_mem_smul ((l _).2 <| n + 1 - n') hm)

Goal state after:
case mpr
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
n₀ : ℕ
⊢ (∀ n ≥ n₀, I • F.N n = F.N (n + 1)) →
    ∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
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:
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.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S S' : ShortComplex V
h : S = S'
⊢ (succ S).snd.fst = eqToHom ⋯ ≫ (succ S').snd.fst ≫ eqToHom ⋯

Tactic:
by
  subst h
  simp

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
    { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1 + 1), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
      X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1 + 1) (n + 1),
      g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }

Tactic:
simp [mk, mkAux]

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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
⊢ x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))

Tactic:
rw [KaehlerDifferential.span_range_derivation]

Goal state after:
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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
⊢ x ∈ ⊤
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
X Y : V
f g : X ⟶ Y
h : f = g
⊢ (succ' f).snd.fst = eqToHom ⋯ ≫ (succ' g).snd.fst

Tactic:
by
  subst h
  simp

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✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ (((shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X)) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X) =
    (((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
          (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
            (shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X)

Tactic:
simp only [Category.assoc, Iso.hom_inv_id_app]

Goal state after:
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
⊢ (shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫
      (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X) ≫
          (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X) =
    (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
        𝟙 ((shiftFunctor C m₁ ⋙ shiftFunctor C m₃).obj ((shiftFunctor C m₂).obj X)) ≫
          (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X)
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
x : S
⊢ (x𝖣1) = 0

Tactic:
← (algebraMap R S).map_one,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (x𝖣(algebraMap R S) 1) = 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 : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
⊢ K.d i j ≫ K.pOpcycles j = 0

Tactic:
by_cases hij : c.Rel i j
  · obtain rfl := c.prev_eq' hij
    exact (K.sc j).f_pOpcycles
  · rw [K.shape _ _ hij, zero_comp]

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

Goal state before:
pp: case a.tmul
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
r : B
s : Ω[A⁄R]
⊢ (mapBaseChange R A B) (r ⊗ₜ[A] s) ∈ (map R A B B).ker

Tactic:
obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s

Goal state after:
case a.tmul
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
r : B
x : A →₀ A
⊢ (mapBaseChange R A B) (r ⊗ₜ[A] (linearCombination A ⇑(D R A)) x) ∈ (map R A B B).ker
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : Ω[A⁄R]
hx :
  x ∈
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ (LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B)) ((TensorProduct.lid A Ω[A⁄R]).symm x) ∈
    (kerCotangentToTensor R A B).range

Tactic:
obtain ⟨x, hx, rfl⟩ := hx

Goal state after:
case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ (LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B))
      ((TensorProduct.lid A Ω[A⁄R]).symm ((linearCombination A ⇑(D R A)) x)) ∈
    (kerCotangentToTensor R A B).range
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Function.Surjective ⇑(mapBaseChange R A B)

Tactic:
have := subsingleton_of_surjective A B h
  rw [← LinearMap.range_eq_top, range_mapBaseChange, ← top_le_iff]
  exact fun x _ ↦ Subsingleton.elim _ _

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₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ C.d k₀ (c.next k₀) ≫ hom (c.next k₀) k₀ + hom k₀ k₁ ≫ D.d k₁ k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

Tactic:
C.shape,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ 0 ≫ hom (c.next k₀) k₀ + hom k₀ k₁ ≫ D.d k₁ k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)
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
⊢ C.d k₀ (c.next k₀) ≫ hom (c.next k₀) k₀ + hom k₀ (c.prev k₀) ≫ D.d (c.prev k₀) k₀ = 0

Tactic:
C.shape,

Goal state after:
ι : 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
⊢ 0 ≫ hom (c.next k₀) k₀ + hom k₀ (c.prev k₀) ≫ D.d (c.prev k₀) k₀ = 0

case a
ι : 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
⊢ ¬c.Rel k₀ (c.next k₀)
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 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))

Tactic:
simp only [comp_add, d_sndX_assoc _ _ _ hjk, add_comp, assoc, H,
        d_fstX_assoc _ _ _ _ hjk, neg_comp, dNext, AddMonoidHom.mk'_apply]

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) =
    -fstX φ j (c.next j) hjk ≫ F.d (c.next j) (c.next (c.next j)) ≫ hα.hom (c.next (c.next j)) (c.next j) +
      (fstX φ j (c.next j) hjk ≫ F.d (c.next j) (c.next (c.next j)) ≫ hα.hom (c.next (c.next j)) (c.next j) +
          fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j ≫ K.d j (c.next j) +
        sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j))
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case hnc
ι : 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 : 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 : ℕ
w : ¬(ComplexShape.down ℕ).Rel j i
⊢ ¬i + 1 = j

Tactic:
exact w

Goal state after:
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 : ℤ
x✝ : Cocycle F G n
⊢ 1 • x✝ = x✝

Tactic:
aesop

Goal state after:
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 : ℤ
x✝ : R
⊢ x✝ • 0 = 0

Tactic:
aesop

Goal state after:
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 : ℤ
x✝² : R
x✝¹ x✝ : Cocycle F G n
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
aesop

Goal state after:
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 : ℤ
⊢ ∀ (x : Cocycle F G n), 0 • x = 0

Tactic:
aesop

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 : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0

Tactic:
CochainComplex.prev_nat_zero

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

Goal state before:
pp: case hnc
ι : 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''
i j : ℕ
w : ¬(ComplexShape.up ℕ).Rel j i
⊢ ¬j + 1 = i

Tactic:
exact w

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 φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 0 = q
⊢ (lift φ α β eq).f p ≫ (snd φ).v p q hpq = β.v p q hpq

Tactic:
by
  obtain rfl : q = p := by lia
  simp [lift]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C✝ : Type u_1
inst✝² : Category.{v_1, u_1} C✝
r : HomRel C✝
C : Type u_2
D : Type u_3
inst✝¹ : Category.{v_2, u_2} C
inst✝ : Category.{v_3, u_3} D
F : C ⥤ D
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z}, F.homRel g g' → F.homRel (f ≫ g) (f ≫ g')

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C✝ : Type u_1
inst✝² : Category.{v_1, u_1} C✝
r : HomRel C✝
C : Type u_2
D : Type u_3
inst✝¹ : Category.{v_2, u_2} C
inst✝ : Category.{v_3, u_3} D
F : C ⥤ D
⊢ ∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z), F.homRel f f' → F.homRel (f ≫ g) (f' ≫ g)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C✝ : Type u_1
inst✝² : Category.{v_1, u_1} C✝
r : HomRel C✝
C : Type u_2
D : Type u_3
inst✝¹ : Category.{v_2, u_2} C
inst✝ : Category.{v_3, u_3} D
F : C ⥤ D
X✝ Y✝ : C
⊢ ∀ {x y : X✝ ⟶ Y✝}, F.homRel x y → F.homRel y x

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C✝ : Type u_1
inst✝² : Category.{v_1, u_1} C✝
r : HomRel C✝
C : Type u_2
D : Type u_3
inst✝¹ : Category.{v_2, u_2} C
inst✝ : Category.{v_3, u_3} D
F : C ⥤ D
X✝ Y✝ : C
⊢ ∀ {x y z : X✝ ⟶ Y✝}, F.homRel x y → F.homRel y z → F.homRel x z

Tactic:
aesop

Goal state after: