mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁷ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁶ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝¹⁵ : AddMonoid M
inst✝¹⁴ : HasShift C₁ M
inst✝¹³ : HasShift C₂ M
inst✝¹² : Φ.functor.CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst✝¹¹ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝¹⁰ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝⁹ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝⁸ : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
⊢ (SmallShiftedHom.equiv W₂ W₂.Q) (Φ.smallShiftedHomMap eX eZ (f.comp g h)) =
    (SmallShiftedHom.equiv W₂ W₂.Q) ((Φ.smallShiftedHomMap eX eY f).comp (Φ.smallShiftedHomMap eY eZ g) h)

Tactic:
let e := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)

Goal state after:
C₁ : Type u₁
inst✝¹⁷ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁶ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝¹⁵ : AddMonoid M
inst✝¹⁴ : HasShift C₁ M
inst✝¹³ : HasShift C₂ M
inst✝¹² : Φ.functor.CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst✝¹¹ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝¹⁰ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝⁹ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝⁸ : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ (SmallShiftedHom.equiv W₂ W₂.Q) (Φ.smallShiftedHomMap eX eZ (f.comp g h)) =
    (SmallShiftedHom.equiv W₂ W₂.Q) ((Φ.smallShiftedHomMap eX eY f).comp (Φ.smallShiftedHomMap eY eZ g) h)
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 : 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)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero (S.X₃.homology i)

Tactic:
· have := hS.epi_g
    have := HomologicalComplex.epi_homologyMap_of_epi_of_not_rel S.g i hi
    rw [IsZero.iff_id_eq_zero,
      ← cancel_epi (HomologicalComplex.homologyMap S.g i),
      ← cancel_epi (HomologicalComplex.homologyMap S.f i)]
    simp [← HomologicalComplex.homologyMap_comp]

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
j : ι
⊢ Epi (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j),
      y₂ ≫ L.d j (c.next j) = 0 →
        ∃ A' π,
          ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ K.d j (c.next j) = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.f j + y₁ ≫ L.d (c.prev j) j

Tactic:
apply ShortComplex.epi_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
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
⊢ π₂ ≫ π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ - π₂ ≫ f₂ ≫ φ.app ⟨2, ⋯⟩ = 0

Tactic:
h₁,

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
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
⊢ π₂ ≫ f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 - π₂ ≫ f₂ ≫ φ.app ⟨2, ⋯⟩ = 0
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
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝² : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
A₃ : C
π₃ : A₃ ⟶ A₂
w✝¹ : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w✝ : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13 ⟶ R₁.obj 1

Tactic:
exact R₁.map' 0 1

Goal state after:
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
a : A
b : B
h : b = φ a
⊢ shiftFunctor (PullbackShift C φ) a = shiftFunctor C b

Tactic:
subst h; rfl

Goal state after:
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₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y ≫ e₂.hom.app Y =
    ((shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
        (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app ((𝟭 D).obj Y)) ≫
      e₂.hom.app Y

Tactic:
simp only [Functor.comp_obj, Iso.inv_hom_id_app, Functor.id_obj, Functor.comp_map, assoc, comp_id,
    ← (shiftFunctor C a).map_comp, right_triangle_components, Functor.map_id]

Goal state after:
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₃
⊢ b₁ + b₂ = b₃

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₁ + b₂ = b₃
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:
rw [shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app_assoc,
    Functor.commShiftIso_hom_naturality_assoc, ← Functor.map_comp,
    left_triangle_components, Functor.map_id, comp_id]

Goal state after:
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 : C ⥤ D
inst✝ : G.CommShift B
x✝ : A
⊢ (Functor.commShiftIso (𝟭 (PullbackShift C φ)) x✝).hom ≫
      Functor.whiskerRight (PullbackShift.natIsoId C φ).hom (shiftFunctor (PullbackShift C φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natIsoId C φ).hom ≫
      (Functor.commShiftIso (PullbackShift.functor φ (𝟭 C)) x✝).hom

Tactic:
by
    ext
    simp [PullbackShift.natIsoId, Functor.commShiftPullback_iso_eq]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
r : CatCenter C
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ (r.localization L W).app (L.obj X) = L.map (r.app X)

Tactic:
dsimp [localization]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
r : CatCenter C
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ app (Localization.liftNatTrans L W L L (𝟭 D) (𝟭 D) (Functor.whiskerRight r L)) (L.obj X) = L.map (r.app X)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ : inv (Q.map π) = Q.map (section_ π)
h₂ : section_ π ≫ g = 0
⊢ inv (Q.map π) ≫ Q.map g = 0

Tactic:
h₁,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ : inv (Q.map π) = Q.map (section_ π)
h₂ : section_ π ≫ g = 0
⊢ Q.map (section_ π) ≫ Q.map g = 0
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
mem_ann : r ∈ Module.annihilator R ↑N
n : ℕ
h : ↑(AddCommGrpCat.of (Ext N M n))
this : r • 𝟙 N = 0
smul_eq : r • h = (mk₀ (r • 𝟙 N)).comp h ⋯
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ((mk₀ (r • 𝟙 M)).postcomp N ⋯))) h = (AddCommGrpCat.Hom.hom 0) h

Tactic:
simp [Ext.mk₀_smul, this, smul_eq]

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✝² : 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 ι)
hπ : IsSplitMono ι
h₁ : inv (Q.map ι) = Q.map (retraction ι)
h₂ : g ≫ retraction ι = 0
⊢ Q.map g ≫ inv (Q.map ι) = 0

Tactic:
h₁,

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 ι)
hπ : IsSplitMono ι
h₁ : inv (Q.map ι) = Q.map (retraction ι)
h₂ : g ≫ retraction ι = 0
⊢ Q.map g ≫ Q.map (retraction ι) = 0
Module: Mathlib.Algebra.CharP.Reduced

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (iterateFrobenius R p n) x = (iterateFrobenius R p n) y
⊢ x = y

Tactic:
by
  rw [← sub_eq_zero] at H ⊢
  simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H
  exact IsReduced.eq_zero _ ⟨_, H⟩

Goal state after:
Module: Mathlib.Algebra.CharP.Reduced

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ (x ^ m) ^ p ^ k = 1 ↔ x ^ m = 1

Tactic:
convert! ← (iterateFrobenius_inj R p k).eq_iff

Goal state after:
case e'_1.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p k) 1 = 1
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✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : { x // x ∈ nthRoots k 1 }
⊢ ↥(rootsOfUnity k R)

Tactic:
refine ⟨⟨x, ↑x ^ (k - 1 : ℕ), ?_, ?_⟩, ?_⟩
    all_goals
      rcases x with ⟨x, hx⟩; rw [mem_nthRoots <| NeZero.pos k] at hx
      simp only [← pow_succ, ← pow_succ', hx, tsub_add_cancel_of_le NeZero.one_le]
    simp only [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, hx, Units.val_one]

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

Goal state before:
pp: R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑(ζ ^ ↑(m % ↑(orderOf ζ)).toNat) = ↑↑ζ ^ m_1

Tactic:
zpow_natCast,

Goal state after:
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑(ζ ^ (m % ↑(orderOf ζ)).toNat) = ↑↑ζ ^ m_1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x : SpecialLinearGroup n R
x✝ : x ∈ center (SpecialLinearGroup n R)
⊢ x ∈ ⊥

Tactic:
by rw [mem_bot, Subsingleton.elim x 1]

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

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = ∏ x with x ≠ i₀, (D x)⁻¹
x : ι
hx : ¬x = i₀
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) x = D x

Tactic:
· simp [hx]

Goal state after:
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
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
⊢ C a

Tactic:
let of : { f : M →ₗ[R] s // ∀ m, f m * f m = Algebra.algebraMap _ _ (Q m) } :=
    ⟨(CliffordAlgebra.ι Q).codRestrict (Subalgebra.toSubmodule s) ι,
      fun m => Subtype.ext <| ι_sq_scalar Q m⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : { f // ∀ (m : M), f m * f m = (Algebra.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
⊢ C 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_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f (a + b) * f (a + b) - f a * f a - f b * f b =
    (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b)

Tactic:
by
      rw [hf, hf, hf]

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 ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ (diagonal D).det = 1

Tactic:
by simpa [hM] using M.2

Goal state after:
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 ↦ ⟨(f a).fst, (f a).snd⟩) l).prod

Tactic:
Sigma.eta

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

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A 0) (GAlgebra.toFun r) * (of A i) xi = (of A i) xi * (of A 0) (GAlgebra.toFun r)

Tactic:
of_mul_of,

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul (GAlgebra.toFun r) xi) = (of A i) xi * (of A 0) (GAlgebra.toFun r)
Module: Mathlib.Algebra.DirectSum.Ring

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

Tactic:
rw [pow_succ, n_ih, of_mul_of]

Goal state after:
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A (n • i + i)) (GradedMonoid.GMul.mul (GradedMonoid.GMonoid.gnpow n a) a) =
    (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ (toAddMonoid f) ((of A xi) xv * (of A yi) yv) = (toAddMonoid f) ((of A xi) xv) * (toAddMonoid f) ((of A yi) yv)

Tactic:
of_mul_of,

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ (toAddMonoid f) ((of A (xi + yi)) (GradedMonoid.GMul.mul xv yv)) =
    (toAddMonoid f) ((of A xi) xv) * (toAddMonoid f) ((of A yi) yv)
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
ι : Type u_8
Q : QuadraticMap R M N
s : Finset ι
f : ι → M
⊢ Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    simp_rw [Finset.sum_cons, QuadraticMap.map_add Q, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply, polar_self]
    abel_nf

Goal state after: