mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
· obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some
      · rw [extend.d_none_eq_zero' K _ _ hj']
      · rw [extend.d_eq K hi hj, K.shape, zero_comp, comp_zero]
        obtain rfl := e.f_eq_of_r_eq_some hi
        obtain rfl := e.f_eq_of_r_eq_some hj
        intro hij
        exact h (e.rel hij)

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

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✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Projective (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Projective ((K.extend e).X i')

Tactic:
· exact (isZero_extend_X K e i' hi').projective

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

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ { f := fun i ↦ (K.extendXIso e ⋯).inv ≫ ((e.extendFunctor C).map f).f (e.f i) ≫ (L.extendXIso e ⋯).hom, comm' := ⋯ } =
    f

Tactic:
by
    ext i
    simp [HomologicalComplex.extendMap_f _ _ rfl]

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' e).d i j =
    (K.restriction e).d i j ≫ (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ ⋯).inv

Tactic:
K.truncGE'_d_eq_fromOpcycles e hij rfl rfl hi

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
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
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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : HasZeroObject C
i' : ι'
i : ι
hi : e.f i = i'
⊢ Epi ((K.πTruncGE e).f i')

Tactic:
dsimp [πTruncGE]

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
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : HasZeroObject C
i' : ι'
i : ι
hi : e.f i = i'
⊢ Epi ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f i')
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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
i' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso ((K.πTruncGE e).f i')

Tactic:
dsimp [πTruncGE]

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
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
i' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f i')
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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
i' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f i')

Tactic:
e.isIso_liftExtend_f_iff _ _ hi

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
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
i' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso ((K.restrictionToTruncGE' e).f i)
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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'
inst✝ : HasZeroObject C
⊢ QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
by
  have : ∀ (i : ι) (i' : ι') (_ : e.f i = i'),
      QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i' := by
    rintro i _ rfl
    rw [← quasiIsoAt_iff_comp_left (K.πTruncGE e), πTruncGE_naturality φ e,
      quasiIsoAt_iff_comp_right]
  rw [quasiIso_iff]
  constructor
  · intro h i i' hi
    simpa only [← this i i' hi] using h i'
  · intro h i'
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, hi⟩ := hi'
      simpa only [this i i' hi] using h i i' hi
    · rw [quasiIsoAt_iff_exactAt]
      all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsStrictlyGE n
⊢ IsIso (K.πTruncGE n)

Tactic:
dsimp [πTruncGE]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsStrictlyGE n
⊢ IsIso (HomologicalComplex.πTruncGE K (embeddingUpIntGE n))
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
inst✝¹ : L.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
inst✝ : HasSmallLocalizedHom W X Y
⊢ (equiv W L) (mkInv f hf) = (isoOfHom L W f hf).inv

Tactic:
simp only [equiv, mkInv, Equiv.symm_trans_apply, Equiv.symm_symm, homEquiv_symm_apply,
    Equiv.trans_apply, Equiv.symm_apply_apply, homEquiv_isoOfHom_inv]

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

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : i < n
⊢ n - ↑(n - i).natAbs = i

Tactic:
rw [Int.natAbs_of_nonneg (by lia), sub_sub_cancel]

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

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃

Tactic:
· dsimp [triangleOfSESδ]
    rw [CategoryTheory.Functor.map_id, comp_id, IsIso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)

Tactic:
@pullbackShiftFunctorAdd'_hom_app (OppositeShift C ℤ) _ _ _ _ _ _ _ X
    a₁ a₂ a₃ h b₁ b₂ b₃ (by dsimp; lia) (by dsimp; lia) (by dsimp; lia)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₃ b₃ ⋯).hom.app X ≫
      (shiftFunctorAdd' (OppositeShift C ℤ) b₁ b₂ b₃ ⋯).hom.app X ≫
        (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₂ b₂ ⋯).inv.app
            ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫
          (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯)) a₂).map
            ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₁ b₁ ⋯).inv.app X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (iso adj a) (iso adj b)) (Functor.commShiftIso G (a + b))

