mathlib-initiative/mathlib-tactics huggingface dataset:
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 : { x // x ∈ nthRoots k 1 }
⊢ { val := ↑x, inv := ↑x ^ (k - 1), val_inv := ⋯, inv_val := ⋯ } ∈ rootsOfUnity k R

Tactic:
rcases x with ⟨x, 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
⊢ { 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
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (L →* ↥S)
f : L →* Rˣ
a : L
⊢ f a ∈ S

Tactic:
mem_rootsOfUnity,

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✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (L →* ↥S)
f : L →* Rˣ
a : L
⊢ f a ^ Monoid.exponent L = 1
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
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑g).map ⇑f * (↑g)⁻¹.map ⇑f = 1

Tactic:
← Matrix.map_mul

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑g * (↑g)⁻¹).map ⇑f = 1
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
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑g)⁻¹.map ⇑f * (↑g).map ⇑f = 1

Tactic:
← Matrix.map_mul

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ ((↑g)⁻¹ * ↑g).map ⇑f = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι✝ : 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✝¹⁰ : Field K
inst✝⁹ : Invertible 2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : FiniteDimensional K V
ι : Type u_10
S : Type u_11
R : Type u_12
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R R
w w' : ι → S
h : w = w'
⊢ ∀ (m : ι → R), (weightedSumSquares R w') ((↑(LinearEquiv.refl R (ι → R))).toFun m) = (weightedSumSquares R w) m

Tactic:
simp [h]

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
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
i : n
h : ↑g i = 0
⊢ ∀ (j : n), ↑g i j = 0

Tactic:
simp [h]

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
hn : IsEmpty n
⊢ ↥⊥ ≃* ↥(rootsOfUnity (max 0 1) R)

Tactic:
max_eq_right_of_lt zero_lt_one,

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
hn : IsEmpty n
⊢ ↥⊥ ≃* ↥(rootsOfUnity 1 R)
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
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
a b : R
h : a ≠ 0
⊢ !![a, b; 0, a⁻¹].det = 1

Tactic:
simp [h]

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b₁ b₂ : F
⊢ ↑(transvection hij (b₁ + b₂)) = ↑(transvection hij b₁ * transvection hij b₂)

Tactic:
simp [transvection_coe, mul_add, add_mul,
    single_mul_single_of_ne _ _ _ _ hij.symm, single_add, add_assoc]

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
k : Fin 2
⊢ (diag2 a ha • Pi.single 0 1) k = (a • Pi.single 0 1) k

Tactic:
fin_cases k <;> simp [Matrix.SpecialLinearGroup.smul_def, diag2_coe]

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
k : Fin 2
⊢ (diag2 a ha • Pi.single 1 1) k = (a⁻¹ • Pi.single 1 1) k

Tactic:
fin_cases k <;> simp [Matrix.SpecialLinearGroup.smul_def, diag2_coe]

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

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) (B ∘ₗ f) = (toMatrix' f)ᵀ * (toMatrix₂' R) B

Tactic:
← LinearMap.compl₂_id (B.comp f),

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) ((B ∘ₗ f).compl₂ id) = (toMatrix' f)ᵀ * (toMatrix₂' R) B
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₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂
i : n
j : m
⊢ (toMatrix₂ b₁ b₂) B i j = (B (b₁ i)) (b₂ j)

Tactic:
by
  simp only [toMatrix₂, LinearEquiv.trans_apply, toMatrixₛₗ₂'_apply, LinearEquiv.arrowCongr_apply,
    Basis.equivFun_symm_apply, Pi.single_apply, ite_smul, one_smul, zero_smul, sum_ite_eq',
    mem_univ, ↓reduceIte, LinearEquiv.refl_apply]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
x✝ : ⨁ (i : ι), A i
⊢ x✝ * 0 = 0

Tactic:
by simp only [Mul.mul, HMul.hMul, map_zero]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A).flip ((of A 0) GradedMonoid.GOne.one)) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
rw [flip_apply, mulHom_of_of]

Goal state after:
ι : 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)
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
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ (B x) y = ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ ⇑(b₂.repr y)

