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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleTriangle.mor₃ ≫
        (shiftFunctorAdd' (DerivedCategory C) 1 ↑n₀ ↑n₁ ⋯).inv.app hS.singleTriangle.obj₁ =
    x.hom.comp hS.singleδ ⋯

Tactic:
ShiftedHom.comp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleTriangle.mor₃ ≫
        (shiftFunctorAdd' (DerivedCategory C) 1 ↑n₀ ↑n₁ ⋯).inv.app hS.singleTriangle.obj₁ =
    x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleδ ≫
        (shiftFunctorAdd' (DerivedCategory C) ↑1 ↑n₀ ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj S.X₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ hS.singleTriangle.mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) (↑n₀) 1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y) =
    ShiftedHom.comp hS.singleδ x.hom ⋯

Tactic:
ShiftedHom.comp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ hS.singleTriangle.mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) (↑n₀) 1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y) =
    hS.singleδ ≫
      (shiftFunctor (DerivedCategory C) ↑1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) ↑n₀ ↑1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y)
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
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
a✝ : relations.G
⊢ (π ∘ₗ Finsupp.lsingle a✝) 1 = ((Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)) ∘ₗ Finsupp.lsingle a✝) 1

Tactic:
;

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
a✝ : relations.G
⊢ (π ∘ₗ Finsupp.lsingle a✝) 1 = ((Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)) ∘ₗ Finsupp.lsingle a✝) 1
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
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
a✝ : relations.G
⊢ ((ofπ π hπ).π ∘ₗ Finsupp.lsingle a✝) 1 = (π ∘ₗ Finsupp.lsingle a✝) 1

Tactic:
;

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
a✝ : relations.G
⊢ ((ofπ π hπ).π ∘ₗ Finsupp.lsingle a✝) 1 = (π ∘ₗ Finsupp.lsingle a✝) 1
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₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤ ∧ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
;

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₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤ ∧ solution.π.ker = Submodule.span A (Set.range relations.relation)
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Mᵀ.SeparatingLeft ↔ M.SeparatingRight

Tactic:
have := Fintype.ofFinite m
  have := Fintype.ofFinite n
  simp_rw [separatingLeft_def, separatingRight_def, dotProduct_transpose_mulVec]

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

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)

Tactic:
;

Goal state after:
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
κ : 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
b : Basis ι R M
c : Basis κ R N
f : M →ₗ[R] N
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Finite κ
i✝ : κ
j✝ : ι
⊢ (LinearMap.toMatrix b c) f i✝ j✝ = c.toMatrix (⇑f ∘ ⇑b) i✝ j✝

Tactic:
;

Goal state after:
ι : Type u_1
κ : 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
b : Basis ι R M
c : Basis κ R N
f : M →ₗ[R] N
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Finite κ
i✝ : κ
j✝ : ι
⊢ (LinearMap.toMatrix b c) f i✝ j✝ = c.toMatrix (⇑f ∘ ⇑b) i✝ j✝
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℤ
x✝ : Mˣ
⊢ x✝ ∈ (zpowGroupHom k).ker ↔ x✝ ∈ rootsOfUnity k.natAbs M

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℤ
x✝ : Mˣ
⊢ x✝ ∈ (zpowGroupHom k).ker ↔ x✝ ∈ rootsOfUnity k.natAbs M
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
⊢ Subsingleton ↥(rootsOfUnity 1 M)

Tactic:
simp [subsingleton_iff]

Goal state after:
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✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
⊢ ↑⟨(Units.map ↑σ) ↑1, ⋯⟩ = ↑1

Tactic:
;

Goal state after:
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✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
⊢ ↑⟨(Units.map ↑σ) ↑1, ⋯⟩ = ↑1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ₁ ξ₂ : ↥(rootsOfUnity n R)
⊢ ↑⟨(Units.map ↑σ) ↑(ξ₁ * ξ₂), ⋯⟩ = ↑(⟨(Units.map ↑σ) ↑ξ₁, ⋯⟩ * ⟨(Units.map ↑σ) ↑ξ₂, ⋯⟩)

Tactic:
;

Goal state after:
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✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ₁ ξ₂ : ↥(rootsOfUnity n R)
⊢ ↑⟨(Units.map ↑σ) ↑(ξ₁ * ξ₂), ⋯⟩ = ↑(⟨(Units.map ↑σ) ↑ξ₁, ⋯⟩ * ⟨(Units.map ↑σ) ↑ξ₂, ⋯⟩)
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✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ ↑↑((_root_.restrictRootsOfUnity σ.symm n) ((_root_.restrictRootsOfUnity σ n) ξ)) = ↑↑ξ

Tactic:
;

Goal state after:
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✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ ↑↑((_root_.restrictRootsOfUnity σ.symm n) ((_root_.restrictRootsOfUnity σ n) ξ)) = ↑↑ξ
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✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n S)
⊢ ↑↑((_root_.restrictRootsOfUnity σ n) ((_root_.restrictRootsOfUnity σ.symm n) ξ)) = ↑↑ξ

Tactic:
;

Goal state after:
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✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n S)
⊢ ↑↑((_root_.restrictRootsOfUnity σ n) ((_root_.restrictRootsOfUnity σ.symm n) ξ)) = ↑↑ξ
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommMonoid R
inst✝ : NeZero k
x : R
x✝ : x ∈ val '' ↑(rootsOfUnity k R)
y : Rˣ
hy1 : y ∈ ↑(rootsOfUnity k R)
hy2 : ↑y = x
⊢ x ∈ {z | z ^ k = 1}

Tactic:
← hy2

Goal state after:
R : Type u_4
k : ℕ
inst✝¹ : CommMonoid R
inst✝ : NeZero k
x : R
x✝ : x ∈ val '' ↑(rootsOfUnity k R)
y : Rˣ
hy1 : y ∈ ↑(rootsOfUnity k R)
hy2 : ↑y = x
⊢ ↑y ∈ {z | z ^ k = 1}
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommMonoid R
inst✝ : NeZero k
x : R
x✝ : x ∈ val '' ↑(rootsOfUnity k R)
y : Rˣ
hy1 : y ∈ ↑(rootsOfUnity k R)
hy2 : ↑y = x
⊢ ↑y ∈ {z | z ^ k = 1}

Tactic:
;

Goal state after:
R : Type u_4
k : ℕ
inst✝¹ : CommMonoid R
inst✝ : NeZero k
x : R
x✝ : x ∈ val '' ↑(rootsOfUnity k R)
y : Rˣ
hy1 : y ∈ ↑(rootsOfUnity k R)
hy2 : ↑y = x
⊢ ↑y ∈ {z | z ^ k = 1}
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:
;

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
⊢ ↑⟨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:
;

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
⊢ ↑⟨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:
;

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
⊢ { val := ↑⟨x, hx⟩, inv := ↑⟨x, hx⟩ ^ (k - 1), val_inv := ⋯, inv_val := ⋯ } ∈ rootsOfUnity k R
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0

Tactic:
;

Goal state after:
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case inr.inr
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
⊢ ∃ j, ∑ i, A i j ≤ 0

Tactic:
refine this h1 inferInstance h2 (-1 • v) (by simp [*]) ?_ ?_

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 • v) ᵥ* A = 0

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
⊢ 0 < Finset.univ.sup' ⋯ (-1 • v)
Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry

Goal state before:
pp: case mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₁ →qᵢ Q₂
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h : (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = (fun f ↦ ⇑f.toLinearMap) g
⊢ { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₁ →qᵢ Q₂
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h : (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = (fun f ↦ ⇑f.toLinearMap) g
⊢ { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = g
Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry

Goal state before:
pp: case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ (toLinearMap✝¹.toFun m) = Q₁ m
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } = { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ (toLinearMap✝¹.toFun m) = Q₁ m
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } = { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry

Goal state before:
pp: case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ (toLinearMap✝¹.toFun m) = Q₁ m
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ (toLinearMap✝¹.toFun m) = Q₁ m
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: case mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
g : Q₁.IsometryEquiv Q₂
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ ((↑toLinearEquiv✝).toFun m) = Q₁ m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv = ⇑g.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm = ⇑g.symm →
      { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } = g

Tactic:
;

Goal state after:
case mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
g : Q₁.IsometryEquiv Q₂
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ ((↑toLinearEquiv✝).toFun m) = Q₁ m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv = ⇑g.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm = ⇑g.symm →
      { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } = g