mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Triangulated

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
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle D
hT₁ : T₁ ∈ L.essImageDistTriang
hT₂ : T₂ ∈ L.essImageDistTriang
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃

Tactic:
refine L.complete_distinguished_essImageDistTriang_morphism ?_ T₁ T₂ hT₁ hT₂ a b 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
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle D
hT₁ : T₁ ∈ L.essImageDistTriang
hT₂ : T₂ ∈ L.essImageDistTriang
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∀ (T₁' T₂' : Triangle C),
    T₁' ∈ distinguishedTriangles →
      T₂' ∈ distinguishedTriangles →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
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
f : Z ⟶ F.obj (X₁ ⊞ X₂)
hf : f ≫ F.biprodComparison X₁ X₂ = 0
⊢ f = 0

Tactic:
let S := (ShortComplex.mk _ _ (biprod.inl_snd (X := X₁) (Y := X₂))).map F

Goal state after:
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
f : Z ⟶ F.obj (X₁ ⊞ X₂)
hf : f ≫ F.biprodComparison X₁ X₂ = 0
S : ShortComplex A := { X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := biprod.inl, g := biprod.snd, zero := ⋯ }.map F
⊢ f = 0
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P.retracts ≤ P

Tactic:
← isStableUnderRetracts_iff_retracts_le

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P.IsStableUnderRetracts
Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ

Tactic:
quasiIso_eq_trW_subcategoryAcyclic

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (subcategoryAcyclic C).trW.IsCompatibleWithShift ℤ
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
a : ℤ
x✝ : C
⊢ eqToHom ⋯ = ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app ((single C (ComplexShape.up ℤ) a).obj x✝)).f a

Tactic:
simp only [single, shiftFunctorZero_eq, shiftFunctorZero'_hom_app_f,
      XIsoOfEq, eqToIso.hom]

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : QuasiIso φ
⊢ QuasiIso ((opFunctor V c).map φ.op)

Tactic:
quasiIso_opFunctor_map_iff

Goal state after:
ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : QuasiIso φ
⊢ QuasiIso φ
Module: Mathlib.Algebra.Homology.Embedding.Restriction

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
⊢ (K.restriction e).d i j = (K.restrictionXIso e ⋯).hom ≫ K.d (e.f i) (e.f j) ≫ (K.restrictionXIso e ⋯).inv

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Restriction

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (restrictionMap φ e).f i = (K.restrictionXIso e ⋯).hom ≫ φ.f (e.f i) ≫ (L.restrictionXIso e ⋯).inv

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
have : (K.extendXIso e hi'').hom ≫ f' = f'' := by
      apply Fork.IsLimit.hom_ext hcone
      rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
this : (K.extendXIso e hi'').hom ≫ f' = f''
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
⊢ e.HasLift (e.homRestrict ψ)

Tactic:
intro j hj i' hij'
  have : (L.extend e).d i' (e.f j) = 0 := by
    apply (L.isZero_extend_X e i' (hj.notMem hij')).eq_of_src
  dsimp [homRestrict]
  rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

Tactic:
obtain ⟨i, rfl⟩ := hi'
    simp [e.homRestrict_f _ rfl, e.liftExtend_f _ _ rfl]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
k' : ι'
hk' : e.f k = k'
hk'' : c'.next (e.f j) = k'
hi'' : c'.prev (e.f j) = e.f i
⊢ (K.restrictionXIso e ⋯).hom ≫ (K.sc' (e.f i) (e.f j) k').f =
    ((K.restriction e).sc' i j k).f ≫ (K.restrictionXIso e ⋯).hom

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' : ι'
hi' : e.f i = i'
hi'' : c'.prev (e.f j) = i'
hk'' : c'.next (e.f j) = e.f k
⊢ (K.restrictionXIso e ⋯).hom ≫ (K.sc' i' (e.f j) (e.f k)).g =
    ((K.restriction e).sc' i j k).g ≫ (K.restrictionXIso e ⋯).hom

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (truncGE'Map φ e).f i = (K.truncGE'XIso e ⋯ hi).hom ≫ φ.f (e.f i) ≫ (L.truncGE'XIso e ⋯ hi).inv

Tactic:
exact dif_neg hi

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv =
    (K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (K.truncGE'XIso e ⋯ hi).inv = (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).inv

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ ((K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv) ≫
      (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv =
    (K.restriction e).d i j ≫ (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ ⋯).inv

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ ((K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).inv) ≫
      (K.truncGE'XIso e ⋯ hi).hom ≫ K.d (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv =
    (K.restriction e).d i j ≫ (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ ⋯).inv

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f j) ≫ (K.truncGE'XIsoOpcycles e ⋯ hj).inv = 0

Tactic:
simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ (K.truncLE e).Acyclic ↔ K.IsSupportedOutside e

Tactic:
by
  rw [← acyclic_op_iff, ← isSupportedOutside_op_iff]
  exact K.op.acyclic_truncGE_iff_isSupportedOutside e.op

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ (desc.aux X (ac.equiv (ac.equiv.symm (e₁.f i₁))) (e₁.f i₁) ⋯)
      ((desc.aux X (e₁.f i₁) (ac.equiv (ac.equiv.symm (e₁.f i₁))) ⋯) (x₁ i₁)) =
    x₁ i₁

Tactic:
desc.aux_trans

Goal state after:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ (desc.aux X (e₁.f i₁) (e₁.f i₁) ⋯) (x₁ i₁) = x₁ i₁
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ (desc.aux X (ac.equiv (ac.equiv.symm (e₂.f i₂))) (e₂.f i₂) ⋯)
      ((desc.aux X (e₂.f i₂) (ac.equiv (ac.equiv.symm (e₂.f i₂))) ⋯) (x₂ i₂)) =
    x₂ i₂

Tactic:
desc.aux_trans

Goal state after:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ (desc.aux X (e₂.f i₂) (e₂.f i₂) ⋯) (x₂ i₂) = x₂ i₂
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ¬∃ j, c.Rel i j
⊢ Mono (homologyMap φ.τ₃ i)

Tactic:
refine mono_of_epi_of_epi_of_mono (mapComposableArrows₂ φ i)
      (composableArrows₂_exact hS₁ i) (composableArrows₂_exact hS₂ i) ?_ h₁ h₂
    have := hS₁.epi_g
    apply epi_homologyMap_of_epi_of_not_rel
    simpa using hi

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Ext S.X₃ S.X₁ 1

Tactic:
change SmallHom W (S').X₃ ((S').X₁⟦(1 : ℤ)⟧)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := ⋯
⊢ ((Ext.mk₀ S.g).comp hS.extClass ⋯).hom = Ext.hom 0

Tactic:
simp only [Ext.comp_hom, Ext.mk₀_hom, extClass_hom, Ext.zero_hom,
    ShiftedHom.mk₀_comp]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (singleFunctor C 0).map S.g ≫ hS.singleδ = 0
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃

Tactic:
obtain ⟨c, hc₁, hc₂⟩ :=
    Pretriangulated.complete_distinguished_triangle_morphism₁ _ _ hT₂ hT₁
      b.unop a.unop (Quiver.Hom.op_inj comm.symm)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c :
  (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂)).obj₁ ⟶
    (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁)).obj₁
hc₁ :
  (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂)).mor₁ ≫ b.unop =
    c ≫ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁)).mor₁
hc₂ :
  (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂)).mor₃ ≫ (shiftFunctor C 1).map c =
    a.unop ≫ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁)).mor₃
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
N M : ModuleCat R
inst✝¹ : Module.Finite R ↑N
inst✝ : Module.Finite R ↑M
i : ℕ
⊢ Module.Finite R (Ext N M i)

Tactic:
induction i generalizing N with
  | zero => exact Module.Finite.equiv (Ext.linearEquiv₀.trans ModuleCat.homLinearEquiv).symm
  | succ n ih =>
    obtain ⟨N, _, _, _, _, f, surjf⟩ := Module.exists_finite_presentation R N
    let exac := LinearMap.shortExact_shortComplexKer surjf
    exact Module.Finite.of_surjective (exac.extClass.precompOfLinear R M (add_comm 1 n))
      (precomp_extClass_surjective_of_projective_X₂ M exac n)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S✝ : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
⊢ Finite (L →* Rˣ)

Tactic:
have : Finite (L →* S) := .of_injective _ DFunLike.coe_injective

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S✝ : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (L →* ↥S)
⊢ Finite (L →* Rˣ)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
g : SL(2, R)
⊢ P g

Tactic:
by
  obtain ⟨m, hm⟩ := g
  convert! h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm)
  ext i j; fin_cases i <;> fin_cases j <;> rfl

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = mk (l.dProdIndex fun i ↦ (f i).fst) (l.dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd)

Tactic:
by
  rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]
  simp_rw [Sigma.eta]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + polar f x y

Tactic:
rw [polar]
  abel

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
⊢ ∀ (x y : ⨁ (i : ι), A i), (toAddMonoid f) (x * y) = (toAddMonoid f) x * (toAddMonoid f) y

Tactic:
rw [(toAddMonoid f).map_mul_iff]
      refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))
      refine DirectSum.addHom_ext' (fun yi ↦ AddMonoidHom.ext (fun yv ↦ ?_))
      change
        toAddMonoid f (of A xi xv * of A yi yv) =
          toAddMonoid f (of A xi xv) * toAddMonoid f (of A yi yv)
      simp_rw [of_mul_of, toAddMonoid_of]
      exact hmul _ _

Goal state after:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ s.prod n = 0

Tactic:
have := listProd_apply_eq_zero (l := s.toList) (by simpa using hs)
    (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])
  simpa [← Multiset.prod_coe, ← Multiset.map_coe]

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ ∈ powersetCard α m

Tactic:
by simp [Finset.card_compl, mem_iff.mp s.2]; omega

Goal state after: