mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    iCycles K i ≫
      (iCyclesIso K i (i + 1) ⋯ ⋯).inv ≫
        (homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom) ≫
          (singleObjXSelf (ComplexShape.up ℤ) i P).inv

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    iCycles K i ≫
      (iCyclesIso K i (i + 1) ⋯ ⋯).inv ≫
        homologyπ K i ≫
          (homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom) ≫
            (singleObjXSelf (ComplexShape.up ℤ) i P).inv
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    iCycles K i ≫
      (iCyclesIso K i (i + 1) ⋯ ⋯).inv ≫
        homologyπ K i ≫
          (homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom) ≫
            (singleObjXSelf (ComplexShape.up ℤ) i P).inv

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    iCycles K i ≫
      (iCyclesIso K i (i + 1) ⋯ ⋯).inv ≫
        homologyπ K i ≫
          homologyMap π i ≫
            (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ ((singleObjXSelf (ComplexShape.up ℤ) i P).hom ≫ Projective.factorThru (𝟙 P) α) ≫ π.f i =
    (𝟙 ((singleFunctor C i).obj P)).f i

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ (singleObjXSelf (ComplexShape.up ℤ) i P).hom ≫ Projective.factorThru (𝟙 P) α ≫ π.f i =
    (𝟙 ((singleFunctor C i).obj P)).f i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

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

Tactic:
let S := ShortComplex.mk _ _ (kernel.condition (Projective.π X))

Goal state after:
case succ
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
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := kernel (Projective.π X), X₂ := Projective.over X, X₃ := X, f := kernel.ι (Projective.π X),
    g := Projective.π X, zero := ⋯ }
⊢ Small.{w, max u v} (Ext X Y (n + 1))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    ((singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
        (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
          homologyMap ι i ≫ homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv) ≫
      pOpcycles L i

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      ((singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
          homologyMap ι i ≫ homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv) ≫
        pOpcycles L i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      ((singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
          homologyMap ι i ≫ homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv) ≫
        pOpcycles L i

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
        (homologyMap ι i ≫ homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv) ≫ pOpcycles L i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
        (homologyMap ι i ≫ homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv) ≫ pOpcycles L i

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
        homologyMap ι i ≫ (homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv) ≫ pOpcycles L i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
        homologyMap ι i ≫ (homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv) ≫ pOpcycles L i

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
        homologyMap ι i ≫ homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv ≫ pOpcycles L i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ ((singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α) ≫
      Injective.factorThru (𝟙 I) α ≫ (singleObjXSelf (ComplexShape.up ℤ) i I).inv =
    𝟙 (((singleFunctor C i).obj I).X i)

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      α ≫ Injective.factorThru (𝟙 I) α ≫ (singleObjXSelf (ComplexShape.up ℤ) i I).inv =
    𝟙 (((singleFunctor C i).obj I).X i)
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ Submodule.Quotient.mk (relations.relation r) = 0

Tactic:
Submodule.Quotient.mk_eq_zero

Goal state after:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.relation r ∈ Submodule.span A (Set.range relations.relation)
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
g : relations.G
⊢ (h.desc s) (solution.var g) = s.var g

Tactic:
dsimp [desc]

Goal state after:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
g : relations.G
⊢ s.fromQuotient (h.linearEquiv.symm (solution.var g)) = s.var g
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Finite ι
inst✝ : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this : b₁.toMatrix ⇑b₂ * (toMatrix b₃ b₂) ((toLin b₃ b₂) A) = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
⊢ b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)

Tactic:
rwa [LinearMap.toMatrix_toLin] at this

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

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val✝ : Fintype κ
this : (toMatrix b₁ b₃) ((toLin b₁ b₃) A) * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)

Tactic:
rwa [LinearMap.toMatrix_toLin] at this

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
hn : IsEmpty n
⊢ (∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A) → A ∈ center (SpecialLinearGroup n R)

Tactic:
by simp [Subsingleton.elim A 1]

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
S : Type u_1
inst✝ : CommRing S
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
B : SpecialLinearGroup n R
⊢ ↑(B * ⟨a • 1, ⋯⟩) = ↑(⟨a • 1, ⋯⟩ * B)

Tactic:
by simp [coe_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
⊢ IsCoprime ((↑A *ᵥ v) 0) ((↑A *ᵥ v) 1)

Tactic:
by
  simpa only [← vecMul_transpose] using! hab.vecMulSL A.transpose

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

Goal state before:
pp: case mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
hx : x ∈ Algebra.adjoin R (Set.range ⇑(ι Q))
hy : y ∈ Algebra.adjoin R (Set.range ⇑(ι Q))
⊢ x * y ∈ Algebra.adjoin R (Set.range ⇑(ι Q))

Tactic:
| mul x y hx hy =>

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

Goal state before:
pp: case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ (diagonalRingHom ι F) D = (diagonalRingHom ι F) ({i | i ≠ i₀}.prod g)

Tactic:
diag_decompose i₀ D hD

Goal state after:
case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ (diagonalRingHom ι F) D = (diagonalRingHom ι F) D
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
ext x y z

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : Std.Associative fun x y ↦ x * y
⊢ mulLeft₃ = mulRight₃

Tactic:
ext x y z

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : Std.Associative fun x y ↦ x * y
x y z : R
⊢ ((mulLeft₃ x) y) z = ((mulRight₃ x) y) z
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
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
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) + Q (∑ i ∈ s, f i) + polar (⇑Q) (f a) (∑ i ∈ s, f i) =
    Q (f a) + ∑ i ∈ s, Q (f i) + ∑ ij ∈ (Finset.cons a s ha).sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)

Tactic:
ih,

Goal state after:
case cons
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
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) + (∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)) +
      polar (⇑Q) (f a) (∑ i ∈ s, f i) =
    Q (f a) + ∑ i ∈ s, Q (f i) + ∑ ij ∈ (Finset.cons a s ha).sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
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
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + Q (∑ i ∈ s, f i) + polar (⇑Q) (f a) (∑ i ∈ s, f i) =
    ∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q) (Sym2.map f ij) - (Q (f a) + ∑ i ∈ s, Q (f i))

