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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : f₁ ≫ a₂ = a₁ ≫ g₁
ha₂₃ : f₂ ≫ a₃ = a₂ ≫ g₂
b₂ : X' ⟶ X
hb₁₂ : g₁ ≫ b₂ = b₁ ≫ f₁
hb₂₃ : g₂ ≫ b₃ = b₂ ≫ f₂
⊢ (Triangle.mk f₁ f₂ f₃).mor₂ ≫ 𝟙 B = (a₂ ≫ b₂) ≫ (Triangle.mk f₁ f₂ f₃).mor₂

Tactic:
dsimp; grind

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

Goal state before:
pp: case succ
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
hPQ : P ≤ Q
n : ℕ
h : P.extensionProductIter n ≤ Q.extensionProductIter n
⊢ P.extensionProductIter (n + 1) ≤ Q.extensionProductIter (n + 1)

Tactic:
grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
⊢ QuasiIso f

Tactic:
quasiIso_iff

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
⊢ ∀ (i : ι), QuasiIsoAt f i
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

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'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ K.ExactAt i'

Tactic:
rw [exactAt_iff]

Goal state after:
ι : 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'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ (K.sc i').Exact
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
by_cases hi : ∃ i, e.f i = i'

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
hi : ∃ i, e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

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
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
hi : ¬∃ i, e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ∃ j, e.f j = j'
⊢ (((single C c i).obj X).extend e).d j' k' = 0

Tactic:
obtain ⟨j, rfl⟩ := hj
    by_cases hk : ∃ k, e.f k = k'
    · obtain ⟨k, rfl⟩ := hk
      simp [extend_d_eq _ _ rfl rfl]
    · exact IsZero.eq_of_tgt (isZero_extend_X _ _ _ (by tauto)) _ _

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
φ : (e.extendFunctor C).obj K ⟶ (e.extendFunctor C).obj L
i j : ι
h : c.Rel i j
⊢ ((K.extendXIso e ⋯).inv ≫ φ.f (e.f i) ≫ (L.extendXIso e ⋯).hom) ≫ L.d i j =
    K.d i j ≫ (K.extendXIso e ⋯).inv ≫ φ.f (e.f j) ≫ (L.extendXIso e ⋯).hom

Tactic:
have := φ.comm (e.f i) (e.f j)
        simp only [extendFunctor_obj, K.extend_d_eq e rfl rfl, L.extend_d_eq e rfl rfl] at this
        simp [← cancel_mono (L.extendXIso e rfl).inv, Category.assoc, this]

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

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'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
⊢ K.homologyι j' ≫ K.fromOpcycles j' (e.f k) ≫ (K.truncGE'XIso e ⋯ ⋯).inv = 0

Tactic:
homologyι_comp_fromOpcycles_assoc,

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'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
⊢ 0 ≫ (K.truncGE'XIso e ⋯ ⋯).inv = 0
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case mpr
ι : 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'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
⊢ QuasiIso (K.πTruncGE e)

Tactic:
quasiIso_iff

Goal state after:
case mpr
ι : 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'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
⊢ ∀ (i : ι'), QuasiIsoAt (K.πTruncGE e) i
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

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 M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncLE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
⊢ (K.truncLE e).IsStrictlySupported e'

Tactic:
by
  rw [← isStrictlySupported_op_iff]
  exact inferInstanceAs ((K.op.truncGE e.op).IsStrictlySupported e'.op)

Goal state after:
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
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
quasiIso_iff

Goal state after:
ι : 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
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ (∀ (i : ι'), QuasiIsoAt (truncGEMap φ e) i) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
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
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ QuasiIso (truncGEMap φ n) ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i

Tactic:
HomologicalComplex.quasiIso_truncGEMap_iff

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ (∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i) → ∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i'

Tactic:
rintro h i i' rfl

Goal state after:
case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
h : ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
i : ℕ
⊢ QuasiIsoAt φ ((embeddingUpIntGE n).f i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ (∀ i ≤ n, QuasiIsoAt φ i) → ∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i'

Tactic:
rintro h i i' rfl

Goal state after:
case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
h : ∀ i ≤ n, QuasiIsoAt φ i
i : ℕ
⊢ QuasiIsoAt φ ((embeddingUpIntLE n).f i)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: 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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
⊢ QuasiIso φ.τ₃

Tactic:
quasiIso_iff

Goal state after:
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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
⊢ ∀ (i : ι), QuasiIsoAt φ.τ₃ i
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: 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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
⊢ QuasiIso φ.τ₃

Tactic:
by
  rw [quasiIso_iff]
  intro i
  rw [quasiIsoAt_iff_isIso_homologyMap]
  apply isIso_homologyMap_τ₃ φ hS₁ hS₂
  all_goals infer_instance

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

Goal state before:
pp: case pos.hf
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.f =
    0

pp: case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.g =
    0

Tactic:
· simp [← cancel_epi (HomologicalComplex.homologyMap S.f i),
        ← HomologicalComplex.homologyMap_comp]

Goal state after:
case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.g =
    0
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
this : HasDerivedCategory C := ⋯
⊢ (comp 0 β h).hom = hom 0

Tactic:
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
this : HasDerivedCategory C := ⋯
⊢ (α.comp 0 h).hom = hom 0

Tactic:
simp [this, zero_hom']

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ (opEquiv' n a a' h).symm (x + y) = (opEquiv' n a a' h).symm x + (opEquiv' n a a' h).symm y

Tactic:
dsimp [opEquiv']
  rw [opEquiv_symm_add, Preadditive.add_comp]

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

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := kernel (Projective.π X), X₂ := Projective.over X, X₃ := X, f := kernel.ι (Projective.π X),
    g := Projective.π X, zero := ⋯ }
hS : S.ShortExact
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
have : Function.Surjective (Ext.precomp hS.extClass Y (add_comm 1 n)) := fun x₃ ↦
      Ext.contravariant_sequence_exact₃ hS Y x₃
        (Ext.eq_zero_of_projective _) (by lia)

Goal state after:
case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
this✝¹ : HasDerivedCategory C := HasDerivedCategory.standard C
this✝ : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := kernel (Projective.π X), X₂ := Projective.over X, X₃ := X, f := kernel.ι (Projective.π X),
    g := Projective.π X, zero := ⋯ }
hS : S.ShortExact
this : Function.Surjective ⇑(hS.extClass.precomp Y ⋯)
⊢ Small.{w, max u v} (Ext X Y (n + 1))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i : ℤ
φ : Q.obj K ⟶ Q.obj ((CochainComplex.singleFunctor C i).obj I)
n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
⊢ φ = 0

Tactic:
obtain ⟨L, _, g, ι, h, rfl⟩ := left_fac_of_isStrictlyGE φ i

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
⊢ Q.map g ≫ inv (Q.map ι) = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
⊢ AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯) ≫ AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯) = 0

Tactic:
by
        ext
        dsimp
        simp only [mk₀_comp_mk₀_assoc, ShortComplex.zero, mk₀_zero, zero_comp]

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

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.relation r ∈ Submodule.span A (Set.range relations.relation)

Tactic:
exact Submodule.subset_span (by simp)

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
⊢ (Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)) (relations.relation r) = 0

Tactic:
by
    have : π = Finsupp.linearCombination _ (fun g ↦ π (Finsupp.single g 1)) := by ext; simp
    rw [← this]
    exact hπ r

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

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Finite n
this : Fintype n
h : ∀ (v : m → R), v ᵥ* M = 0 → v = 0
w : m → R
hw : ∀ (w_1 : n → R), w ⬝ᵥ M *ᵥ w_1 = 0
i : n
⊢ (w ᵥ* M) i = 0 i

Tactic:
classical simpa using! hw <| Pi.single i 1

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)

Tactic:
cases nonempty_fintype ι; rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]

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✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
⊢ ⟨(Units.map ↑σ) ↑1, ⋯⟩ = 1

Tactic:
ext1; simp only [OneMemClass.coe_one, map_one]

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

Goal state before:
pp: R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ((toLinearMap₂'Aux σ₁ σ₂ f) (Pi.single i 1)) (Pi.single j 1) = f i j

Tactic:
rw [Matrix.toLinearMap₂'Aux, mk₂'ₛₗ_apply]
  have : (∑ i', ∑ j', (if i = i' then (1 : S₁) else (0 : S₁)) •
        (if j = j' then (1 : S₂) else (0 : S₂)) • f i' j') =
      f i j := by
    simp_rw [← Finset.smul_sum]
    simp only [ite_smul, one_smul, zero_smul, sum_ite_eq, mem_univ, ↓reduceIte]
  rw [← this]
  exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by aesop

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
⊢ (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)

Tactic:
by
  induction n with
  | zero => exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm
  | succ n n_ih =>
    rw [pow_succ, n_ih, of_mul_of]
    exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ - -1 • Q x = Q x

Tactic:
neg_neg,

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ 1 • Q x = Q x
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : (coeAlgHom 𝒜).comp decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : ↥(𝒜 i)), decompose ↑x = (of (fun i ↦ ↥(𝒜 i)) i) x
i : ι
x : ↥(𝒜 i)
⊢ ((decompose.comp (coeAlgHom 𝒜)).toLinearMap ∘ₗ lof R ι (fun i ↦ ↥(𝒜 i)) i) x =
    ((AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))).toLinearMap ∘ₗ lof R ι (fun i ↦ ↥(𝒜 i)) i) x

Tactic:
exact (decompose.congr_arg <| DirectSum.coeAlgHom_of _ _ _).trans (left_inv i x)

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

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = 0

Tactic:
by
  lift a to 𝒜 i using a_mem
  rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
⊢ 2 * ⟨⅟2, ⋯⟩ • 1 = 1

Tactic:
ext m
    dsimp [Submonoid.smul_def]
    rw [← ofNat_smul_eq_nsmul R, smul_invOf_smul (2 : R) m]

Goal state after: