mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⊗[R] S
hx✝ : x ∈ ideal R S
hx : x ∈ Submodule.restrictScalars S (ideal R S)
⊢ (fromIdeal R S) ⟨x, hx✝⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
← KaehlerDifferential.submodule_span_range_eq_ideal

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx✝ : x ∈ ideal R S
hx : x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ (fromIdeal R S) ⟨x, hx✝⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ (n + 1) ⟶ X✝ n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ (n + 1) ⟶ Y✝ n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
X Y : ChainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f (i + 1) ≫ Y.d (i + 1) i = X.d (i + 1) i ≫ f i
n m : α
⊢ (ComplexShape.down α).Rel n m → f n ≫ Y.d n m = X.d n m ≫ f m

Tactic:
simp only [ComplexShape.down_Rel]

Goal state after:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ (n + 1) ⟶ X✝ n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ (n + 1) ⟶ Y✝ n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
X Y : ChainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f (i + 1) ≫ Y.d (i + 1) i = X.d (i + 1) i ≫ f i
n m : α
⊢ m + 1 = n → f n ≫ Y.d n m = X.d n m ≫ f m
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 ≫
        𝟙
          { 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 := ⋯ }.X₁
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 3) (n + 2) =
    (mkXIso X₀ X₁ X₂ d₀ d₁ s succ n).hom ≫
      (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

Tactic:
comp_id

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
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 3) (n + 2) =
    (mkXIso X₀ X₁ X₂ d₀ d₁ s succ n).hom ≫
      (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
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ limit.π (F ⋙ eval C c n) j ≫ (F.obj j).d n m = 0 ≫ limit.π (F ⋙ eval C c m) j

Tactic:
(F.obj j).shape _ _ h,

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ limit.π (F ⋙ eval C c n) j ≫ 0 = 0 ≫ limit.π (F ⋙ eval C c m) j
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ (F.obj j).d n m ≫ colimit.ι (F ⋙ eval C c m) j = colimit.ι (F ⋙ eval C c n) j ≫ 0

Tactic:
(F.obj j).shape _ _ h,

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ 0 ≫ colimit.ι (F ⋙ eval C c m) j = colimit.ι (F ⋙ eval C c n) j ≫ 0
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
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
a : S
ha : a ∈ EssFiniteType.finset R S
⊢ ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight) a =
    ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft) a

Tactic:
simp only [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq,
        Function.comp_apply, TensorProduct.includeLeft_apply, TensorProduct.includeRight_apply,
        Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
a : S
ha : a ∈ EssFiniteType.finset R S
⊢ 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ I
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 y z : S
⊢ (z𝖣x + y) = (kerTotal R S).mkQ (single x z + single y z)

Tactic:
eq_comm,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ (kerTotal R S).mkQ (single x z + single y z) = z𝖣x + y
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 y z : S
⊢ (z𝖣x * y) = (kerTotal R S).mkQ (single y (z * x) + single x (z * y))

Tactic:
eq_comm,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ (kerTotal R S).mkQ (single y (z * x) + single x (z * y)) = z𝖣x * y
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)
i : ι
⊢ biprod.inl.f i ≫ biprod.fst.f i = 𝟙 (K.X i)

Tactic:
by
  rw [← comp_f, biprod.inl_fst, id_f]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
⊢ nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun i j hij ↦ hom i j hij ≫ g.f j

Tactic:
by
  rw [nullHomotopicMap', nullHomotopicMap_comp]
  congr
  ext i j
  split_ifs
  · rfl
  · rw [zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ 𝟙 (X ((H.mapHomologicalComplex c).map φ) i) =
    inrX ((H.mapHomologicalComplex c).map φ) i

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
⊢ inrX ((H.mapHomologicalComplex c).map φ) i = inrX ((H.mapHomologicalComplex c).map φ) i
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ f ≫ 𝟙 (L.X q) = f

pp: case hc
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ p = p ∧ q = q

Tactic:
comp_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ f = f

case hc
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ p = p ∧ q = q
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
φ₀ φ₁ : K ⟶ F
h : Homotopy φ₀ φ₁
⊢ ι₀ K ≫ desc φ₀ φ₁ h = φ₀

Tactic:
simp [ι₀, desc]

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
i j : ι
hij : c.Rel j i
hj : ∃ k, c.Rel k j
⊢ inlX K i j hij ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inlX K i j hij ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
obtain ⟨k, hjk⟩ := hj
    simp only [assoc, Homotopy.nullHomotopicMap'_f hjk hij, homotopyCofiber_d,
      homotopyCofiber.d_sndX_assoc _ _ _ hij, add_comp, comp_add, homotopyCofiber.inlX_fstX_assoc,
      homotopyCofiber.inlX_sndX_assoc, zero_comp, add_zero, comp_sub, inlX_π_assoc, comp_id,
      zero_sub, ← HomologicalComplex.comp_f_assoc, biprod.lift_snd, neg_f_apply, id_f,
      neg_comp, id_comp]

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

Goal state before:
pp: case e_a.e_a.succ
ι : 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✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ eqToHom ⋯ =
    ((mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ eqToHom ⋯) ≫ 𝟙 (xPrev Q (n✝ + 1))

Tactic:
comp_id

Goal state after:
case e_a.e_a.succ
ι : 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✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ eqToHom ⋯ =
    (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ eqToHom ⋯
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✝ : ι
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : F.Additive
f g : C ⟶ D
h : Homotopy f g
i : ι
H : f.f i = C.d i (c.next i) ≫ h.hom (c.next i) i + h.hom i (c.prev i) ≫ D.d (c.prev i) i + g.f i
⊢ F.map (f.f i) =
    F.map (C.d i (c.next i)) ≫ F.map (h.hom (c.next i) i) + F.map (h.hom i (c.prev i)) ≫ F.map (D.d (c.prev i) i) +
      F.map (g.f i)

Tactic:
simp [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✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : F.Additive
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ ((F.mapHomologicalComplex c).map f).f i =
    (((dNext i) fun i j ↦ F.map (h.hom i j)) + (prevD i) fun i j ↦ F.map (h.hom i j)) +
      ((F.mapHomologicalComplex c).map g).f i

Tactic:
by
    have H := h.comm i
    dsimp [dNext, prevD] at H ⊢
    simp [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 g : C ⟶ D
h✝ k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : F.Additive
h : HomotopyEquiv C D
⊢ Homotopy ((F.mapHomologicalComplex c).map (h.inv ≫ h.hom)) ((F.mapHomologicalComplex c).map (𝟙 D))

Tactic:
exact F.mapHomotopy h.homotopyInvHomId

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
G : Type u_2
inst✝ : Groupoid G
r : HomRel G
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as), Quotient.inv r (Quot.mk (HomRel.CompClosure r) a) ≫ Quot.mk (HomRel.CompClosure r) a = 𝟙 Y✝

Tactic:
by simp [CategoryStruct.comp, CategoryStruct.id]

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
G : Type u_2
inst✝ : Groupoid G
r : HomRel G
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as), Quot.mk (HomRel.CompClosure r) a ≫ Quotient.inv r (Quot.mk (HomRel.CompClosure r) a) = 𝟙 X✝

Tactic:
by simp [CategoryStruct.comp, CategoryStruct.id]

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
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ functor r ⋙ lift r F H = F

Tactic:
by
  tauto

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

Goal state before:
pp: case pos
ι✝ : 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)
⊢ f.f (c.next i) =
    K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

Tactic:
ho.comm (c.next i)

Goal state after:
case pos
ι✝ : 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)
⊢ (dNext (c.next i)) ho.hom + (prevD (c.next i)) ho.hom + g.f (c.next i) =
    K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
by
  tauto

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
⊢ ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
by
  tauto

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f p ≫
      ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app K).f p =
    (XIsoOfEq K ⋯).hom

Tactic:
shiftFunctorAdd'_inv_app_f',

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app K).f p =
    (XIsoOfEq K ⋯).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
n : ℤ
X✝ Y✝ : HomologicalComplex C (ComplexShape.up ℤ)
x✝ : X✝ ⟶ Y✝
i✝ : ℤ
⊢ F.map (x✝.f (i✝ + n)) ≫ 𝟙 (F.obj (Y✝.X (i✝ + n))) = F.map (x✝.f (i✝ + n))

Tactic:
comp_id

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
n : ℤ
X✝ Y✝ : HomologicalComplex C (ComplexShape.up ℤ)
x✝ : X✝ ⟶ Y✝
i✝ : ℤ
⊢ F.map (x✝.f (i✝ + n)) = F.map (x✝.f (i✝ + n))
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
e : A ≅ B := A.isoMk B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃) ⋯ ⋯ ⋯
⊢ IsIso f

Tactic:
exact (inferInstance : IsIso e.hom)

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

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
f g h : T₁ ⟶ T₂
⊢ (f + g + h).hom₁ = (f + (g + h)).hom₁

Tactic:
apply add_assoc

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

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
f g h : T₁ ⟶ T₂
⊢ (f + g + h).hom₂ = (f + (g + h)).hom₂

Tactic:
apply add_assoc

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

Goal state before:
pp: case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
f g h : T₁ ⟶ T₂
⊢ (f + g + h).hom₃ = (f + (g + h)).hom₃

Tactic:
apply add_assoc

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

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
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
⊢ n' + m = t'

Tactic:
← ht',

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
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
⊢ n' + m = t + a
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
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ (T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫ (Limits.Pi.map fun j ↦ (T j).mor₃) ≫ 𝟙 (∏ᶜ fun j ↦ (shiftFunctor C 1).obj (T j).obj₁)

Tactic:
comp_id

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ (T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫ Limits.Pi.map fun j ↦ (T j).mor₃
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
this : HasShift C A := hF.hasShift s i
a b : A
X : C
⊢ (i (a + b)).hom.app X = (isoAdd (i a) (i b)).hom.app X

Tactic:
simp [ShiftMkCore.shiftFunctorAdd_eq, ShiftMkCore.shiftFunctor_eq,
        ← Functor.map_comp_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯ ≫ 𝟙 (L.X (q + a)) =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯

Tactic:
comp_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯ =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