mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (inl φ).v p p ⋯ ≫ (snd φ).v p q hpq = 0

Tactic:
obtain rfl : q = p + -1 := by lia
  simp [inl, snd, Cochain.rightShift_v (n := -1) _ _ _ _ p _ _ (p + -1) (by lia),
    Cochain.leftShift_v _ _ _ _ _ _ hpq]

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 : ℤ
α : Cocycle M K n
β : Cochain M L m
h : m + 1 = n
hαβ : δ m n β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
⊢ liftCochain φ (↑α) β h ∈ cocycle M (mappingCocone φ) n

Tactic:
by simp [Cocycle.mem_iff _ _ rfl, δ_liftCochain _ _ _ _ _ rfl, hαβ]

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 (DerivedCategory C)
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
⊢ (homologyFunctor C n₀).map T.mor₁ ≫ (homologyFunctor C n₀).map T.mor₂ = 0

Tactic:
simp only [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT,
        Functor.map_zero]

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

Goal state before:
pp: case pos.e_a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
⊢ i = k

Tactic:
simpa using hi.symm

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

Goal state before:
pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
k : ι
⊢ ¬c'.Rel (e.f j) (e.f k)

Tactic:
hk

Goal state after:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
k : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ False
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
⊢ ¬c.Rel j (c.next j)

Tactic:
hk

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
⊢ ¬c.Rel j k
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ ¬c.Rel j (c.next j)

Tactic:
hk

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ ¬c.Rel j k
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
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
⊢ k = c.next j

Tactic:
hk

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
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
⊢ k = k
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionToTruncGE' e).f i)

Tactic:
rw [K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi]
  infer_instance

Goal state after:
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 : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (truncGE'Map ((opFunctor C c').map φ.op) e.op).f i =
    (L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫
      (L.opcyclesOpIso i').hom ≫
        (cyclesMap φ i').op ≫ (K.opcyclesOpIso i').inv ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv

Tactic:
truncGE'Map_f_eq_opcyclesMap _ e.op (by simpa) h,

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.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫
      opcyclesMap ((opFunctor C c').map φ.op) i' ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv =
    (L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫
      (L.opcyclesOpIso i').hom ≫
        (cyclesMap φ i').op ≫ (K.opcyclesOpIso i').inv ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case mp
ι : 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
⊢ QuasiIso (K.πTruncGE e) → K.IsSupported e

Tactic:
intro
    refine ⟨fun i' hi' => ?_⟩
    rw [exactAt_iff_of_quasiIsoAt (K.πTruncGE e) i']
    exact (K.truncGE e).exactAt_of_isSupported e i' hi'

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

Goal state before:
pp: case inr.inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ (mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯).f i = (𝟙 K).f i

Tactic:
· apply (K.isZero_of_isStrictlyLE n i (by lia)).eq_of_tgt

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

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

Tactic:
have := hS₂.epi_g

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inl S₁.f).v (n + 1) n ⋯ ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inl S₁.f).v (n + 1) n ⋯ ≫ (descShortComplex S₁ ≫ f.τ₃).f n

pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inr S₁.f).f n ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inr S₁.f).f n ≫ (descShortComplex S₁ ≫ f.τ₃).f n

Tactic:
· simp [map]

Goal state after:
case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inr S₁.f).f n ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inr S₁.f).f n ≫ (descShortComplex S₁ ≫ f.τ₃).f n
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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂ = e₂'

Tactic:
by
  rw [← Iso.symm_eq_iff]
  ext
  rw [Iso.symm_hom, Iso.symm_hom, compatibilityUnit_right adj e₁ e₂ h,
    compatibilityUnit_right adj e₁ e₂' h']

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

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

Tactic:
· refine exact₂_mk _ (by simp) ?_
      rwa [ShortComplex.exact_iff_mono _ (by simp)]

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 Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
              (shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          (Quiver.Hom.unop g ≫
            ((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
              (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
← unop_comp_assoc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
              (shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y) ≫ g).unop ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

Tactic:
· refine exact₂_mk _ (by simp) ?_
      rwa [ShortComplex.exact_iff_mono _ (by simp)]

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : R
⊢ a • 0 = 0

Tactic:
by
      simp only [smulOfRingMorphism_smul_eq, comp_zero]

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

Goal state before:
pp: 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
X Y : C
n : ℕ
⊢ Small.{w, max u v} (Ext X Y n)

Tactic:
induction n generalizing X Y with

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughInjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
n : ℕ
⊢ Small.{w, max u v} (Ext X Y n)

Tactic:
induction n generalizing X Y with

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

Goal state before:
pp: m : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
hM : M.det ∈ R⁰
x✝¹ x✝ : m → R
hxy : M *ᵥ x✝¹ = M *ᵥ x✝
⊢ M *ᵥ (x✝¹ - x✝) = 0

Tactic:
mulVec_sub,

Goal state after:
m : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
hM : M.det ∈ R⁰
x✝¹ x✝ : m → R
hxy : M *ᵥ x✝¹ = M *ᵥ x✝
⊢ M *ᵥ x✝¹ - M *ᵥ x✝ = 0
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
hg' : (algebraMap R[X] K) g ≠ 0
⊢ (algebraMap R[X] K) f = (algebraMap R[X] K) (f %ₘ g) + (algebraMap R[X] K) (g * (f /ₘ g))

Tactic:
← map_add,

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
hg' : (algebraMap R[X] K) g ≠ 0
⊢ (algebraMap R[X] K) f = (algebraMap R[X] K) (f %ₘ g + g * (f /ₘ g))
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ b.toMatrix ⇑(Pi.basisFun R ι) * A = of fun i j ↦ (b.repr (A.col j)) i

Tactic:
by
  classical
  simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
  ext i j
  rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]

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

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ Matrix.toLin' ↑A⁻¹ ∘ₗ Matrix.toLin' ↑A = LinearMap.id

Tactic:
rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one]

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

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : ↥(center (SpecialLinearGroup n R))
⊢ ↑↑A = (scalar n) ↑↑(center_equiv_rootsOfUnity A)

Tactic:
unfold center_equiv_rootsOfUnity Or.by_cases

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : ↥(center (SpecialLinearGroup n R))
⊢ ↑↑A =
    (scalar n)
      ↑↑((if hp : IsEmpty n then (fun hn ↦ ⋯.mpr (⋯.mpr (⋯.mpr (⋯.mpr MulEquiv.ofUnique)))) hp
            else (fun x ↦ ⋯ ▸ center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯)
            A)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
x y : TensorAlgebra R M
h : Rel Q x y
⊢ (RingCon.ker ((TensorAlgebra.lift R) ↑f).toRingHom) x y

Tactic:
induction h
          simp [f.prop]

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ ↑(transvection hij b * transvection hij (-b)) = ↑1

Tactic:
simp [transvection_coe, mul_add, add_mul,
    single_mul_single_of_ne _ _ _ _ hij.symm, ← single_neg]

Goal state after:
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 with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D

Tactic:
det_diagonal,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : ∏ i, D i = 1
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
hD : (diagonal D).det = 1
j : ι
h : D j = 0
⊢ False

Tactic:
det_diagonal,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
hD : ∏ i, D i = 1
j : ι
h : D j = 0
⊢ False
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
⊢ ∑ x, (if i = x then 1 else 0) •> ∑ x_1, (if j = x_1 then 1 else 0) •> f x x_1 = f i j

Tactic:
simp only [ite_smul, one_smul, zero_smul, sum_ite_eq, mem_univ, ↓reduceIte]

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

Goal state before:
pp: case h
n : Type u_11
m : Type u_12
n' : Type u_13
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 n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m),
    ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •> 0 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) = 0

Tactic:
· intros
      simp only [zero_smul, smul_zero]

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
a b c : ⨁ (i : ι), A i
⊢ a * b * c = a * (b * c)

Tactic:
suffices AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃ by
      simpa only [AddMonoidHom.mulLeft₃_apply, AddMonoidHom.mulRight₃_apply] using
        DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
⊢ AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: case h
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m), (b₁.repr (l (b₁' i))) i' •> 0 •> (B (b₁ i')) (b₂ i_1) = 0

Tactic:
· intros
      simp only [zero_smul, smul_zero]

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

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : Semiring A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ ↑(((decompose 𝒜) ((decompose 𝒜).symm a)) i) = (decompose 𝒜).symm ((of (fun i ↦ ↥(𝒜 i)) i) (a i))

Tactic:
decompose_symm_of,

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : Semiring A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ ↑(((decompose 𝒜) ((decompose 𝒜).symm a)) i) = ↑(a i)