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

Goal state before:
pp: case e_β
C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this✝⁵ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
this✝⁴ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
this✝³ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) Z'
this✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
this✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Z'
this✝ : HasSmallLocalizedHom W₂ Y' (Φ.functor.obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Y)
⊢ (Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom) =
    (SmallHom.mk W₂ (eY.hom ≫ eY.inv)).comp ((Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom))

Tactic:
eY.hom_inv_id,

Goal state after:
case e_β
C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this✝⁵ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
this✝⁴ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
this✝³ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) Z'
this✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
this✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Z'
this✝ : HasSmallLocalizedHom W₂ Y' (Φ.functor.obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Y)
⊢ (Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom) =
    (SmallHom.mk W₂ (𝟙 (Φ.functor.obj Y))).comp ((Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom))
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: 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
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
⊢ S.X₁.ExactAt j

Tactic:
rw [exactAt_iff_isZero_homology]

Goal state after:
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
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
⊢ IsZero (S.X₁.homology j)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ HasExt C

Tactic:
hasExt_iff.{w}

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: 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)
⊢ S.X₃.ExactAt i

Tactic:
rw [exactAt_iff_isZero_homology]

Goal state after:
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)
⊢ IsZero (S.X₃.homology i)
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₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ 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 (CochainComplex.mappingCone.descShortComplex S₁) ≫
      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₁

Tactic:
← Functor.comp_map,

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

Tactic:
let α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α (zero_add n)

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 X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
⊢ (α + β).hom = α.hom + β.hom
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ (shiftFunctorAdd' (OppositeShift C A) a b (a + b) ⋯).hom.app X =
    ((shiftFunctorAdd' C a b (a + b) ⋯).inv.app (Opposite.unop X)).op

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, oppositeShiftFunctorAdd_hom_app]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
X Y : Cᵒᵖ
f : Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y
⊢ (shiftFunctor C n).map (opShiftFunctorEquivalenceSymmHomEquiv f).unop =
    ((opShiftFunctorEquivalence C n).unitIso.hom.app Y).unop ≫ f.unop

Tactic:
rw [← opShiftFunctorEquivalenceSymmHomEquiv_left_inv]
  simp

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✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctorCompIsoId C (-a) a ⋯).inv.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
        (shiftFunctor C a).map ((shiftFunctor C (-a)).map ((Functor.commShiftIso G a).inv.app (F.obj X✝))) ≫
          (shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝))) ≫
            (Functor.commShiftIso G a).hom.app (F.obj X✝)

Tactic:
← Functor.comp_map,

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✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctorCompIsoId C (-a) a ⋯).inv.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
        (shiftFunctor C (-a) ⋙ shiftFunctor C a).map ((Functor.commShiftIso G a).inv.app (F.obj X✝)) ≫
          (shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝))) ≫
            (Functor.commShiftIso G a).hom.app (F.obj X✝)
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ G.map e.inv ≫ G.map (L.map (r • 𝟙 (L.objPreimage X))) ≫ G.map e.hom = r • 𝟙 (G.obj X)

Tactic:
← Functor.comp_map,

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ G.map e.inv ≫ (L ⋙ G).map (r • 𝟙 (L.objPreimage X)) ≫ G.map e.hom = r • 𝟙 (G.obj X)
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ⇑f
n : ℕ
hn : 0 < n
g₀ : G
⊢ #{g | g ^ n = g₀} ≤ (nthRoots n (f g₀)).card

Tactic:
have : DecidableEq R := Classical.decEq _
  calc
    _ ≤ #(nthRoots n (f g₀)).toFinset :=
      card_le_card_of_injOn f (by aesop (add safe unfold Set.MapsTo)) hf.injOn
    _ ≤ _ := (nthRoots n (f g₀)).toFinset_card_le

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

Goal state before:
pp: case refine_1
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 : R
hx : x ∈ nthRoots k 1
⊢ ↑⟨x, hx⟩ * ↑⟨x, hx⟩ ^ (k - 1) = 1

Tactic:
rw [mem_nthRoots <| NeZero.pos k] at hx

Goal state after:
case refine_1
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 : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ ↑⟨x, hx✝⟩ * ↑⟨x, hx✝⟩ ^ (k - 1) = 1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: case refine_2
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 : R
hx : x ∈ nthRoots k 1
⊢ ↑⟨x, hx⟩ ^ (k - 1) * ↑⟨x, hx⟩ = 1