Tactic:
ih,

Goal state after:
case cons
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
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + (∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)) + polar (⇑Q) (f a) (∑ i ∈ s, f i) =
    ∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q) (Sym2.map f ij) - (Q (f a) + ∑ i ∈ s, Q (f i))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
Q : QuadraticMap R N P
f : M →ₗ[R] N
B : BilinMap R N P
h : ∀ (x y : N), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ Q (f (x + y)) = Q (f x) + Q (f y) + ((LinearMap.compl₁₂ B f f) x) y

Tactic:
simp_rw [f.map_add]

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
Q : QuadraticMap R N P
f : M →ₗ[R] N
B : BilinMap R N P
h : ∀ (x y : N), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ Q (f x + f y) = Q (f x) + Q (f y) + ((LinearMap.compl₁₂ B f f) x) y
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
x✝³ x✝² : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((⅟2 • (x✝³ + x✝²).polarBilin) x✝¹) x✝ = ((⅟2 • x✝³.polarBilin + ⅟2 • x✝².polarBilin) x✝¹) x✝

Tactic:
by simp [polar_add]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ (∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
      if x.1 + x.2 = n then ↑(GradedMonoid.GMul.mul (r x.1) (r' x.2)) else ↑0) =
    ∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with x.1 + x.2 = n, ↑(r x.1) * ↑(r' x.2)

Tactic:
ZeroMemClass.coe_zero,

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ (∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
      if x.1 + x.2 = n then ↑(GradedMonoid.GMul.mul (r x.1) (r' x.2)) else 0) =
    ∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with x.1 + x.2 = n, ↑(r x.1) * ↑(r' x.2)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑0 * ↑rj else 0) = 0

Tactic:
ZeroMemClass.coe_zero,

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then 0 * ↑rj else 0) = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∉ DFinsupp.support r'
⊢ 0 = ↑r * ↑0

Tactic:
ZeroMemClass.coe_zero,

Goal state after:
case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∉ DFinsupp.support r'
⊢ 0 = ↑r * 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0

Tactic:
ZeroMemClass.coe_zero,

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then ↑x₁ * 0 else 0) = 0