mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁✝ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
⊢ 0 ≫ R₂.map (homOfLE ⋯) = 0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7

Tactic:
zero_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁✝ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
⊢ 0 = 0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
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
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
        g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.g =
    0

Tactic:
· simp [← cancel_mono (HomologicalComplex.homologyMap S.g j),
        ← HomologicalComplex.homologyMap_comp]

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 Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ (-α).comp β h = -α.comp β h

Tactic:
by
  let := HasDerivedCategory.standard C; ext; simp [this, neg_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 Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ α.comp (-β) h = -α.comp β h

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

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ Mono (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 →
        ∀ (y₁ : A ⟶ L.X i), x₂ ≫ φ.f j = y₁ ≫ L.d i j → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
subst hi hk
  apply ShortComplex.mono_homologyMap_iff_up_to_refinements

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 =
    0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7

Tactic:
zero_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 = 0
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 ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ =
      0 ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d 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:
zero_comp,

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 ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ = 0 ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d 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
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₁ =
      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:
zero_comp,

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₁ = 0
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.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 ≫ (S.f.f n₁ + 0 ≫ S.X₂.d n₀ n₁) + b ≫ S.X₂.d n₀ n₁ = 0
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:
zero_comp,

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 ≫ (S.f.f n₁ + 0) + b ≫ S.X₂.d n₀ n₁ = 0
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.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₃
⊢ φ a₁ + φ a₂ = φ a₃

Tactic:
← h,

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₃
⊢ φ a₁ + φ a₂ = φ (a₁ + a₂)
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✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝)) ≫
        (shiftFunctorCompIsoId D (-a) a ⋯).inv.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝

Tactic:
shift_shiftFunctorCompIsoId_hom_app,

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✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝)) ≫
        (shiftFunctorCompIsoId D (-a) a ⋯).inv.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
          (shiftFunctorCompIsoId D (-a) a ⋯).hom.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
X : C
⊢ (x * y).app X = x.app X ≫ y.app X

Tactic:
rw [mul_app']
  exact x.naturality (y.app X)

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

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ r • homEquiv x = x.hom.comp (ShiftedHom.mk₀ (↑0) mk₀._proof_1 (r • 𝟙 ((DerivedCategory.singleFunctor C 0).obj Y))) ⋯

Tactic:
ShiftedHom.mk₀_smul,

Goal state after:
R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ r • homEquiv x = x.hom.comp (r • ShiftedHom.mk₀ (↑0) mk₀._proof_1 (𝟙 ((DerivedCategory.singleFunctor C 0).obj Y))) ⋯
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
L M N : C
f : M ⟶ N
hf : Mono f
⊢ Function.Injective ⇑((mk₀ f).postcomp L ⋯)

Tactic:
rw [← AddMonoidHom.ker_eq_bot_iff, AddSubgroup.eq_bot_iff_forall]
  intro x hx
  obtain ⟨g, rfl⟩ := Ext.addEquiv₀.symm.surjective x
  simpa [← cancel_mono f] using hx

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

Goal state before:
pp: case mpr
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ (RingHom.id K) z • (B x) y = 0

Tactic:
smul_eq_zero

Goal state after:
case mpr
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ (RingHom.id K) z = 0 ∨ (B x) y = 0
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
solution : relations.Solution M
h : solution.IsPresentation
⊢ Function.Surjective ⇑solution.π

Tactic:
by
  simpa only [← surjective_fromQuotient_iff_surjective_π] using h.bijective.2

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

Goal state before:
pp: ι : Type u_1
ι' : 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
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
⊢ LeftInverse (fun m j ↦ ∑ i, m i j • e i) e.toMatrix

Tactic:
by
    intro v
    ext j
    exact e.sum_toMatrix_smul_self v j

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
u : Rˣ
i✝ j✝ : n
⊢ ↑((map f) ((scalar n) u)) i✝ j✝ = ↑((scalar n) ((Units.map ↑f) u)) i✝ j✝

Tactic:
simp [Matrix.diagonal_apply]

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
u : Rˣ
i✝ j✝ : n
⊢ f (if i✝ = j✝ then ↑u else 0) = if i✝ = j✝ then f ↑u else 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case inr.inr.refine_2
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
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), ¬0 < v x
⊢ ∃ b, 0 < (-1 • v) b

Tactic:
not_lt

Goal state after:
case inr.inr.refine_2
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
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ ∃ b, 0 < (-1 • v) b
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 = (List.map (fun a ↦ mk (f a).fst (f a).snd) l).prod

Tactic:
GradedMonoid.mk

Goal state after:
ι : 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 = (List.map (fun a ↦ ⟨(f a).fst, (f a).snd⟩) l).prod
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
hlist : ∀ (L : List (TransvectionStruct ι F)), P (List.map TransvectionStruct.toSpecialLinearGroup L).prod
⊢ P M

Tactic:
obtain ⟨L, L', D, hD, hM⟩ := exists_list_transvec_mul_diagonal_mul_list_transvec M

Goal state after:
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
hlist : ∀ (L : List (TransvectionStruct ι F)), P (List.map TransvectionStruct.toSpecialLinearGroup L).prod
L L' : List (TransvectionStruct ι F)
D : ι → F
hD : (diagonal D).det = 1
hM :
  M =
    (List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, hD⟩ *
      (List.map TransvectionStruct.toSpecialLinearGroup L').prod
⊢ P M
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ [], r j ∈ A (i j)
⊢ (List.map r []).prod ∈ A (List.map i []).sum

Tactic:
rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ [], r j ∈ A (i j)
⊢ 1 ∈ A 0
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive ↑m
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
ℳ' : ι → AddSubmonoid M := fun i ↦ { carrier := ↑(ℳ i), add_mem' := ⋯, zero_mem' := ⋯ }
t : Decomposition ℳ'
mem : ∀ (m : M), m ∈ iSup ℳ'
⊢ ∀ (m : M), motive m

Tactic:
exact fun m ↦ @AddSubmonoid.iSup_induction _ _ _ ℳ' _ _ (mem m)
    (fun i m h ↦ homogeneous ⟨m, h⟩) zero add

Goal state after: