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 : ↥((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:
by
        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.Basic

Goal state before:
pp: case pos
ι : 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
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ r.coeff (i - n) * a = (r * (monomial n) a).coeff i

Tactic:
rw [show i = (i - n) + n by lia, Polynomial.coeff_mul_monomial]

Goal state after:
case pos
ι : 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
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ r.coeff (i - n + n - n) * a = r.coeff (i - n) * a
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ : (map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • (map R' f✝) f
e₂ : (map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) g
⊢ (map R' f✝) (p • (f + g)) = Polynomial.map (algebraMap R R') p • (map R' f✝) (f + g)

Tactic:
| add f g e₁ e₂ =>

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

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ : (eval r) (p • f) = Polynomial.eval r p • (eval r) f
e₂ : (eval r) (p • g) = Polynomial.eval r p • (eval r) g
⊢ (eval r) (p • (f + g)) = Polynomial.eval r p • (eval r) (f + g)

Tactic:
| add f g e₁ e₂ =>

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

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
r : R
f g : PolynomialModule R M
e₁ : (eval ((algebraMap R R') r)) ((map R' f✝) f) = f✝ ((eval r) f)
e₂ : (eval ((algebraMap R R') r)) ((map R' f✝) g) = f✝ ((eval r) g)
⊢ (eval ((algebraMap R R') r)) ((map R' f✝) (f + g)) = f✝ ((eval r) (f + g))

Tactic:
| add f g e₁ e₂ =>

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

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

Tactic:
| add f g e₁ e₂ =>

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
this : pOrder hM (s i) ≤ pOrder hM (s (oj.get hoj))
⊢ p ^ pOrder hM (s (oj.get hoj)) • s i = 0

Tactic:
rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case smul₁
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
r✝ : R
m✝ : M
mem✝ : m✝ ∈ r • P
h : m✝ ∈ N
⊢ r✝ • m✝ ∈ N

Tactic:
exact N.smul_mem _ h

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
⊢ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i)) = F.submodule.toAddSubmonoid

Tactic:
by
  apply le_antisymm
  · rw [AddSubmonoid.closure_le, Set.iUnion_subset_iff]
    rintro i _ ⟨m, hm, rfl⟩ j
    rw [coeff_single, Finsupp.single_apply]
    split_ifs with h
    · rwa [← h]
    · exact (F.N j).zero_mem
  · intro f hf
    rw [← f.ofCoeff_coeff, ← f.coeff.sum_single, ofCoeff_finsuppSum]
    apply AddSubmonoid.sum_mem _ _
    rintro c -
    exact AddSubmonoid.subset_closure (Set.subset_iUnion _ c <| Set.mem_image_of_mem _ (hf c))

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
⊢ x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x

Tactic:
by
  let N := (⨅ i : ℕ, I ^ i • ⊤ : Submodule R M)
  have hN : ∀ k, (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N :=
    fun k => inf_eq_right.mpr ((iInf_le _ k).trans <| le_of_eq <| by simp)
  constructor
  · obtain ⟨r, hr₁, hr₂⟩ :=
      Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I N (IsNoetherian.noetherian N) (by
        obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
        have := hk k (le_refl _)
        rw [hN, hN] at this
        exact le_of_eq this.symm)
    intro H
    exact ⟨⟨r, hr₁⟩, hr₂ _ H⟩
  · rintro ⟨r, eq⟩
    rw [Submodule.mem_iInf]
    intro i
    induction i with
    | zero => simp
    | succ i hi =>
      rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]
      exact Submodule.smul_mem_smul r.prop hi

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
⊢ 1 - ↑r - 1 ∈ ⊥.jacobson

Tactic:
simpa using h r.2

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (m x : ↑(R.obj X)),
    (ConcreteCategory.hom (R.map f)) (m • x) = (RingHom.id ↑(R.obj X)) m • (ConcreteCategory.hom (R.map f)) x

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
⊢ comapEq C ⋯ = (comapEq C h).symm

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g h : β → γ
k : f = g
l : g = h
⊢ comapEq C ⋯ = comapEq C k ≪≫ comapEq C l

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
⊢ (fun b ↦ b + 0 • s) = id

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
X : GradedObject I C
p : I → J
inst✝ : X.HasMap p
⊢ mapMap (𝟙 X) p = 𝟙 (X.mapObj p)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
ψ : Y ⟶ Z
p : I → J
inst✝² : X.HasMap p
inst✝¹ : Y.HasMap p
inst✝ : Z.HasMap p
⊢ mapMap (φ ≫ ψ) p = mapMap φ p ≫ mapMap ψ p

Tactic:
by cat_disch

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
m n : M
h₁ : m ⊗ n ≅ 𝟙_ M
h₂ : n ⊗ m ≅ 𝟙_ M
H : h₁.hom ▷ m ≫ (λ_ m).hom = (α_ m n m).hom ≫ m ◁ h₂.hom ≫ (ρ_ m).hom
inst✝ : F.Monoidal
X : C
⊢ (F.obj m).map ((unitOfTensorIsoUnit F m n h₁).inv.app X) ≫
      (μ F n m).app ((F.obj m).obj X) ≫ (F.map h₂.hom).app ((F.obj m).obj X) ≫ (η F).app ((F.obj m).obj X) =
    𝟙 ((F.obj m).obj X)

Tactic:
simp only [μ_naturalityᵣ_assoc, μ_naturalityₗ_assoc, η_app_obj, Category.assoc,
      obj_μ_inv_app, Functor.map_comp, δ_μ_app_assoc, obj_ε_app,
      unitOfTensorIsoUnit_inv_app]

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
m n : M
h₁ : m ⊗ n ≅ 𝟙_ M
h₂ : n ⊗ m ≅ 𝟙_ M
H : h₁.hom ▷ m ≫ (λ_ m).hom = (α_ m n m).hom ≫ m ◁ h₂.hom ≫ (ρ_ m).hom
inst✝ : F.Monoidal
X : C
⊢ (F.map (λ_ m).inv).app X ≫
      (F.map (h₁.inv ▷ m)).app X ≫
        (F.map (α_ m n m).hom).app X ≫ (F.map (m ◁ h₂.hom)).app X ≫ (F.map (ρ_ m).hom).app X =
    𝟙 ((F.obj m).obj X)
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:
subst hi

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
A : V
i : ι
⊢ ((single V c i).obj A).X i = A
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₁ C₂ : HomologicalComplex V c
⊢ Function.Injective fun f ↦ f.f

Tactic:
by cat_disch

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

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
hi : i = j
⊢ ((singleObjXIsoOfEq c j A i hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv) ≫ K.d i k = 0

Tactic:
subst hi

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i k : ι
hik : c.Rel i k
φ : A ⟶ K.X i
hφ : ∀ (k : ι), c.Rel i k → φ ≫ K.d i k = 0
⊢ ((singleObjXIsoOfEq c i A i ⋯).hom ≫ φ ≫ (K.XIsoOfEq ⋯).inv) ≫ K.d i k = 0
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₂ a₃ : A
X : C
⊢ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).app X ≫
      (LaxMonoidal.μ (shiftMonoidalFunctor C A) (MonoidalCategoryStruct.tensorObj { as := a₁ } { as := a₂ })
              { as := a₃ }).app
          X ≫
        eqToHom ⋯ ≫
          (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
                  (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
              X ≫
            (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
              (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    (eqToHom ⋯ ≫ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X) ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
        (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)

Tactic:
δ_μ_app_assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
              (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
          X ≫
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    (eqToHom ⋯ ≫ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X) ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
        (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
φ : C ⟶ (single₀ V).obj X
⊢ (fun f ↦ HomologicalComplex.mkHomToSingle ↑f ⋯) ((fun φ ↦ ⟨φ.f 0, ⋯⟩) φ) = φ

Tactic:
by cat_disch

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
⊢ Function.LeftInverse (fun f ↦ HomologicalComplex.mkHomFromSingle f ⋯) fun f ↦ f.f 0

Tactic:
by cat_disch

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
⊢ Function.RightInverse (fun f ↦ HomologicalComplex.mkHomFromSingle f ⋯) fun f ↦ f.f 0

Tactic:
by cat_disch

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
φ : (single₀ V).obj X ⟶ C
⊢ (fun f ↦ HomologicalComplex.mkHomFromSingle ↑f ⋯) ((fun φ ↦ ⟨φ.f 0, ⋯⟩) φ) = φ

Tactic:
by cat_disch

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
⊢ Function.RightInverse (fun f ↦ HomologicalComplex.mkHomFromSingle ↑f ⋯) fun φ ↦ ⟨φ.f 0, ⋯⟩

Tactic:
by cat_disch

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
⊢ Function.LeftInverse (fun f ↦ HomologicalComplex.mkHomToSingle f ⋯) fun f ↦ f.f 0

Tactic:
by cat_disch

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
⊢ Function.RightInverse (fun f ↦ HomologicalComplex.mkHomToSingle f ⋯) fun f ↦ f.f 0

Tactic:
by cat_disch

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 : ι
⊢ Hom.f 0 = 0

Tactic:
by cat_disch

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 : ι
⊢ ∀ (x y : C ⟶ D), (x + y).f = x.f + y.f

Tactic:
by cat_disch

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 : ι
⊢ ∀ (x : C ⟶ D), (-x).f = -x.f

Tactic:
by cat_disch

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 : ι
⊢ ∀ (x y : C ⟶ D), (x - y).f = x.f - y.f

Tactic:
by cat_disch

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 : ι
⊢ ∀ (x : C ⟶ D) (n : ℕ), (n • x).f = n • x.f

Tactic:
by cat_disch

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 : ι
⊢ ∀ (x : C ⟶ D) (n : ℤ), (n • x).f = n • x.f

Tactic:
by cat_disch

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 : V ⥤ W
inst✝² : F.Additive
c : ComplexShape ι
inst✝¹ : F.Faithful
inst✝ : F.Full
X Y : HomologicalComplex V c
f : (F.mapHomologicalComplex c).obj X ⟶ (F.mapHomologicalComplex c).obj Y
⊢ (F.mapHomologicalComplex c).map { f := fun n ↦ F.preimage (f.f n), comm' := ⋯ } = f

Tactic:
by cat_disch

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

Goal state before:
pp: ι : Type u_1
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 ι
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
⊢ mapHomologicalComplex (𝟙 F) c = 𝟙 (F.mapHomologicalComplex c)

Tactic:
by cat_disch

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

Goal state before:
pp: case succ
ι : Type u_1
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
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').X (n + 1 + 2) ≅
    (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1 + 1) (n + 1))).fst

Tactic:
· exact mkXIso _ _ _ _ _ (succ' d₀).2.2 (fun S => succ' S.f) n

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
a : X ⟶ Y
⊢ 1 • a = a

Tactic:
by cat_disch

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by cat_disch

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
⊢ ∀ (a : R) (x y : X ⟶ Y), a • (x + y) = a • x + a • y

Tactic:
by cat_disch

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
⊢ ∀ (x : X ⟶ Y), 0 • x = 0

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
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
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ F.map ((add hF s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ (add hF s i m₁ (m₂ + m₃)).hom.app X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))

Tactic:
← cancel_mono ((i m₃).hom.app ((s m₂).obj ((s m₁).obj X)))

Goal state after:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
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
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ F.map ((add hF s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) ≫
      (i m₃).hom.app ((s m₂).obj ((s m₁).obj X)) =
    F.map (eqToHom ⋯ ≫ (add hF s i m₁ (m₂ + m₃)).hom.app X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X)) ≫
      (i m₃).hom.app ((s m₂).obj ((s m₁).obj 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
a : S
⊢ ∀ (b : S), ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a

Tactic:
b

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
⊢ ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a