Tactic:
nth_rw 1 [← b₁.sum_repr x, ← b₂.sum_repr y]
  suffices ∑ j, ∑ i, σ₂ (b₂.repr y j) * σ₁ (b₁.repr x i) * B (b₁ i) (b₂ j) =
           ∑ i, ∑ j, σ₁ (b₁.repr x i) * σ₂ (b₂.repr y j) * B (b₁ i) (b₂ j) by
    simpa [dotProduct, Matrix.mulVec_eq_sum, Finset.mul_sum, -Basis.sum_repr, ← mul_assoc]
  simp_rw [mul_comm (σ₂ _)]
  exact Finset.sum_comm

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 x' y : M
⊢ f (x + x' + y) + f y + f x' + f y + f x = f (x + y) + f (x' + y) + f y + f (x + x') ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Tactic:
simp only [add_right_comm _ (f y) _, add_right_comm _ (f x') (f x)]

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
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 (∑ i ∈ Finset.cons a s ha, f i) =
    ∑ i ∈ Finset.cons a s ha, Q (f i) + ∑ ij ∈ (Finset.cons a s ha).sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)

Tactic:
simp_rw [Finset.sum_cons, QuadraticMap.map_add, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_filter, Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons,
      Sym2.mkEmbedding_apply, Sym2.mk_isDiag_iff, not_true, if_false, zero_add,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply]

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) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + ∑ x ∈ s, polar (⇑Q) (f a) (f x))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁'
b₁' : Basis n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ (toMatrix₂ b₁' b₂) (B ∘ₗ f) = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B

Tactic:
← LinearMap.compl₂_id (B.comp f),

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁'
b₁' : Basis n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ (toMatrix₂ b₁' b₂) ((B ∘ₗ f).compl₂ id) = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B
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✝⁵ : Monoid S
inst✝⁴ : Monoid T
inst✝³ : DistribMulAction S N
inst✝² : DistribMulAction T N
inst✝¹ : SMulCommClass S R N
inst✝ : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
this : SMulCommClass R S N := SMulCommClass.symm S R N
⊢ ∀ (x y : M), (a • ⇑Q) (x + y) = (a • ⇑Q) x + (a • ⇑Q) y + ((a • B) x) y

Tactic:
simp [h]

Goal state after:
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 B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'

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

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

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 : ι
⊢ ∑ a ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with a.1 + a.2 = n, ↑(GradedMonoid.GMul.mul (r a.1) (r' a.2)) =
    ∑ 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 ↑r * ↑rj else 0) = ↑r * ↑(r' j)

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:
swap

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

ι : 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 ↑r * ↑rj else 0) = ↑r * ↑(r' j)
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_1 ri ↦
      DFinsupp.sum ((of (fun i ↦ ↥(A i)) i) r') fun j rj ↦ if i_1 + j = n then ↑ri * ↑rj else 0) =
    ↑(r j) * ↑r'

Tactic:
DFinsupp.sum_comm

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 ((of (fun i ↦ ↥(A i)) i) r') fun i₂ x₂ ↦
      DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i₂ = n then ↑x₁ * ↑x₂ else 0) =
    ↑(r j) * ↑r'
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₁ * ↑r' else 0) = ↑(r j) * ↑r'

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:
swap

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

ι : 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₁ * ↑r' else 0) = ↑(r j) * ↑r'
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : x = 0
⊢ Q x ≤ 0

Tactic:
simp [h]

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✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑r * ↑rj else 0) = 0

pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑0 * ↑rj else 0) = 0

Tactic:
swap

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✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑0 * ↑rj else 0) = 0

ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑r * ↑rj else 0) = 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✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i_1 ri ↦
      DFinsupp.sum ((of (fun i ↦ ↥(A i)) i) r') fun j rj ↦ if i_1 + j = n then ↑ri * ↑rj else 0) =
    0

Tactic:
DFinsupp.sum_comm

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✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum ((of (fun i ↦ ↥(A i)) i) r') fun i₂ x₂ ↦
      DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i₂ = n then ↑x₁ * ↑x₂ else 0) =
    0