Tactic:
rw [G.commShiftIso_add]

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
    (Functor.CommShift.isoAdd (Functor.commShiftIso G a) (Functor.commShiftIso G b))
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁷ : AddMonoid A
inst✝⁶ : AddMonoid B
inst✝⁵ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasShift D B
F : C ⥤ D
inst✝² : F.CommShift B
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.CommShift B
inst✝ : adj.CommShift B
⊢ NatTrans.CommShift (PullbackShift.adjunction φ adj).unit A

Tactic:
dsimp [PullbackShift.adjunction]

Goal state after:
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁷ : AddMonoid A
inst✝⁶ : AddMonoid B
inst✝⁵ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasShift D B
F : C ⥤ D
inst✝² : F.CommShift B
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.CommShift B
inst✝ : adj.CommShift B
⊢ NatTrans.CommShift
    ((NatTrans.PullbackShift.natIsoId C φ).hom ≫
      PullbackShift.natTrans φ adj.unit ≫ (NatTrans.PullbackShift.natIsoComp φ F G).hom)
    A
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁷ : AddMonoid A
inst✝⁶ : AddMonoid B
inst✝⁵ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasShift D B
F : C ⥤ D
inst✝² : F.CommShift B
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.CommShift B
inst✝ : adj.CommShift B
⊢ NatTrans.CommShift (PullbackShift.adjunction φ adj).counit A

Tactic:
dsimp [PullbackShift.adjunction]

Goal state after:
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁷ : AddMonoid A
inst✝⁶ : AddMonoid B
inst✝⁵ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasShift D B
F : C ⥤ D
inst✝² : F.CommShift B
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.CommShift B
inst✝ : adj.CommShift B
⊢ NatTrans.CommShift
    ((NatTrans.PullbackShift.natIsoComp φ G F).inv ≫
      PullbackShift.natTrans φ adj.counit ≫ (NatTrans.PullbackShift.natIsoId D φ).inv)
    A
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
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α

Tactic:
← cancel_mono e.hom

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 ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ e.hom = ((singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α) ≫ e.hom
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Function.Injective ⇑solution.fromQuotient

Tactic:
rw [← LinearMap.ker_eq_bot, eq_bot_iff]

Goal state after:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.fromQuotient.ker ≤ ⊥
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
⊢ (toLin b' c) (c.toMatrix ⇑c' * (toMatrix b' c') f) = (toLin b' c) ((toMatrix b' c) f)

Tactic:
have := Classical.decEq κ'
    rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]

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

Goal state before:
pp: n✝ : Type u_1
inst✝⁵ : Fintype n✝
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
⊢ ∑ i, A i j₀ ≤ 0

Tactic:
← mul_le_mul_iff_right₀ (h_j₀ ▸ h_sup),

Goal state after:
n✝ : Type u_1
inst✝⁵ : Fintype n✝
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
⊢ v j₀ * ∑ i, A i j₀ ≤ v j₀ * 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
⊢ (↑{i | i ≠ i₀}).Pairwise (Function.onFun Commute fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1)

Tactic:
intro i1

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
⊢ i1 ∈ ↑{i | i ≠ i₀} →
    ∀ ⦃y : ι⦄,
      y ∈ ↑{i | i ≠ i₀} → i1 ≠ y → Function.onFun Commute (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1 y
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
m' : Type u_14
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₂ f) = (toMatrix₂' R) B * toMatrix' f

Tactic:
by
  rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂]
  simp

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

Goal state before:
pp: case zero
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ 0 ∈ A 0

Tactic:
exact zero_mem (A 0)

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

Goal state before:
pp: case ofNat
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) ∈ A 0

Tactic:
Int.ofNat_eq_natCast,

Goal state after:
case ofNat
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑↑a✝ ∈ A 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ 1 (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝

Tactic:
Module.End.one_apply,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ Q (x✝¹ + x✝) - Q x✝¹ - Q x✝ = polar (⇑Q) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

Tactic:
let x := A₁ᵀ * Pᵀ * J

Goal state after:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑0 * ↑rj else 0) = 0

Tactic:
simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑0 * ↑rj else 0) = 0

Tactic:
simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑r * ↑rj else 0) = 0

Tactic:
rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]

Goal state after:
case h
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ∀ x ∈ DFinsupp.support r', ¬i + x = n