mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by aesop

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) = reesAlgebra I

Tactic:
by
  apply le_antisymm
  · apply Algebra.adjoin_le _
    rintro _ ⟨r, hr, rfl⟩
    exact reesAlgebra.monomial_mem.mpr (by rwa [pow_one])
  · intro p hp
    rw [p.as_sum_support]
    apply Subalgebra.sum_mem _ _
    rintro i -
    exact monomial_mem_adjoin_monomial (hp i)

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

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion ℕ M
x : M
⊢ IsOfFinAddOrder x

Tactic:
rw [isOfFinAddOrder_iff_nsmul_eq_zero]
    obtain ⟨n, hn⟩ := @h x
    exact ⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ N' ≤ N

Tactic:
· apply_fun comap (I • N).mkQ at hmaple
    simp only [comap_map_mkQ, smul_le_right, sup_of_le_right] at hmaple
    rw [hmaple]; apply le_sup_right

Goal state after:
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₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = (single R (n + 1) x).coeff (n + 1)
⊢ x ∈ I • F.N n

Tactic:
PolynomialModule.coeff_single,

Goal state after:
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₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = (Finsupp.single (n + 1) x) (n + 1)
⊢ x ∈ I • F.N n
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
R : Type u
inst✝⁴ : CommRing R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
h : Function.Surjective ⇑(lift f hf)
⊢ Function.Surjective ⇑f

pp: case refine_2
R : Type u
inst✝⁴ : CommRing R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
h : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(lift f hf)

Tactic:
· rw [← Cotangent.lift_comp_toCotangent f hf, LinearMap.coe_comp]
    exact Function.Surjective.comp h (toCotangent_surjective I)

Goal state after:
case refine_2
R : Type u
inst✝⁴ : CommRing R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
h : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(lift f hf)
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr.succ
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ x ∈ (I ^ 1 * I ^ i) • ⊤

Tactic:
← smul_smul,

Goal state after:
case mpr.succ
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ x ∈ I ^ 1 • I ^ i • ⊤
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ 0 - (TensorProduct.lmul' R) 0 ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

pp: case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ ∀ (x y : S),
    x ⊗ₜ[R] y - (TensorProduct.lmul' R) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

pp: case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ ∀ (x y : S ⊗[R] S),
    x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
      y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
        x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
· rw [map_zero, TensorProduct.zero_tmul, sub_zero]; exact zero_mem _

Goal state after:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ ∀ (x y : S),
    x ⊗ₜ[R] y - (TensorProduct.lmul' R) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ ∀ (x y : S ⊗[R] S),
    x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
      y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
        x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
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 : ι
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ F.map (d (n + 1) ≫ d n) = 0

Tactic:
sq n,

Goal state after:
ι : 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 : ι
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ F.map 0 = 0
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
i j : A
⊢ shiftFunctorComm C i j = (shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯

Tactic:
shiftFunctorAdd'_eq_shiftFunctorAdd

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorComm C i j = (shiftFunctorAdd C i j).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case pos
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
hij : c.Rel i j
⊢ K.d i j ≫ K.pOpcycles j = 0

Tactic:
obtain rfl := c.prev_eq' hij
    exact (K.sc j).f_pOpcycles

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 : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx✝ : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
⊢ K.pOpcycles i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
p_descOpcycles,

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 : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx✝ : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
⊢ k = 0
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)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
x✝ : biprod.inl.f i ≫ f = biprod.inl.f i ≫ g ∧ biprod.inr.f i ≫ f = biprod.inr.f i ≫ g
h₁ : biprod.inl.f i ≫ f = biprod.inl.f i ≫ g
h₂ : biprod.inr.f i ≫ f = biprod.inr.f i ≫ g
⊢ 𝟙 ((K ⊞ L).X i) ≫ f = 𝟙 ((K ⊞ L).X i) ≫ g

Tactic:
simp [← biprod_total_f, h₁, h₂]

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
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
n : ι
⊢ f.f n ≫ (D.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ E.dTo n) =
    C.dFrom n ≫ f.f (c.next n) ≫ hom (c.next n) n + (f.f n ≫ hom n (c.prev n)) ≫ E.dTo n

Tactic:
simp only [Preadditive.comp_add, assoc, f.comm_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 : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j ↦ dite (c.Rel j i) (h i j) fun x ↦ 0).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Tactic:
nullHomotopicMap_f_of_not_rel_left r₁₀ hk₀

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
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (dite (c.Rel k₁ k₀) (h k₀ k₁) fun x ↦ 0) ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
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 : ℤ
α β : Cochain F G n
h : ¬n + 1 = m
⊢ δ n m (α + β) = δ n m α + δ n m β

Tactic:
simp only [δ_shape _ _ h, add_zero]

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

Goal state before:
pp: 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)

Tactic:
simp only [d_sndX_assoc _ _ _ hjk, add_comp, assoc, H, dNext_eq_zero _ _ hj, zero_add]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ K.d (p + n₁ + n₂) q +
      (n₁ + n₂ + 1).negOnePow • F.d p (p + 1) ≫ (z₁.comp z₂ ⋯).v (p + 1) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫ (δ n₂ (n₂ + 1) z₂).v (p + n₁) q ⋯ +
      n₂.negOnePow • (δ n₁ (n₁ + 1) z₁).v p (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯

Tactic:
z₁.comp_v z₂ rfl (p + 1) (p + n₁ + 1) q (by lia) (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ K.d (p + n₁ + n₂) q +
      (n₁ + n₂ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫ (δ n₂ (n₂ + 1) z₂).v (p + n₁) q ⋯ +
      n₂.negOnePow • (δ n₁ (n₁ + 1) z₁).v p (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯
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:
by 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:
by 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:
by 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:
by 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
F G K : CochainComplex C ℤ
n : ℤ
f : F ⟶ G
z : Cochain G K n
m : ℤ
⊢ δ n m ((Cochain.ofHom f).comp z ⋯) = (Cochain.ofHom f).comp (δ n m z) ⋯

Tactic:
rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp]

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

Goal state before:
pp: case e_a
ι : 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 : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (fromNext i) fun i j ↦
      if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0

Tactic:
· dsimp [fromNext]
      rw [dif_pos (by simp only [CochainComplex.next])]
      simp [xNextIso, id_comp]

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 ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

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

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

Goal state before:
pp: case neg
ι✝ : 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✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel i (c.next i)
⊢ ((shortComplexFunctor C c i).obj K).g ≫ (f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) = 0

Tactic:
· dsimp
      rw [K.shape _ _ h, zero_comp]

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:
by 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:
by 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:
by 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:
by aesop

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✝
f✝ g✝ : C✝ ⟶ D
h k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
⊢ ((shortComplexFunctor C c i).map f).τ₁ =
    (((shortComplexFunctor C c i).obj K).f ≫ ho.hom i (c.prev i) +
        if c.Rel (c.prev i) i then ho.hom (c.prev i) (c.prev (c.prev i)) ≫ L.d (c.prev (c.prev i)) (c.prev i)
        else f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      ((shortComplexFunctor C c i).map g).τ₁

Tactic:
by
    dsimp
    split_ifs with h
    · rw [ho.comm (c.prev i)]
      dsimp [dFrom, dTo, fromNext, toPrev]
      rw [congr_arg (fun j => d K (c.prev i) j ≫ ho.hom j (c.prev i)) (c.next_eq' h)]
    · abel

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (x y : R) (b : T₁ ⟶ T₂), (x * y) • b = x • y • b

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (b : T₁ ⟶ T₂), 1 • b = b

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (a : R) (x y : T₁ ⟶ T₂), a • (x + y) = a • x + a • y

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (r s : R) (x : T₁ ⟶ T₂), (r + s) • x = r • x + s • x

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (x : T₁ ⟶ T₂), 0 • x = 0

Tactic:
by aesop

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
A : Type u_4
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
⊢ F.CommShift A

Tactic:
letI := hF.hasShift s i
  exact
  { commShiftIso := i
    commShiftIso_zero := by
      ext X
      simp [ShiftMkCore.shiftFunctorZero_eq]
    commShiftIso_add := fun a b => by
      ext X
      simp [ShiftMkCore.shiftFunctorAdd_eq, ShiftMkCore.shiftFunctor_eq,
        ← Functor.map_comp_assoc] }

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ CategoryTheory.shiftFunctorAdd' (Triangle C) a b (a + b) ⋯ = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
shiftFunctorAdd'_eq_shiftFunctorAdd

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ shiftFunctorAdd (Triangle C) a b = shiftFunctorAdd' C a b (a + b) ⋯