Tactic:
rw [mem_nthRoots <| NeZero.pos k] at hx

Goal state after:
case refine_2
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 : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ ↑⟨x, hx✝⟩ ^ (k - 1) * ↑⟨x, hx✝⟩ = 1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: case refine_3
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 : R
hx : x ∈ nthRoots k 1
⊢ { val := ↑⟨x, hx⟩, inv := ↑⟨x, hx⟩ ^ (k - 1), val_inv := ⋯, inv_val := ⋯ } ∈ rootsOfUnity k R

Tactic:
rw [mem_nthRoots <| NeZero.pos k] at hx

Goal state after:
case refine_3
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 : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ { val := ↑⟨x, hx✝⟩, inv := ↑⟨x, hx✝⟩ ^ (k - 1), val_inv := ⋯, inv_val := ⋯ } ∈ rootsOfUnity k R
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
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
⊢ Finite (L →* Rˣ)

Tactic:
by
  let S := rootsOfUnity (Monoid.exponent L) R
  have : Finite (L →* S) := .of_injective _ DFunLike.coe_injective
  refine .of_surjective (fun f : L →* S ↦ (Subgroup.subtype _).comp f) fun f ↦ ?_
  have H a : f a ∈ S := by
    rw [mem_rootsOfUnity, ← map_pow, Monoid.pow_exponent_eq_one, map_one]
  exact ⟨.codRestrict f S H, MonoidHom.ext fun _ ↦ by simp⟩

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

Goal state before:
pp: case inr.inr.refine_2
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
i : n
hi : v i ≠ 0 i
⊢ 0 < Finset.univ.sup' ⋯ (-1 • v)

Tactic:
simp_rw [Finset.lt_sup'_iff, Finset.mem_univ, true_and] at h_sup ⊢

Goal state after:
case inr.inr.refine_2
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
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ b, 0 < v b
⊢ ∃ b, 0 < (-1 • v) b
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha)⁻¹ = diag2 a⁻¹ ⋯

Tactic:
by
  apply inv_eq_of_mul_eq_one_right
  exact diag2_mul_inv a ha

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : (∀ k ∈ F', g k ∈ A (i k)) → ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ ∏ k ∈ insert j F', g k ∈ A (∑ k ∈ insert j F', i k)

Tactic:
Finset.prod_insert hF2,

Goal state after:
ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : (∀ k ∈ F', g k ∈ A (i k)) → ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ g j * ∏ x ∈ F', g x ∈ A (∑ k ∈ insert j F', i k)
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 (i + 0)) (GradedMonoid.GMul.mul xi GradedMonoid.GOne.one) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

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

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + polar f x y

Tactic:
polar

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + (f (x + y) - f x - f y)
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) = r

Tactic:
conv_rhs =>
    rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (decompose ℳ r)]

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) =
    (decompose ℳ).symm (∑ i ∈ DFinsupp.support ((decompose ℳ) r), (of (fun i ↦ ↥(ℳ i)) i) (((decompose ℳ) r) i))
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
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 : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
⊢ ∀ (B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'

Tactic:
B'

Goal state after:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
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' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
⊢ B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'
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
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) (i + j)) = ↑a * ↑(((decompose 𝒜) b) j)

Tactic:
rw [decompose_mul, decompose_coe, coe_of_mul_apply_add]

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_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 : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ ∀ (B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'

Tactic:
B'

Goal state after:
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
⊢ B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
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✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ Q (x✝¹ + x✝) - Q x✝¹ - Q x✝ = polar (⇑Q) x✝¹ x✝

Tactic:
polar

Goal state after:
S : Type u_1
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✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ Q (x✝¹ + x✝) - Q x✝¹ - Q x✝ = Q (x✝¹ + x✝) - Q x✝¹ - Q x✝
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₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

Tactic:
dsimp only [Matrix.IsAdjointPair]
    simp only [Matrix.transpose_mul]
    simp only [← mul_assoc, P.transpose_nonsing_inv]
    convert! this using 2
    · rw [mul_assoc, mul_assoc, ← mul_assoc J]
      rfl
    · rw [mul_assoc, mul_assoc, ← mul_assoc _ _ J]
      rfl

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p✝ : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ i * p✝ ^ j

Tactic:
exact Submodule.mul_mem_mul hp hq

Goal state after: