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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
⊢ ⋯.δ i' j' hij' = 0

Tactic:
by_cases hj : ∃ j, e.f j = j'

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
hj : ∃ j, e.f j = j'
⊢ ⋯.δ i' j' hij' = 0

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
hj : ¬∃ j, e.f j = j'
⊢ ⋯.δ i' j' hij' = 0
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₂ : ι₂
h : Sum.inr i₂ = i
⊢ ac.desc' x₁ x₂ i = (desc.aux X (e₂.f i₂) (ac.equiv i) ⋯) (x₂ i₂)

Tactic:
by subst h; rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjCyclesSelfIso c j A).inv ≫ cyclesMap ((single C c j).map f) j = f ≫ (singleObjCyclesSelfIso c j B).inv

Tactic:
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc,
    ← singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

Goal state after:
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
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_mono (HomologicalComplex.homologyMap S.f j)]

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
this : HasDerivedCategory C := ⋯
⊢ (mk₀ 0).hom = hom 0

Tactic:
simp [zero_hom']

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

Tactic:
rw [← cancel_epi π₁, comp_zero, hf₁, ← cancel_epi π₂, ← cancel_epi π₃, comp_zero,
    comp_zero, ← reassoc_of% h₄, ← R₁.map'_comp 0 1 2, hR₁, comp_zero]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ hS.extClass.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
by
  let := HasDerivedCategory.standard C
  ext
  simp only [Ext.comp_hom, Ext.mk₀_hom, extClass_hom, Ext.zero_hom,
    ShiftedHom.comp_mk₀]
  exact comp_distTriang_mor_zero₃₁ _ hS.singleTriangle_distinguished

Goal state after:
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 : ℤ
⊢ ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast.map' 1 2
        _proof_246✝ _proof_363✝ ≫
      (homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n =
    (homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂ ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 1 2 _proof_246✝ _proof_363✝

Tactic:
erw [(homologyFunctorFactors C (up ℤ) n).hom.naturality_assoc]
          -- Disable `Fin.reduceFinMk`, otherwise `Precomp.obj_succ` does not fire. (https://github.com/leanprover-community/mathlib4/issues/27382)
          dsimp [-Fin.reduceFinMk]
          rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex]

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:
by subst h; rfl

Goal state after:
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₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n = (descShortComplex S₁ ≫ f.τ₃).f n

Tactic:
apply ext_from _ (n + 1) n rfl

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 : ℤ
⊢ (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

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.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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
⊢ IsIso (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)

Tactic:
by
  let ψ : mk₄ (R₁.map' 0 1) (R₁.map' 1 2) (0 : _ ⟶ (0 : C)) (0 : _ ⟶ (0 : C)) ⟶
      mk₄ (R₂.map' 0 1) (R₂.map' 1 2) (0 : _ ⟶ (0 : C)) (0 : _ ⟶ (0 : C)) :=
    homMk₄ (app' φ 0) (app' φ 1) (app' φ 2) 0 0 (naturality' φ 0 1)
      (naturality' φ 1 2) (by simp) (by simp)
  refine isIso_of_epi_of_isIso_of_isIso_of_mono ?_ ?_ ψ h₀ h₁ inferInstance inferInstance
  · refine exact_of_δ₀ (hR₁.exact 0).exact_toComposableArrows (exact_of_δ₀ ?_ ?_)
    · refine exact₂_mk _ (by simp) ?_
      rwa [ShortComplex.exact_iff_epi _ (by simp)]
    · refine exact₂_mk _ (by simp) ?_
      rw [ShortComplex.exact_iff_epi _ (by simp)]
      infer_instance
  · refine exact_of_δ₀ (hR₂.exact 0).exact_toComposableArrows (exact_of_δ₀ ?_ ?_)
    · refine exact₂_mk _ (by simp) ?_
      rwa [ShortComplex.exact_iff_epi _ (by simp)]
    · refine exact₂_mk _ (by simp) ?_
      rw [ShortComplex.exact_iff_epi _ (by simp)]
      infer_instance

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

Tactic:
F.commShiftIso_add

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (Functor.commShiftIso F a) (Functor.commShiftIso F b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
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
  | zero =>
    rw [small_congr Ext.homEquiv₀]
    infer_instance
  | succ n hn =>
    let S := ShortComplex.mk _ _ (kernel.condition (Projective.π X))
    have hS : S.ShortExact :=
      { exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel S.g) }
    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)
    exact small_of_surjective.{w} this

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
N M : ModuleCat R
inst✝¹ : Module.Finite R ↑N
inst✝ : Module.Finite R ↑M
i : ℕ
⊢ Module.Finite R (Ext N M i)

Tactic:
induction i generalizing N with

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

Goal state before:
pp: case inr.inr.refine_1
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
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ -1 • v ᵥ* A = 0

Tactic:
h_vA,

Goal state after:
case inr.inr.refine_1
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
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ -1 • 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case inr.refine_1
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ ↑A i i ^ Fintype.card n = 1

pp: case inr.refine_2
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ (scalar n) (↑A i i) = ↑A

pp: case inr.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ B * A = A * B

Tactic:
· have : det ((scalar n) (A i i)) = 1 := (scalar_eq_self_of_mem_center h i).symm ▸ A.property
    simpa using! this

Goal state after:
case inr.refine_2
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ (scalar n) (↑A i i) = ↑A

case inr.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ B * A = A * B
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
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
by
  rcases isEmpty_or_nonempty n with hn | ⟨⟨i⟩⟩; · exact ⟨by aesop, by simp [Subsingleton.elim A 1]⟩
  refine ⟨fun h ↦ ⟨A i i, ?_, ?_⟩, fun ⟨r, _, hr⟩ ↦ Subgroup.mem_center_iff.mpr fun B ↦ ?_⟩
  · have : det ((scalar n) (A i i)) = 1 := (scalar_eq_self_of_mem_center h i).symm ▸ A.property
    simpa using! this
  · exact scalar_eq_self_of_mem_center h i
  · suffices ↑ₘ(B * A) = ↑ₘ(A * B) from Subtype.val_injective this
    simpa only [coe_mul, ← hr] using! (scalar_commute (n := n) r (Commute.all r) B).symm

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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ (F.toLinearMap ∘ₗ ι Q) m * (F.toLinearMap ∘ₗ ι Q) m = (algebraMap R A) (Q m)

Tactic:
rw [LinearMap.comp_apply, AlgHom.toLinearMap_apply, comp_ι_sq_scalar]

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

Goal state before:
pp: case pos
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

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:
· simpa [hx, hD, -Finset.prod_inv_distrib] using Finset.prod_congr rfl (by grind)

Goal state after:
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
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
h : Std.Associative fun x y ↦ x * y
x y z : R
⊢ associator x y z = 0 x y z

Tactic:
simp [associator, Std.Associative.assoc]

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

Goal state before:
pp: n : ℤ
g : SL(2, ℤ)
⊢ ↑(T ^ n * g) 1 = ↑g 1

Tactic:
ext j
  simp [coe_T_zpow, Matrix.vecMul, dotProduct, Fin.sum_univ_succ]

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
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
exact of_eq_of_gradedMonoid_eq (one_mul <| GradedMonoid.mk i xi)

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

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

Tactic:
exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm

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✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 0
⊢ ↑(((decompose 𝒜) (a * b)) j) = a * ↑(((decompose 𝒜) b) j)

Tactic:
by
  lift a to 𝒜 0 using a_mem
  rw [decompose_mul, decompose_coe, coe_of_mul_apply_of_mem_zero]

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁

Tactic:
by
  rw [selfAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule, Matrix.IsSelfAdjoint]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ (∏ xn ∈ s, xn.1) n = 0

Tactic:
by
  simpa using listProd_apply_eq_zero' (l := s.toList) (by simpa using hs) (by simpa)

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (range fun x ↦ (ExteriorAlgebra.ιMulti R n) x) = ⋀[R]^n M

Tactic:
exact ExteriorAlgebra.ιMulti_span_fixedDegree R n

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ (ConcreteCategory.hom (ε (restrictScalars f))) r = f r

Tactic:
let := f.toAlgebra

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ (ConcreteCategory.hom (ε (restrictScalars f))) r = f r
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
I B : C
t : IsInitial I
inst✝ : MonoidalClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
this : IsIso g
⊢ g = h

Tactic:
have := strict_initial t h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
I B : C
t : IsInitial I
inst✝ : MonoidalClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
this✝ : IsIso g
this : IsIso h
⊢ g = h
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁸ : Category.{v_1, u_1} J
inst✝⁷ : Category.{v_2, u_2} C
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Category.{v_4, u_4} E
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory E
K : Type u_5
inst✝² : Category.{v_5, u_5} K
inst✝¹ : HasColimitsOfShape K C
inst✝ : ∀ (X : C), PreservesColimitsOfShape K (tensorLeft X)
F : J ⥤ C
k : J
this : tensorLeft F ⋙ (evaluation J C).obj k ≅ (evaluation J C).obj k ⋙ tensorLeft (F.obj k)
⊢ PreservesColimitsOfShape K (tensorLeft F ⋙ (evaluation J C).obj k)

Tactic:
exact preservesColimitsOfShape_of_natIso this.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ autoParam (∀ {K : Discrete WalkingPair ⥤ C ⥤ Type u}, PreservesLimit K colim)
    PreservesLimitsOfShape.preservesLimit._autoParam

Tactic:
intro F

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
F : Discrete WalkingPair ⥤ C ⥤ Type u
⊢ PreservesLimit F colim
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
c x✝ : C
x : Over c
s s' : (forget c).obj x ⟶ x✝
⊢ ∃ c' t, (forget c).map t ≫ s = (forget c).map t ≫ s'

Tactic:
use mk (IsCofiltered.eqHom s s' ≫ x.hom)

Goal state after:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
c x✝ : C
x : Over c
s s' : (forget c).obj x ⟶ x✝
⊢ ∃ t, (forget c).map t ≫ s = (forget c).map t ≫ s'
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : C
x : ↑(M.obj (Opposite.op X))
⊢ (ConcreteCategory.hom ((freeYonedaEquiv.symm x).app (Opposite.op X)))
      (ModuleCat.freeMk (𝟙 (Opposite.unop (Opposite.op X)))) =
    x

Tactic:
by
  simp [freeYonedaEquiv, freeHomEquiv, yonedaEquiv]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal

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
R : Dᵒᵖ ⥤ CommRingCat
x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (isoMk (fun x ↦ Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj x✝¹).obj x))
            ⋯).hom ▷
        (pushforward₀OfCommRingCat F R).obj x✝ ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj (x✝² ⊗ x✝¹) ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((pushforward₀OfCommRingCat F R).obj x✝²) ((pushforward₀OfCommRingCat F R).obj x✝¹)
          ((pushforward₀OfCommRingCat F R).obj x✝)).hom ≫
      (pushforward₀OfCommRingCat F R).obj x✝² ◁
          (isoMk
              (fun x ↦
                Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝¹ ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
              ⋯).hom ≫
        (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj (x✝¹ ⊗ x✝)).obj x))
            ⋯).hom

Tactic:
ext1
        exact tensor_ext₃' fun m₁ m₂ m₃ ↦ rfl

Goal state after: