mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.restrictScalars R (Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s)) =
      Submodule.restrictScalars R ⊤ ↔
    Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤

Tactic:
Submodule.restrictScalars_span

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span R (⇑(maximalIdeal R).toCotangent '' s) = Submodule.restrictScalars R ⊤ ↔
    Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤

case hsur
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Function.Surjective ⇑(algebraMap R (ResidueField R))
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
j : ι
hj : ∀ (k : ι), ¬c.Rel j k
⊢ ¬∃ j_1, c.Rel j j_1

Tactic:
by simpa using hj

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
h₁ h₂ : d.Universal
this : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d'
⊢ h₁ = h₂

Tactic:
cases h₁

Goal state after:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
h₂ : d.Universal
desc✝ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝ d') = d'
postcomp_injective✝ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
this :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ),
    { desc := desc✝, fac := fac✝, postcomp_injective := postcomp_injective✝ }.desc d' = h₂.desc d'
⊢ { desc := desc✝, fac := fac✝, postcomp_injective := postcomp_injective✝ } = h₂
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
J : Type u_4
inst✝ : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
⊢ e.inv j ≫ e.hom j = 𝟙 (Y j)

Tactic:
by
  rw [← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id]

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
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
⊢ f = g

Tactic:
ext i
  by_cases h : i = j
  · subst h
    exact hfg
  · apply (isZero_single_obj_X c j A i h).eq_of_tgt

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✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
rw [← h₂₃, ← add_assoc, h₁₂₃]

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✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
rw [← h₂₃, ← add_assoc, h₁₂₃]

Goal state after:
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
⊢ Submodule.span S (Set.range ⇑(D R S)) = ⊤

Tactic:
rw [_root_.eq_top_iff]
  rintro x -
  obtain ⟨⟨x, hx⟩, rfl⟩ := fromIdeal_surjective R S x
  rw [← Submodule.restrictScalars_mem S, ← KaehlerDifferential.submodule_span_range_eq_ideal] at hx
  suffices ∃ hx,
      fromIdeal R S ⟨x, hx⟩ ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) from
    this.snd
  -- TODO: this proof looks like we're reinventing `Submodule.span_le`.
  -- I'm not sure what's the RHS here though.
  refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
  · rintro _ ⟨x, rfl⟩
    refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩
    apply Submodule.subset_span
    exact ⟨x, KaehlerDifferential.DLinearMap_apply R S x⟩
  · exact ⟨zero_mem _, Submodule.zero_mem _⟩
  · rintro x y - - ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩; exact ⟨add_mem hx₁ hy₁, Submodule.add_mem _ hx₂ hy₂⟩
  · rintro r x - ⟨hx₁, hx₂⟩
    exact ⟨((KaehlerDifferential.ideal R S).restrictScalars S).smul_mem r hx₁,
      Submodule.smul_mem _ r hx₂⟩

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✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ (shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X) =
    (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
        (shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)

Tactic:
rw [← cancel_mono ((shiftFunctorComm C m₁ m₃).inv.app (X⟦m₂⟧)),
    ← cancel_mono (((shiftFunctorComm C m₁ m₂).inv.app X)⟦m₃⟧')]

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ (((shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X)) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X) =
    (((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
          (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
            (shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app 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
x y z : S
⊢ (z𝖣x + y) = (z𝖣x) + z𝖣y

Tactic:
rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

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

Tactic:
rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single y (z * x) + single x (z * y) - single (x * y) z ∈ kerTotal R S
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hk : ¬c.Rel k (c.next k)
⊢ -F.d j k ≫ homotopyCofiber.inlX φ k j hjk ≫ homotopyCofiber.d φ j k + F.d j k ≫ φ.f k ≫ homotopyCofiber.inrX φ k = 0

Tactic:
· simp [homotopyCofiber.inlX_d' φ j k hjk hk]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ LiftCommShift.iso F r hF 0 = Functor.CommShift.isoZero (lift r F hF) A

Tactic:
ext1
    apply natTrans_ext
    ext X
    dsimp
    rw [LiftCommShift.iso_hom_app, (functor r).commShiftIso_zero,
      Functor.CommShift.isoZero_hom_app, Functor.CommShift.isoZero_inv_app,
      Functor.map_comp, assoc, F.commShiftIso_zero, Functor.CommShift.isoZero_hom_app,
      lift_map_functor_map, ← F.map_comp_assoc, Iso.inv_hom_id_app]
    dsimp [lift_obj_functor_obj]
    rw [F.map_id, id_comp]

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 : ℤ
K' : CochainComplex C ℤ
g : K' ⟶ K
f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
⊢ equivHomShift (g ≫ f) = (equivHomShift f).precomp g

Tactic:
by
  ext p q hpq
  simp [equivHomShift_apply, Cochain.rightUnshift_v _ _ _ _ _ _ _ (add_zero p)]

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
⊢ δ (-1) 0 0 = Cochain.ofHom (inr φ ≫ (triangle φ).mor₃)

Tactic:
by simp only [δ_zero, inr_triangleδ, Cochain.ofHom_zero]

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
n : ℤ
⊢ n + 1 + -1 = n

Tactic:
by simp only [add_neg_cancel_right]

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

Goal state before:
pp: case refine_1
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₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ g_1, g ≫ Pi.π (fun j ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
⊢ f = 0

Tactic:
let α := fun j => (hg'' j).choose

Goal state after:
case refine_1
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₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ g_1, g ≫ Pi.π (fun j ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ := fun j ↦ ⋯.choose
⊢ f = 0
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: case refine_5
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C
u₁₂' : X₁' ⟶ X₂'
u₂₃' : X₂' ⟶ X₃'
u₁₃' : X₁' ⟶ X₃'
comm' : u₁₂' ≫ u₂₃' = u₁₃'
e₁ : X₁ ≅ X₁'
e₂ : X₂ ≅ X₂'
e₃ : X₃ ≅ X₃'
comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂'
comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ u₂₃'
v₁₂' : X₂' ⟶ Z₁₂'
w₁₂' : Z₁₂' ⟶ (shiftFunctor C 1).obj X₁'
h₁₂' : Triangle.mk u₁₂' v₁₂' w₁₂' ∈ distinguishedTriangles
v₂₃' : X₃' ⟶ Z₂₃'
w₂₃' : Z₂₃' ⟶ (shiftFunctor C 1).obj X₂'
h₂₃' : Triangle.mk u₂₃' v₂₃' w₂₃' ∈ distinguishedTriangles
v₁₃' : X₃' ⟶ Z₁₃'
w₁₃' : Z₁₃' ⟶ (shiftFunctor C 1).obj X₁'
h₁₃' : Triangle.mk u₁₃' v₁₃' w₁₃' ∈ distinguishedTriangles
H : Octahedron comm' h₁₂' h₂₃' h₁₃'
iso₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ≅ Triangle.mk u₁₂' v₁₂' w₁₂' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂
iso₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ≅ Triangle.mk u₂₃' v₂₃' w₂₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃
iso₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ≅ Triangle.mk u₁₃' v₁₃' w₁₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯
eq₁₂ :
  v₁₂ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂).hom.hom₃ =
    e₂.hom ≫ v₁₂'
eq₁₂' :
  w₁₂ ≫ (shiftFunctor C 1).map e₁.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂).hom.hom₃ ≫ w₁₂'
eq₁₃ :
  v₁₃ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯).hom.hom₃ =
    e₃.hom ≫ v₁₃'
eq₁₃' :
  w₁₃ ≫ (shiftFunctor C 1).map e₁.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯).hom.hom₃ ≫ w₁₃'
eq₂₃ :
  v₂₃ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃).hom.hom₃ =
    e₃.hom ≫ v₂₃'
eq₂₃' :
  w₂₃ ≫ (shiftFunctor C 1).map e₂.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃).hom.hom₃ ≫ w₂₃'
rel₁₂ : v₁₂' ≫ H.m₁ = u₂₃' ≫ v₁₃'
rel₁₃ : w₁₂' = H.m₁ ≫ w₁₃'
rel₂₂ : v₁₃' ≫ H.m₃ = v₂₃'
rel₂₃ : w₁₃' ≫ (shiftFunctor C 1).map u₁₂' = H.m₃ ≫ w₂₃'
⊢ (w₂₃ ≫ (shiftFunctor C 1).map v₁₂) ≫ (shiftFunctor C 1).map iso₁₂.hom.hom₃ =
    iso₂₃.hom.hom₃ ≫ w₂₃' ≫ (shiftFunctor C 1).map v₁₂'

Tactic:
rw [assoc, ← Functor.map_comp, eq₁₂, Functor.map_comp, reassoc_of% eq₂₃']

Goal state after:
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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ e',
    e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom ∧
      e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
⊢ T₁ ≅ T₂

Tactic:
let e := h.choose

Goal state after:
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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ e',
    e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom ∧
      e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
e : T₁.invRotate ≅ T₂.invRotate := h.choose
⊢ T₁ ≅ T₂
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 L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map ((iso B L.inverse R.inverse T).inv.app (L.functor.obj X)) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (iso T L.functor R.functor B).hom.app X

Tactic:
vInv_iso_inv_app

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 L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (iso T L.functor R.functor B).hom.app X
Module: Mathlib.CategoryTheory.Localization.Predicate

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
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₁
⊢ L₂.IsLocalization W

Tactic:
MorphismProperty.IsInvertedBy.iff_of_iso W e

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
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
⊢ L₂.IsLocalization W
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (T₁ × T₂) κ

Tactic:
rw [hasCardinalLT_iff_cardinal_mk_lt] at h₁ h₂ ⊢

Goal state after:
T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : Cardinal.mk T₁ < κ
h₂ : Cardinal.mk T₂ < κ
⊢ Cardinal.mk (T₁ × T₂) < κ
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
E : Type u_3
inst✝¹ : Category.{v_2, u_3} E
inst✝ : HasShift E A
⊢ ∀ {X Y : C} (x : X ≅ Y), P.shiftClosure A X → P.shiftClosure A Y

Tactic:
by
    rintro X Y i ⟨Z, a, i', hZ⟩
    exact ⟨Z, a, i.symm.trans i', hZ⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : { X' := X₂, s := z₁.s, hs := ⋯, f := z₂.f }.f ≫ z₁₂.s = { X' := X₂, s := z₁.s, hs := ⋯, f := z₂.f }.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : { X' := X₃, s := z₂.s, hs := ⋯, f := z₃.f }.f ≫ z₂₃.s = { X' := X₃, s := z₂.s, hs := ⋯, f := z₃.f }.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac :
  { X' := z₂.Y', s := z₁₂.s, hs := ⋯, f := z₂₃.f }.f ≫ z'.s = { X' := z₂.Y', s := z₁₂.s, hs := ⋯, f := z₂₃.f }.s ≫ z'.f
⊢ (z₁.comp z₂).comp (Hom.mk z₃) = (Hom.mk z₁).comp (z₂.comp z₃)

Tactic:
dsimp at fac₁₂ fac₂₃ fac

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ (z₁.comp z₂).comp (Hom.mk z₃) = (Hom.mk z₁).comp (z₂.comp z₃)
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasShift D ℤ
inst✝⁹ : Preadditive D
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁷ : Pretriangulated D
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.IsHomological
X₁ X₂ : C
this✝ : HasBinaryBiproduct (F.obj X₁) (F.obj X₂)
Z : A
S : ShortComplex A := { X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := biprod.inl, g := biprod.snd, zero := ⋯ }.map F
this : Mono S.f
ex : S.Exact
g : Z ⟶ S.X₁
hf : g = 0
⊢ g ≫ F.map biprod.inl = 0

Tactic:
rw [hf, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ → LeftFractionRel φ ψ

Tactic:
intro h
    rw [← MorphismProperty.LeftFraction.Localization.map_eq_iff]
    apply map_eq_of_map_eq _ _ _ _ h

Goal state after: