mathlib-initiative/mathlib-tactics huggingface dataset:
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ G.Additive ↔ (L ⋙ G).Additive

Tactic:
constructor
  · intro
    infer_instance
  · intro h
    suffices ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g by
      refine ⟨fun {X Y f g} => ?_⟩
      have hL := essSurj L W
      have eq := this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
        ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
      rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp,
        ← comp_add, ← comp_add, ← add_comp, ← add_comp, Functor.map_comp, Functor.map_comp] at eq
      rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
        ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]
    intro X Y f g
    obtain ⟨φ, rfl, rfl⟩ := exists_leftFraction₂ L W f g
    rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
      add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
      LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
      Functor.map_add, Functor.comp_map, Functor.comp_map]

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }
this : Φ.IsLocalizedEquivalence
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans
    (Trans.trans
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight (CatCommSq.iso Φ.functor L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
⊢ W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)

Tactic:
simpa only [← MorphismProperty.IsInvertedBy.iff_comp _ _ E₃.inverse,
      MorphismProperty.IsInvertedBy.iff_of_iso W₃ iso] using hW₃

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ i

Tactic:
constructor
  · intro
    exact quasiIsoAt_of_comp_right φ φ' i
  · intro
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
⊢ subcategoryAcyclic C ((quotient C (ComplexShape.up ℤ)).obj K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n

Tactic:
by
  rw [mem_subcategoryAcyclic_iff]
  refine forall_congr' (fun n => ?_)
  simp only [HomologicalComplex.exactAt_iff_isZero_homology]
  exact ((homologyFunctorFactors C (ComplexShape.up ℤ) n).app K).isZero_iff

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ (↑(inr φ)).v p q hpq ≫ (snd φ).v q p ⋯ = 𝟙 (L.X p)

Tactic:
simp [inr, snd, Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero p),
    Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero p),
    Int.negOnePow_even 2 ⟨1, rfl⟩]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ δ m n (descCochain φ α β h) =
    (Cochain.ofHom (fst φ)).comp (δ m n α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯ + (snd φ).comp (δ n n' β) ⋯

Tactic:
dsimp [descCochain, fst, snd, mappingCocone]
  ext p q hpq
  subst h
  obtain rfl : n' = m + 2 := by lia
  simp [Cochain.δ_leftShift _ (-1) _ (m + 1) _ (m + 2) (by lia),
    mappingCone.δ_descCochain (m := m) (n := m + 1) _ _ _ _ (m + 2) (by lia),
    Cochain.leftShift_v (n := 1) _ _ _ _ p p _ (p + -1) (by lia),
    Cochain.leftShift_v (n := m + 2) _ (-1) _ _ _ q _ (p + -1) (by lia),
    Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
    Cochain.comp_v (n₁ := 1) _ _ _ (p + -1) p _ (by lia) hpq,
    Cochain.comp_v (n₂ := m + 2) _ _ _ p (p + -1) q rfl (by lia),
    smul_smul, Int.negOnePow_add, Int.negOnePow_even 2 ⟨1, rfl⟩]
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind` -/
  abel

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n : ℤ
⊢ homologyMap T.mor₁ n ≫ homologyMap T.mor₂ n = 0

Tactic:
by
  rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    ← DerivedCategory.homologyFunctorFactors_hom_naturality_assoc,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality,
    ← Functor.map_comp_assoc, dsimp% comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero,
    Limits.zero_comp, Limits.comp_zero]

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

Goal state before:
pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Tactic:
have := h.2 n

Goal state after:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬(up ℤ).Rel ((embeddingUpIntGE p).f n) ((embeddingUpIntGE p).f (n + 1))
⊢ n + 1 = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ n + 1 = 0

Tactic:
have := h.2 n

Goal state after:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
this : ¬(up ℤ).Rel ((embeddingUpIntLE p).f (n + 1)) ((embeddingUpIntLE p).f n)
⊢ n + 1 = 0
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 j k : ι
⊢ d K e i j ≫ d K e j k = 0

Tactic:
by
  dsimp [d]
  by_cases hij : c.Rel i j
  · by_cases hjk : c.Rel j k
    · rw [dif_pos hij, dif_pos hjk, dif_neg (e.not_boundaryGE_next hij)]
      split_ifs <;> simp
    · rw [dif_neg hjk, comp_zero]
  · rw [dif_neg hij, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
this : IsIso (Q.map (CochainComplex.truncLEMap s n))
⊢ IsIso (Q.map (CochainComplex.truncLEMap s n ≫ X.ιTruncLE n))

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
this : IsIso (Q.map (CochainComplex.truncLEMap s n))
⊢ inv (Q.map s) ≫ Q.map g =
    inv (Q.map (CochainComplex.truncLEMap s n ≫ X.ιTruncLE n)) ≫ Q.map (CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n)

Tactic:
· rw [Q.map_comp]
    infer_instance

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
this : IsIso (Q.map (CochainComplex.truncLEMap s n))
⊢ inv (Q.map s) ≫ Q.map g =
    inv (Q.map (CochainComplex.truncLEMap s n ≫ X.ιTruncLE n)) ≫ Q.map (CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n)
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
⊢ IsIso (Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n))

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
⊢ Q.map g ≫ inv (Q.map s) =
    Q.map (X.πTruncGE n ≫ CochainComplex.truncGEMap g n) ≫ inv (Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n))

Tactic:
· rw [Q.map_comp]
    infer_instance

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
⊢ Q.map g ≫ inv (Q.map s) =
    Q.map (X.πTruncGE n ≫ CochainComplex.truncGEMap g n) ≫ inv (Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n))
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ IsIso (Q.map (CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a)))

pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ f =
    inv (Q.map (CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a))) ≫
      Q.map (CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a))

Tactic:
· rw [Q.map_comp]
    infer_instance

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ f =
    inv (Q.map (CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a))) ≫
      Q.map (CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a))
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ IsIso (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ f =
    Q.map (inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b) ≫
      inv (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

Tactic:
· rw [Q.map_comp]
    infer_instance

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ f =
    Q.map (inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b) ≫
      inv (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ comp 0 β h = 0

Tactic:
by
  let := HasDerivedCategory.standard C; ext; simp [this, zero_hom']

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
⊢ α.comp 0 h = 0

Tactic:
by
  let := HasDerivedCategory.standard C; ext; simp [this, zero_hom']

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (triangleOfSES h₁).mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (Q.map f.τ₁) = Q.map f.τ₃ ≫ (triangleOfSES h₂).mor₃

Tactic:
dsimp [triangleOfSES, triangleOfSESδ]
    rw [assoc, assoc, IsIso.inv_comp_eq, ← Functor.map_comp_assoc,
      ← CochainComplex.mappingCone.map_descShortComplex,
      Functor.map_comp_assoc, IsIso.hom_inv_id_assoc,
      ← Functor.commShiftIso_hom_naturality,
      ← Functor.map_comp_assoc, ← Functor.map_comp_assoc]
    congr 2
    exact (CochainComplex.mappingCone.triangleMap S₁.f S₂.f f.τ₁ f.τ₂ f.comm₁₂.symm).comm₃

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧
    a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ ≫ (snd S.f).v n₁ n₁ ⋯ +
        b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁ ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
inr_f_snd_v,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧
    a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ ≫ (snd S.f).v n₁ n₁ ⋯ + b ≫ S.X₂.d n₀ n₁ ≫ 𝟙 (S.X₂.X n₁) =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
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
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    (𝟙 ((singleFunctors C).functor 0)).app S.X₃ ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁)

Tactic:
singleFunctorsPostcompQIso_inv_hom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    (𝟙 ((singleFunctors C).functor 0)).app S.X₃ ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map
              ((𝟙 (((CochainComplex.singleFunctors C).postcomp Q).functor 0)).app S.X₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
⊢ IsSplitMono ι

Tactic:
let e := L.pOpcyclesIso (i - 1) i (by simp)
    ((L.isZero_of_isStrictlyGE i (i - 1) (by simp)).eq_of_src _ _)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
⊢ IsSplitMono ι
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
μ : V₁ → K₁
h : (B x) (μ x • x) = 0
hμzero : μ x = 0
⊢ 0 ∈ ⊥

Tactic:
Submodule.mem_bot

Goal state after:
K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
μ : V₁ → K₁
h : (B x) (μ x • x) = 0
hμzero : μ x = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: R : Type u_1
M : Type u_4
M₁ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
⊢ (B.domRestrict₁₂ W W).Nondegenerate

Tactic:
by
  rw [(hB.domRestrict W).nondegenerate_iff_separatingLeft]
  rintro ⟨x, hx⟩ b₁
  rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R]
  refine hW.le_bot ⟨hx, fun y hy ↦ ?_⟩
  specialize b₁ ⟨y, hy⟩
  simp_rw [domRestrict₁₂_apply] at b₁
  exact hB.eq_zero b₁

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
this : π = Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)
⊢ π (relations.relation r) = 0

Tactic:
exact hπ r

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
inst✝ : DecidableEq ι
⊢ e.toMatrix ⇑e = 1

Tactic:
by
  unfold Basis.toMatrix
  ext i j
  simp [Matrix.one_apply, Finsupp.single_apply, eq_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ i, w i • ∑ j, A i j • v j = 0
⊢ ∀ (i : κ), w i = 0

Tactic:
suffices w = 0 by aesop

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ i, w i • ∑ j, A i j • v j = 0
⊢ w = 0