mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • x ∈ R ∙ a * b
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

Tactic:
Submodule.mem_span_singleton

Goal state after:
case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • (a * b) = a • x
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) 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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
⊢ D.tensorProductTo (x * y) =
    (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_

Goal state after:
case refine_1
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
D : Derivation R S M
x y : S ⊗[R] S
⊢ D.tensorProductTo (0 * y) =
    (TensorProduct.lmul' R) 0 • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo 0

case refine_2
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
D : Derivation R S M
x y : S ⊗[R] S
⊢ ∀ (x y_1 : S),
    D.tensorProductTo (x ⊗ₜ[R] y_1 * y) =
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y_1) • D.tensorProductTo y +
        (TensorProduct.lmul' R) y • D.tensorProductTo (x ⊗ₜ[R] y_1)

case refine_3
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
D : Derivation R S M
x y : S ⊗[R] S
⊢ ∀ (x y_1 : S ⊗[R] S),
    D.tensorProductTo (x * y) =
        (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x →
      D.tensorProductTo (y_1 * y) =
          (TensorProduct.lmul' R) y_1 • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y_1 →
        D.tensorProductTo ((x + y_1) * y) =
          (TensorProduct.lmul' R) (x + y_1) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x + y_1)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫
      (h.add (m₁ + m₂) m₃).inv.app X ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫
      (h.add m₁ (m₂ + m₃)).inv.app X ≫
        eqToHom ⋯ ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫
      (h.add m₁ (m₂ + m₃)).inv.app X ≫
        eqToHom ⋯ ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X)) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫
      (h.add m₁ (m₂ + m₃)).inv.app X ≫ (h.add m₁ (m₂ + m₃)).hom.app X ≫ (h.add m₂ m₃).hom.app ((h.F m₁).obj X)

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X)) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₂ m₃).hom.app ((h.F m₁).obj X)
Module: Mathlib.RingTheory.Kaehler.Basic

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

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_

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

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.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯ ≫ eqToHom ⋯
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 : ℕ
eq :
  (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst =
    eqToHom ⋯ ≫
      (succ
            { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), 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 + 2) (n + 1),
              g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 3) (n + 2) = (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst

Tactic:
dsimp only [mk, of, of.d]

Goal state after:
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 : ℕ
eq :
  (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst =
    eqToHom ⋯ ≫
      (succ
            { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), 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 + 2) (n + 1),
              g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
⊢ (if h : n + 3 = n + 2 + 1 then eqToHom ⋯ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).g else 0) =
    (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst
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
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) =
    (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X) ≫
      (shiftFunctorComm C n 0).inv.app X ≫
        (shiftFunctorComm C n 0).hom.app X ≫ (shiftFunctor C n).map ((shiftFunctorZero C A).hom.app X)

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) =
    (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X) ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).hom.app X)
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: case pos
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
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ PreservesColimitsOfShape J (single C c i ⋙ eval C c j)

pp: case neg
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
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
h : ¬j = i
⊢ PreservesColimitsOfShape J (single C c i ⋙ eval C c j)

Tactic:
· subst h
      exact preservesColimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm

Goal state after:
case neg
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
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
h : ¬j = i
⊢ PreservesColimitsOfShape J (single C c i ⋙ eval C c j)
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))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
        (shiftFunctor D m₃).map ((i (m₁ + m₂)).inv.app X) ≫
          (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
            (i m₃).hom.app ((s (m₁ + m₂)).obj X) ≫
              (shiftFunctor D m₃).map ((i (m₁ + m₂)).hom.app X) ≫
                (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) ≫
                  (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X) ≫ (i m₂).inv.app ((s m₁).obj X)) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))

Tactic:
Iso.inv_hom_id_app_assoc,

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))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
        (shiftFunctor D m₃).map ((i (m₁ + m₂)).inv.app X) ≫
          (shiftFunctor D m₃).map ((i (m₁ + m₂)).hom.app X) ≫
            (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) ≫
              (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X) ≫ (i m₂).inv.app ((s m₁).obj X)) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))
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)
⊢ (map R R A B).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker

Tactic:
rw [ker_map, ← kerTotal_map' R A B h, Submodule.comap_map_eq, Submodule.map_sup,
    Submodule.map_sup, ← kerTotal_eq, ← Submodule.comap_bot,
    Submodule.map_comap_eq_of_surjective (linearCombination_surjective _ _),
    bot_sup_eq, Submodule.map_span, ← Set.range_comp]

Goal state after:
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)
⊢ Submodule.span A (Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x ↦ single ((algebraMap R A) x) 1)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
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 k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ K.homologyπ j ≫ (K.homologyIsoSc' i j k hi hk).hom = (K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyπ

Tactic:
apply ShortComplex.homologyπ_naturality

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 j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).homologyπ ≫ (K.homologyIsoSc' i j k hi hk).inv = (K.cyclesIsoSc' i j k hi hk).inv ≫ K.homologyπ j

Tactic:
apply ShortComplex.homologyπ_naturality

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 j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.homologyIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyι = K.homologyι j ≫ (K.opcyclesIsoSc' i j k hi hk).hom

Tactic:
apply ShortComplex.homologyι_naturality

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 j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.homologyIsoSc' i j k hi hk).inv ≫ K.homologyι j = (K.sc' i j k).homologyι ≫ (K.opcyclesIsoSc' i j k hi hk).inv

Tactic:
apply ShortComplex.homologyι_naturality

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{v_3, u_3} E₁
inst✝ : Category.{v_4, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f)

Tactic:
rw [isIso_prod_iff]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{v_3, u_3} E₁
inst✝ : Category.{v_4, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F

Tactic:
by
  constructor
  · intro h X Y f hf
    have : IsIso (G.map (F.map f)) := h _ hf
    exact isIso_of_reflects_iso (F.map f) G
  · intro hF
    exact IsInvertedBy.of_comp W F hF G

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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
⊢ p + n = p + n + 1 - 1

Tactic:
add_sub_cancel_right

Goal state after:
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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
⊢ p + n = p + n
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 : ι
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)
n : ℕ
I : (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) :=
  mkInductiveAux₁ e zero one comm_one succ n
⊢ e.f (n + 1) = dFrom P (n + 1) ≫ (xNextIso P ⋯).hom ≫ I.fst + (I.snd.fst ≫ (xPrevIso Q ⋯).inv) ≫ dTo Q (n + 1)

Tactic:
simpa using! I.2.2

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ ↑z ∈ cocycle F G n

Tactic:
exact z.2

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 : ι
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''
n : ℕ
I : (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' :=
  mkCoinductiveAux₁ e zero one comm_one succ n
⊢ e.f (n + 1) = (I.fst ≫ (xPrevIso Q ⋯).inv) ≫ dTo Q (n + 1) + dFrom P (n + 1) ≫ (xNextIso P ⋯).hom ≫ I.snd.fst

Tactic:
simpa using! I.2.2

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

Goal state before:
pp: case right
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (H.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ +
        H.map ((snd φ).v n n ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫
      ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
          ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ).f (n + 1) +
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫
          ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj G).d n (n + 1)) =
    ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
      (H.map ((↑(fst φ)).v (n + 1) (n + 2) ⋯) ≫
            (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 2) (n + 1) ⋯ +
          H.map ((snd φ).v (n + 1) (n + 1) ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
dsimp
      simp only [comp_add, add_comp, assoc, inl_v_fst_v_assoc, inr_f_fst_v_assoc,
        Functor.mapHomologicalComplex_obj_X, zero_comp, comp_zero, add_zero, inl_v_snd_v_assoc,
        inr_f_snd_v_assoc, zero_add, inl_v_snd_v, inr_f_snd_v, comp_id, ← H.map_comp,
        d_snd_v φ n (n + 1) rfl, Functor.map_add]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f✝ : X ⟶ Y
f g : X.as ⟶ Y.as
⊢ HomRel.CompClosure r f g → Quot.mk (HomRel.CompClosure r) (-f) = Quot.mk (HomRel.CompClosure r) (-g)

Tactic:
by
      intro hfg
      simp only [HomRel.compClosure_iff_self] at hfg
      erw [functor_map_eq_iff]
      apply Congruence.equivalence.symm
      convert! hr f g _ _ hfg (Congruence.equivalence.refl (-f - g)) using 1 <;> abel

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X