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
⊢ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = ideal R S

Tactic:
apply le_antisymm
  · rw [Ideal.span_le]
    rintro _ ⟨s, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _
  · change (KaehlerDifferential.ideal R S).restrictScalars S ≤ (Ideal.span _).restrictScalars S
    rw [← KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span]
    conv_rhs => rw [← Submodule.span_span_of_tower S]
    exact Submodule.subset_span

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i : A
⊢ (shiftFunctor C i).IsEquivalence

Tactic:
change (shiftEquiv C i).functor.IsEquivalence
  infer_instance

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

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

Tactic:
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
  rw [if_pos rfl, Category.comp_id]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d 0 1 = d₀

Tactic:
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
  rw [if_pos rfl, Category.comp_id]

Goal state after:
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)
M : HomologicalComplex C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ (biprod.lift α β ≫ biprod.fst).f i = α.f i

Tactic:
biprod.lift_fst

Goal state after:
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)
M : HomologicalComplex C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ α.f i = α.f i
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ 1 ⊗ₜ[A] (linearCombination A ⇑(D R A)) x ∈ (kerCotangentToTensor R A B).range

Tactic:
rw [← Finsupp.sum_single x, Finsupp.sum, ← Finset.sum_fiberwise_of_maps_to
      (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))]

Goal state after:
case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ 1 ⊗ₜ[A]
      (linearCombination A ⇑(D R A))
        (∑ j ∈ Finset.image (⇑(algebraMap A B)) x.support,
          ∑ i ∈ x.support with (algebraMap A B) i = j, single i (x i)) ∈
    (kerCotangentToTensor R A B).range
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case h₁
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
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ homotopyCofiber.inlX φ j i hij ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k =
    homotopyCofiber.inlX φ j i hij ≫ 0

Tactic:
simp only [comp_zero, homotopyCofiber.inlX_d_assoc φ i j k hij hjk,
        add_comp, assoc, homotopyCofiber.inrX_d, Hom.comm_assoc, neg_comp]

Goal state after:
case h₁
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
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ -F.d j k ≫ homotopyCofiber.inlX φ k j hjk ≫ homotopyCofiber.d φ j k + F.d j k ≫ φ.f k ≫ homotopyCofiber.inrX φ k = 0
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 K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
⊢ (φ ≫ inr φ).f j =
    (((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) +
        (prevD j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) +
      Hom.f 0 j

Tactic:
prevD_eq _ hij,

Goal state after:
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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
⊢ (φ ≫ inr φ).f j =
    ((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) +
        (if hij : c.Rel i j then inlX φ j i hij else 0) ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ

Tactic:
by
  obtain rfl : d = e := by lia
  rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_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 K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
φ₀ φ₁ : K ⟶ F
h : Homotopy φ₀ φ₁
⊢ biprod.lift (𝟙 K) (-𝟙 K) ≫ biprod.desc φ₀ φ₁ = φ₀ - φ₁

Tactic:
simp only [biprod.lift_desc, id_comp, neg_comp, sub_eq_add_neg]

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 ≫ (F.mapHomologicalComplex c).map h.hom)
    (𝟙 ((F.mapHomologicalComplex c).obj D))

Tactic:
by
    rw [← (F.mapHomologicalComplex c).map_comp, ← (F.mapHomologicalComplex c).map_id]
    exact F.mapHomotopy h.homotopyInvHomId

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 : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
⊢ (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

Tactic:
by
  ext p q hpq
  dsimp
  simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by lia), smul_v, Linear.comp_smul,
    smul_comm x]

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 M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq

Tactic:
comp_v _ _ (show n + m' = nm' by lia) p (p + n) q (by lia) (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    γ.v p (p + n) ⋯ ≫ (γ'.rightUnshift m' hm').v (p + n) q ⋯
Module: Mathlib.CategoryTheory.Triangulated.Rotate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ X✝.rotate.mor₃ ≫ (shiftFunctor C 1).map f.hom₂ = (shiftFunctor C 1).map f.hom₁ ≫ Y✝.rotate.mor₃

Tactic:
by
      dsimp
      simp only [comp_neg, neg_comp, ← Functor.map_comp, f.comm₁]

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
⊢ ((γ.leftShift a n' hn').rightShift a n hn').v p q hpq = ((a * n' + a * (a - 1) / 2).negOnePow • γ.shift a).v p q hpq

Tactic:
simp only [rightShift_v _ a n hn' p q hpq (q + a) (by lia),
    leftShift_v _ a n' hn' p (q + a) (by lia) (p + a) (by lia), units_smul_v, shift_v']

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 • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯) ≫
      (L.shiftFunctorObjXIso a q (q + a) ⋯).inv =
    (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₃ = 0
⊢ Epi T.mor₂

Tactic:
rw [epi_iff_cancel_zero]

Goal state after:
case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₃ = 0
⊢ ∀ (R : C) (g : T.obj₃ ⟶ R), T.mor₂ ≫ g = 0 → g = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0 → IsZero T.obj₂

Tactic:
intro ⟨h₁, h₂⟩
    obtain ⟨f, hf⟩ := coyoneda_exact₂ T hT (𝟙 _) (by rw [h₂, comp_zero])
    rw [IsZero.iff_id_eq_zero, hf, h₁, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ (mapOfHomotopy H ≫ (triangle φ₂).mor₃).f p =
    ((triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a).f p

Tactic:
dsimp [mapOfHomotopy, triangle]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ (desc φ₁
            ((Cochain.ofHom a).comp (inl φ₂) mapOfHomotopy._proof_2 +
              (Cochain.ofHomotopy H).comp (Cochain.ofHom (inr φ₂)) mapOfHomotopy._proof_3)
            (b ≫ inr φ₂) ⋯).f
        p ≫
      ((-↑(fst φ₂)).rightShift 1 0 triangle._proof_3).v p p ⋯ =
    ((-↑(fst φ₁)).rightShift 1 0 triangle._proof_3).v p p ⋯ ≫ a.f (p + 1)
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
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₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝¹ : IsIso φ'.hom₁
this✝ : IsIso φ'.hom₂
this : IsIso φ'.hom₃
⊢ productTriangle T ∈ distinguishedTriangles

Tactic:
by
    have : IsIso φ' := by
      apply Triangle.isIso_of_isIsos
      all_goals infer_instance
    exact isomorphic_distinguished _ hT' _ (asIso φ').symm

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    (mapHomologicalComplexXIso' φ G n (n + 1) ⋯).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃.f n

Tactic:
mapHomologicalComplexXIso'_hom

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    (G.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ +
        G.map ((snd φ).v n n ⋯) ≫ (inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃.f n
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
⊢ ∀ {v₁₃ : Y₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles),
    Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
v₁₃

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Y₃ ⟶ Z₁₃
⊢ ∀ {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles),
    Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.pOpcycles i ≫ K.opcyclesToCycles i j = K.toCycles i j

Tactic:
simp only [← cancel_mono (K.iCycles j), assoc, opcyclesToCycles_iCycles,
    p_fromOpcycles, toCycles_i]

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

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g'
⊢ f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p

Tactic:
apply Quiver.Path.comp_cons

Goal state after:
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map ((iso T.symm.functor R L B.symm.functor).inv.app (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)

Tactic:
simp only [Equivalence.symm_functor]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map ((iso T.inverse R L B.inverse).inv.app (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ L.map φ₀.neg.f ≫ L.map t₁ = φ.neg.map L ⋯ ≫ L.map (φ.s ≫ t₂)

Tactic:
L.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ L.map φ₀.neg.f ≫ L.map t₁ = φ.neg.map L ⋯ ≫ L.map φ.s ≫ L.map t₂
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ φ₀.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁) = φ.add.map L ⋯ ≫ L.map (φ.s ≫ t₂)

Tactic:
L.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ φ₀.add.map L ⋯ ≫ L.map φ₀.s ≫ L.map t₁ = φ.add.map L ⋯ ≫ L.map (φ.s ≫ t₂)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ φ₀.add.map L ⋯ ≫ L.map φ₀.s ≫ L.map t₁ = φ.add.map L ⋯ ≫ L.map (φ.s ≫ t₂)

Tactic:
L.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ φ₀.add.map L ⋯ ≫ L.map φ₀.s ≫ L.map t₁ = φ.add.map L ⋯ ≫ L.map φ.s ≫ L.map t₂