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

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{v_2, u_2} C₁
inst✝⁷ : Category.{v_3, u_3} C₂
inst✝⁶ : Category.{v_4, u_4} C₃
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Tactic:
let G := Φ.localizedFunctor L₁ L₂
  let G' := Ψ.localizedFunctor L₂ L₃
  let e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso _ _ _ _
  let e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso _ _ _ _
  rw [Φ.homMap_apply L₁ L₂ G e, Ψ.homMap_apply L₂ L₃ G' e',
    (Φ.comp Ψ).homMap_apply L₁ L₃ (G ⋙ G')
      (Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ e' ≪≫
      (Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight e _ ≪≫
      Functor.associator _ _ _)]
  dsimp
  simp only [Functor.map_comp, assoc, comp_id, id_comp]

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
⊢ (singleObjOpcyclesSelfIso c j A).hom ≫ opcyclesMap ((single C c j).map f) j = f ≫ (singleObjOpcyclesSelfIso c j B).hom

Tactic:
by
  rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
    single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
    singleObjOpcyclesSelfIso_hom, assoc]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
by
  constructor
  · intro h
    exact small_map (homEquiv W W.Q L).symm
  · intro h
    exact ⟨small_map (homEquiv W W.Q L)⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X Y'

Tactic:
by
  simp only [hasSmallLocalizedHom_iff W W.Q]
  exact small_congr (Iso.homCongr (Iso.refl _) (Localization.isoOfHom W.Q W f hf))

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁹ : AddMonoid M
inst✝⁸ : HasShift C M
inst✝⁷ : HasShift D M
L : C ⥤ D
inst✝⁶ : L.IsLocalization W
inst✝⁵ : L.CommShift M
X Y Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ (equiv W L) (f.comp g h) = ((equiv W L) f).comp ((equiv W L) g) h

Tactic:
dsimp [comp, equiv, ShiftedHom.comp]
  erw [SmallHom.equiv_comp]
  simp only [equiv_shift', Functor.comp_obj, assoc, Iso.inv_hom_id_app,
    comp_id, Functor.map_comp]
  rfl

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 : 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
this✝ : Epi S.g
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ IsZero (S.X₃.homology i)

Tactic:
rw [IsZero.iff_id_eq_zero,
      ← cancel_epi (HomologicalComplex.homologyMap S.g i),
      ← cancel_epi (HomologicalComplex.homologyMap S.f i)]

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 : 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
this✝ : Epi S.g
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i ≫ 𝟙 (S.X₃.homology i) =
    HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i ≫ 0
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:
by
  subst hi hk
  apply ShortComplex.mono_homologyMap_iff_up_to_refinements

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
this : 0 = comp 0 β ⋯
⊢ (hom 0).comp 0 ⋯ = 0

Tactic:
ShiftedHom.comp_zero

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
this : 0 = comp 0 β ⋯
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (triangleOfSES h₁).mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (Q.map f.τ₁) = Q.map f.τ₃ ≫ (triangleOfSES h₂).mor₃

Tactic:
dsimp [triangleOfSES, triangleOfSESδ]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (inv (Q.map (CochainComplex.mappingCone.descShortComplex S₁)) ≫
        Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₁.X₁) ≫
      (shiftFunctor (DerivedCategory C) 1).map (Q.map f.τ₁) =
    Q.map f.τ₃ ≫
      inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂)) ≫
        Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁
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) ⋯ +
        b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f 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:
inr_f_fst_v,

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) ⋯ + b ≫ S.X₂.d n₀ n₁ ≫ 0 =
      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
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
F : C ⥤ D
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝ : A
⊢ (Functor.commShiftIso (OppositeShift.functor A (F ⋙ G)) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natIsoComp A F G).hom (shiftFunctor (OppositeShift E A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natIsoComp A F G).hom ≫
      (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝).hom

Tactic:
ext
    dsimp [OppositeShift.natIsoComp, Functor.commShiftOp_iso_eq]
    simp only [Functor.map_id, comp_id, id_comp]
    rfl

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

Goal state before:
pp: R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
this : Linear R D := ⋯
⊢ autoParam (∀ {X Y : C} (f : X ⟶ Y) (r : R), L.map (r • f) = r • L.map f) Functor.Linear.map_smul._autoParam

Tactic:
intro X Y f r

Goal state after:
R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
this : Linear R D := linear R L W
X Y : C
f : X ⟶ Y
r : R
⊢ L.map (r • f) = r • L.map f
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
S T : Submodule R₁ M₁
u v : M₂
hu : u ∈ {y | ∀ x ∈ S, (B x) y = 0}
hv : v ∈ {y | ∀ x ∈ S, (B x) y = 0}
x : M₁
hx : x ∈ S
⊢ (B x) (u + v) = 0

Tactic:
by simp [hu _ hx, hv _ hx]

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

Goal state before:
pp: case mpr
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
⊢ M.det ≠ 0

Tactic:
have : Function.Injective (Matrix.toLin' M) := by
      simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h

Goal state after:
case mpr
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
this : Function.Injective ⇑(toLin' M)
⊢ M.det ≠ 0
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
u : Rˣ
A : GL n R
⊢ (Matrix.scalar n) ↑u * ↑A = ↑A * (Matrix.scalar n) ↑u

Tactic:
Matrix.scalar_comm _ (Commute.all _)

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
u : Rˣ
A : GL n R
⊢ ↑A * (Matrix.scalar n) ↑u = ↑A * (Matrix.scalar n) ↑u
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case inl
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
exact ⟨by aesop, by simp [Subsingleton.elim A 1]⟩

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
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * ((ι Q) a * ((ι Q) b * y)) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)

Tactic:
← mul_assoc _ _ y,

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
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * ((ι Q) a * (ι Q) b * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ ↑T⁻¹ = !![1, -1; 0, 1]

Tactic:
simp [coe_inv, coe_T, adjugate_fin_two]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ ∑ x, ∑ x_1, σ₁ ((Finsupp.single i 1) x) •> (Finsupp.single j 1) x_1 •> M x x_1 = M i j

Tactic:
rw [Finset.sum_eq_single_of_mem i (by simp) fun k _ hk ↦ by simp [hk],
    Finset.sum_eq_single_of_mem j (by simp) fun k _ hk ↦ by simp [hk]]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ σ₁ ((Finsupp.single i 1) i) •> (Finsupp.single j 1) j •> M i j = M i j
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 : A 0
n : ℕ
⊢ (of A 0) (a ^ (n + 1)) = (of A 0) a ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ 2 • Q₁ = 2 • Q₂

Tactic:
show (2 : R) = (2 : ℕ) by rfl

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ ↑2 • Q₁ = ↑2 • Q₂
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n : ℕ
⊢ ↑n ∈ A 0

Tactic:
induction n with
  | zero =>
    rw [Nat.cast_zero]
    exact zero_mem (A 0)
  | succ _ n_ih =>
    rw [Nat.cast_succ]
    exact add_mem n_ih (SetLike.one_mem_graded _)

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

Goal state before:
pp: case mpr
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : M₁ →ₗ[R] M₂ →ₗ[R] R
h : (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'
⊢ B = B'

Tactic:
exact (LinearMap.toMatrix₂ b₁ b₂).injective h

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
⊢ ∃ x, Q x ≠ 0

Tactic:
rw [← not_forall]
  intro h
  apply hB₁
  rw [(QuadraticMap.ext h : Q = 0), map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

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
⊢ Submodule.comap reverse (ι Q).range = (ι Q).range

Tactic:
← submodule_map_reverse_eq_comap,

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
⊢ Submodule.map reverse (ι Q).range = (ι Q).range
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
⊢ (toMatrix (Pi.basisFun R n) Q).det = Q.toMatrix'.det

Tactic:
toMatrix_eq_toMatrix'

Goal state after:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
⊢ Q.toMatrix'.det = Q.toMatrix'.det
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

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
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.comap reverse (p * q) = Submodule.comap reverse q * Submodule.comap reverse p

Tactic:
← submodule_map_reverse_eq_comap,

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
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

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
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.comap reverse (p ^ n) = Submodule.comap reverse p ^ n

Tactic:
← submodule_map_reverse_eq_comap,

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
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

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
n : ZMod 2
⊢ Submodule.comap reverse (evenOdd Q n) = evenOdd Q n

Tactic:
← submodule_map_reverse_eq_comap,

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
n : ZMod 2
⊢ Submodule.map reverse (evenOdd Q n) = evenOdd Q n
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ (ι Q).range ^ (2 * k + n.val)), motive xv ⋯

Tactic:
pow_add,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ (ι Q).range ^ (2 * k) * (ι Q).range ^ n.val), motive xv ⋯
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
m₁ m₂ : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
i : ℕ
⊢ (f i.succ).curryLeft (m₁ + m₂) = ((fun i ↦ (f i.succ).curryLeft m₁) + fun i ↦ (f i.succ).curryLeft m₂) i

Tactic:
simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
i : ℕ
⊢ (f i.succ).curryLeft (c • m) = (c • fun i ↦ (f i.succ).curryLeft m) i

Tactic:
simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case refine_1.refine_3
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
m : M
f₁ f₂ : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
i : ℕ
⊢ ((f₁ + f₂) i.succ).curryLeft m = ((fun i ↦ (f₁ i.succ).curryLeft m) + fun i ↦ (f₂ i.succ).curryLeft m) i

Tactic:
simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]

Goal state after: