mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⟶ X✝ (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ n ⟶ Y✝ (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
X Y : CochainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f i ≫ Y.d i (i + 1) = X.d i (i + 1) ≫ f (i + 1)
n : α
⊢ f n ≫ Y.d n (n + 1) = X.d n (n + 1) ≫ f (n + 1)

Tactic:
simpa using comm n

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

Goal state before:
pp: case mp
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
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (G.map (F.map f))
⊢ IsIso (F.map f)

Tactic:
exact isIso_of_reflects_iso (F.map f) G

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case h
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
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ ∑ x_1 ∈ {i ∈ x.support | (algebraMap A B) i = c}.attach, x ↑x_1 • 1 ⊗ₜ[A] ((D R A) ↑x_1 - (D R A) a) =
    1 ⊗ₜ[A] ∑ x_1 ∈ x.support with (algebraMap A B) x_1 = c, x x_1 • (D R A) x_1

Tactic:
simp_rw [← TensorProduct.tmul_smul]

Goal state after:
case h
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
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ ∑ x_1 ∈ {i ∈ x.support | (algebraMap A B) i = c}.attach, 1 ⊗ₜ[A] (x ↑x_1 • ((D R A) ↑x_1 - (D R A) a)) =
    1 ⊗ₜ[A] ∑ x_1 ∈ x.support with (algebraMap A B) x_1 = c, x x_1 • (D R A) x_1
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 n₂ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
m₂ : ℤ
h₂ : n₂ + 1 = m₂
⊢ n₂ + 1 = m₂

Tactic:
h₂

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 n₂ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
m₂ : ℤ
h₂ : n₂ + 1 = m₂
⊢ m₂ = m₂
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
L : C ⥤ D
inst✝ : L.Full
⊢ ∀ {X Y : Quotient L.homRel}, Function.Surjective (Quotient.lift L.homRel L ⋯).map

Tactic:
rintro ⟨X⟩ ⟨Y⟩ (f : L.obj X ⟶ L.obj Y)

Goal state after:
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
L : C ⥤ D
inst✝ : L.Full
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ a, (Quotient.lift L.homRel L ⋯).map a = f
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.hom ≫ (quotient V c).map f.inv = 𝟙 ((quotient V c).obj C)

Tactic:
by
    rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
    exact eq_of_homotopy _ _ f.homotopyHomInvId

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

Goal state before:
pp: case mpr
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ Nonempty (Homotopy (𝟙 C) 0) → 𝟙 ((quotient V c).obj C) = 0

Tactic:
· rintro ⟨h⟩
    simpa using (eq_of_homotopy _ _ h)

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

Goal state before:
pp: case e_a
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₂
a b : A
X : C
⊢ (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
      (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
        F.map ((shiftFunctorAdd C a b).inv.app X) ≫
          F.map ((shiftFunctorAdd C a b).hom.app X) ≫
            (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
              (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫
                (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
      (shiftFunctor D b).map
          ((lift r F hF).map ((Functor.commShiftIso (functor r) a).inv.app X) ≫ (Functor.commShiftIso F a).hom.app X) ≫
        (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
rw [← cancel_epi ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map
      (NatTrans.app (Functor.commShiftIso (functor r) a).hom X))]

Goal state after:
case e_a
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₂
a b : A
X : C
⊢ (shiftFunctor (Quotient r) b ⋙ lift r F hF).map ((Functor.commShiftIso (functor r) a).hom.app X) ≫
      (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
        (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
          F.map ((shiftFunctorAdd C a b).inv.app X) ≫
            F.map ((shiftFunctorAdd C a b).hom.app X) ≫
              (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
                (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫
                  (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (shiftFunctor (Quotient r) b ⋙ lift r F hF).map ((Functor.commShiftIso (functor r) a).hom.app X) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map
            ((lift r F hF).map ((Functor.commShiftIso (functor r) a).inv.app X) ≫
              (Functor.commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))
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✝
n a n' : ℤ
hn' : n' + a = n
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
⊢ (fun γ ↦ γ.rightShift a n' hn') ((fun γ ↦ γ.rightUnshift n hn') γ) = γ

Tactic:
simp only [rightShift_rightUnshift]

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
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).leftShift a n' hn').v p q hpq = x • (γ.leftShift a n' hn').v p q hpq

Tactic:
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.CategoryTheory.Triangulated.Basic

Goal state before:
pp: 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
n : ℕ
f : T₁ ⟶ T₂
⊢ Int.negSucc n • f = -(↑n.succ • f)

Tactic:
ext <;> apply SubNegMonoid.zsmul_neg'

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) ⋯).inv) ≫
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L).d (p + n') q +
      m'.negOnePow • K.d p (p + 1) ≫ (γ.rightShift a n' hn').v (p + 1) q ⋯ =
    a.negOnePow •
      (γ.v p (p + n) ⋯ ≫ L.d (p + n) (p + m) + m.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯) ≫
        (L.shiftFunctorObjXIso a q (p + m) ⋯).inv

Tactic:
γ.rightShift_v a n' hn' (p + 1) q _ (p + m) (by lia)

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) ⋯).inv) ≫
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L).d (p + n') q +
      m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + m) ⋯).inv =
    a.negOnePow •
      (γ.v p (p + n) ⋯ ≫ L.d (p + n) (p + m) + m.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯) ≫
        (L.shiftFunctorObjXIso a q (p + m) ⋯).inv
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
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} D₁
inst✝²¹ : Category.{v_5, u_5} D₂
inst✝²⁰ : Category.{v_6, u_6} D₃
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : D₁ ⥤ D₂
G₂₃ : D₂ ⥤ D₃
G₁₃ : D₁ ⥤ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃
A : Type u_7
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : HasShift C₁ A
inst✝¹⁷ : HasShift C₂ A
inst✝¹⁶ : HasShift C₃ A
inst✝¹⁵ : HasShift D₁ A
inst✝¹⁴ : HasShift D₂ A
inst✝¹³ : HasShift D₃ A
inst✝¹² : F₁₂.CommShift A
inst✝¹¹ : F₂₃.CommShift A
inst✝¹⁰ : F₁₃.CommShift A
inst✝⁹ : CommShift α A
inst✝⁸ : G₁₂.CommShift A
inst✝⁷ : G₂₃.CommShift A
inst✝⁶ : G₁₃.CommShift A
inst✝⁵ : CommShift β A
inst✝⁴ : L₁.CommShift A
inst✝³ : L₂.CommShift A
inst✝² : L₃.CommShift A
inst✝¹ : CommShift e₁₂ A
inst✝ : CommShift e₂₃ A
h₁₃ :
  e₁₃ =
    Functor.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        F₁₂.whiskerLeft e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β
⊢ CommShift e₁₃ A

Tactic:
by
  subst h₁₃
  infer_instance

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' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (n + a) + a * (a - 1) / 2).negOnePow) • γ.shift a

Tactic:
add_comm n a,

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' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (a + n) + a * (a - 1) / 2).negOnePow) • γ.shift a
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
X₁ X₃ : C
⊢ HasBinaryBiproduct X₁ X₃

Tactic:
obtain ⟨X₂, inl, snd, mem⟩ := distinguished_cocone_triangle₂ (0 : X₃ ⟶ X₁⟦(1 : ℤ)⟧)
  obtain ⟨inr : X₃ ⟶ X₂, inr_snd : 𝟙 _ = inr ≫ snd⟩ :=
    Triangle.coyoneda_exact₃ _ mem (𝟙 X₃) (by simp)
  obtain ⟨fst : X₂ ⟶ X₁, hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl⟩ :=
    Triangle.coyoneda_exact₂ _ mem (𝟙 X₂ - snd ≫ inr) (by
      dsimp
      simp only [sub_comp, assoc, id_comp, ← inr_snd, comp_id, sub_self])
  refine ⟨⟨binaryBiproductData _ mem rfl inr inr_snd.symm fst ?_⟩⟩
  dsimp
  simp only [← hfst, sub_add_cancel]

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
p q : ℤ
hpq : p + -1 = q
⊢ p = q + 1

Tactic:
rw [← hpq, neg_add_cancel_right]

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
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₁
⊢ IsIso φ'.hom₂

Tactic:
h₂

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
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₁
⊢ IsIso (𝟙 T'.obj₂)
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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this✝² : IsIso φ.hom₁
this✝¹ : IsIso φ.hom₂
this✝ : IsIso φ.hom₃
this : IsIso φ
⊢ ∃ e', e'.hom.hom₁ = Arrow.Hom.left e.hom ∧ e'.hom.hom₂ = Arrow.Hom.right e.hom

Tactic:
exact ⟨asIso φ, by simp [φ], by simp [φ]⟩

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
⊢ W.multiplicativeClosure ≤ W.paths.strictMap (pathComposition C)

Tactic:
refine (W.multiplicativeClosure_le_iff _).2 fun X Y f hf ↦ ?_

Goal state after:
case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : W f
⊢ W.paths.strictMap (pathComposition C) f
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Paths.of C ⋙q (pathComposition C).toPrefunctor = 𝟭q C

Tactic:
dsimp only [Prefunctor.comp]
  congr
  funext X Y f
  exact Category.id_comp _

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

Goal state before:
pp: case refine_2.inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw : W w
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw⟩)) ≫ eqToHom ⋯

Tactic:
· have hw : W.Q.map w = (wIso w hw).hom := rfl
      have hw' := Functor.congr_hom h w
      simp only [Functor.comp_map, hw] at hw'
      refine Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'
      all_goals apply Functor.congr_obj h

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G✝ : D₁ ⥤ D₂
inst✝ : Φ.IsLocalizedEquivalence
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
⊢ Φ.op.IsLocalizedEquivalence

Tactic:
let : CatCommSq Φ.op.functor W₁.Q.op W₂.Q.op G.op :=
    ⟨NatIso.op (CatCommSq.iso Φ.functor W₁.Q W₂.Q G).symm⟩

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G✝ : D₁ ⥤ D₂
inst✝ : Φ.IsLocalizedEquivalence
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
this : CatCommSq Φ.op.functor W₁.Q.op W₂.Q.op G.op := { iso := NatIso.op (CatCommSq.iso Φ.functor W₁.Q W₂.Q G).symm }
⊢ Φ.op.IsLocalizedEquivalence
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: case refine_1
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this✝ : IsIso (whiskerRight ε₁ W₁.Q)
this : IsIso (whiskerRight ε₂ W₂.Q)
⊢ (Φ.functor ⋙ W₂.Q) ⋙ Ψ.localizedFunctor W₂.Q W₁.Q ≅ W₁.Q

Tactic:
exact Functor.associator _ _ _ ≪≫
        isoWhiskerLeft _ (CatCommSq.iso Ψ.functor W₂.Q W₁.Q _).symm ≪≫
        (Functor.associator _ _ _).symm ≪≫
        (asIso (whiskerRight ε₁ W₁.Q)).symm ≪≫ Functor.leftUnitor _

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G✝ : D₁ ⥤ D₂
inst✝ : Φ.IsLocalizedFullyFaithful
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
⊢ Φ.op.IsLocalizedFullyFaithful

Tactic:
let : CatCommSq Φ.op.functor W₁.Q.op W₂.Q.op G.op :=
    ⟨NatIso.op (CatCommSq.iso Φ.functor W₁.Q W₂.Q G).symm⟩

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G✝ : D₁ ⥤ D₂
inst✝ : Φ.IsLocalizedFullyFaithful
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
this : CatCommSq Φ.op.functor W₁.Q.op W₂.Q.op G.op := { iso := NatIso.op (CatCommSq.iso Φ.functor W₁.Q W₂.Q G).symm }
⊢ Φ.op.IsLocalizedFullyFaithful
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
hf : W₂ f
e : Arrow.mk
    (Φ.functor.map
      (Φ.functor.preimage ((Φ.functor.objObjPreimageIso X).hom ≫ f ≫ (Φ.functor.objObjPreimageIso Y).inv))) ≅
  Arrow.mk f :=
  Arrow.isoMk (Φ.functor.objObjPreimageIso X) (Φ.functor.objObjPreimageIso Y) ⋯
⊢ (W₂.inverseImage Φ.functor).map Φ.functor f

Tactic:
exact ⟨_, _, _, (W₂.arrow_mk_iso_iff e).2 hf, ⟨e⟩⟩

Goal state after:
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
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
h₁ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂
h₂ : add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂
⊢ add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂

Tactic:
h₂

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
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
h₁ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂
h₂ : add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂
⊢ add W eX' eY' f₁ f₂ = add W eX' eY' f₁ f₂
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure.limitsClosure J = P.limitsClosure J

Tactic:
by
  refine le_antisymm (limitsClosure_le ?_)
    (limitsClosure_monotone _ P.le_isoClosure)
  rw [isoClosure_le_iff]
  exact le_limitsClosure P J

Goal state after:
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₂ ⊢
  simpa using Cardinal.mul_lt_of_lt hκ h₁ h₂

Goal state after: