mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Unique

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst✝¹ : Unique m
inst✝ : Unique n
M : Matrix m n A
i : m
j : n
⊢ (fun a ↦ of fun x x_1 ↦ a) ((fun M ↦ M default default) M) i j = M i j

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst✝¹ : Unique m
inst✝ : Unique n
M : Matrix m n A
i : m
j : n
⊢ (fun a ↦ of fun x x_1 ↦ a) ((fun M ↦ M default default) M) i j = M i j
Module: Mathlib.LinearAlgebra.Matrix.Unique

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst✝¹ : Unique m
inst✝ : Unique n
M : Matrix m n A
⊢ (fun a ↦ of fun x x_1 ↦ a) ((fun M ↦ M default default) M) = M

Tactic:
by ext i j; simp [Subsingleton.elim i default, Subsingleton.elim j default]

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ (diagonal fun x ↦ 1).permanent = 1

Tactic:
;

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ (diagonal fun x ↦ 1).permanent = 1
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
| ∏ x, M (x✝ x) x * c

Tactic:
;

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
| ∏ x, M (x✝ x) x * c
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ detp s Ai = ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D

Tactic:
;

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ detp s Ai = ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ detp s Ai = ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D

Tactic:
rw [detp_option_expand_row_none, add_comm]

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ ∑ k, Ai none (some k) * detp (-s) (Ai.submatrix some (Function.update some k none)) +
      Ai none none * detp s (Ai.submatrix some some) =
    ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: case e'_5.a.e'_6
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝² : r < Fintype.card n
x✝¹ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
x✝ : Fin r
a✝ : x✝ ∈ Finset.univ
⊢ Ai.submatrix some (Function.update some x✝ none) = Aj x✝

Tactic:
;

Goal state after:
case e'_5.a.e'_6
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝² : r < Fintype.card n
x✝¹ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
x✝ : Fin r
a✝ : x✝ ∈ Finset.univ
⊢ Ai.submatrix some (Function.update some x✝ none) = Aj x✝
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: case e_M
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k : n
v : n → R
⊢ adjp 1 A * A + detp (-1) A • 1 = adjp (-1) A * A + detp 1 A • 1

Tactic:
;

Goal state after:
case e_M
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k : n
v : n → R
⊢ adjp 1 A * A + detp (-1) A • 1 = adjp (-1) A * A + detp 1 A • 1
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k : n
h : ∀ (v : n → R), (adjp 1 A *ᵥ A *ᵥ v) k + detp (-1) A * v k = (adjp (-1) A *ᵥ A *ᵥ v) k + detp 1 A * v k
⊢ x k * detp 1 A + y k * detp (-1) A = y k * detp 1 A + x k * detp (-1) A

Tactic:
;

Goal state after:
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k : n
h : ∀ (v : n → R), (adjp 1 A *ᵥ A *ᵥ v) k + detp (-1) A * v k = (adjp (-1) A *ᵥ A *ᵥ v) k + detp 1 A * v k
⊢ x k * detp 1 A + y k * detp (-1) A = y k * detp 1 A + x k * detp (-1) A
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily 0) x✝¹ x✝ = 0 x✝¹ x✝

Tactic:
;

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily 0) x✝¹ x✝ = 0 x✝¹ x✝
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily (f + g)) x✝¹ x✝ = (piFamily f + piFamily g) x✝¹ x✝

Tactic:
;

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily (f + g)) x✝¹ x✝ = (piFamily f + piFamily g) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily (s • f)) x✝¹ x✝ = (s • piFamily f) x✝¹ x✝

Tactic:
;

Goal state after:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily (s • f)) x✝¹ x✝ = (s • piFamily f) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
⊢ A.mulVec = ⇑g ∘ ⇑f

Tactic:
;

Goal state after:
R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
⊢ A.mulVec = ⇑g ∘ ⇑f
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
x✝¹ : Fin n → R
x✝ : Fin n
⊢ (A *ᵥ x✝¹) x✝ = (⇑g ∘ ⇑f) x✝¹ x✝

Tactic:
;

Goal state after:
R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
x✝¹ : Fin n → R
x✝ : Fin n
⊢ (A *ᵥ x✝¹) x✝ = (⇑g ∘ ⇑f) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
hA : A.Nonsingular
x✝ : Fin n
⊢ A.row ⟨m, hnm⟩ x✝ = 0 x✝

Tactic:
;

Goal state after:
R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
hA : A.Nonsingular
x✝ : Fin n
⊢ A.row ⟨m, hnm⟩ x✝ = 0 x✝
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝ : InvolutiveStar α
x✝ : WithConv (Matrix m n α)
i✝ : m
j✝ : n
⊢ (star (star x✝)).ofConv i✝ j✝ = x✝.ofConv i✝ j✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝ : InvolutiveStar α
x✝ : WithConv (Matrix m n α)
i✝ : m
j✝ : n
⊢ (star (star x✝)).ofConv i✝ j✝ = x✝.ofConv i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : Mul α
inst✝ : StarMul α
x✝¹ x✝ : WithConv (Matrix m n α)
i✝ : m
j✝ : n
⊢ (star (x✝¹ * x✝)).ofConv i✝ j✝ = (star x✝ * star x✝¹).ofConv i✝ j✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : Mul α
inst✝ : StarMul α
x✝¹ x✝ : WithConv (Matrix m n α)
i✝ : m
j✝ : n
⊢ (star (x✝¹ * x✝)).ofConv i✝ j✝ = (star x✝ * star x✝¹).ofConv i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : CommSemiring α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝² x✝¹ : WithConv (Matrix m n α)
i✝ : n
x✝ : m
⊢ (((↑(congrLinearEquiv toLin')).toFun (x✝² * x✝¹)).ofConv ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝ =
    (((↑(congrLinearEquiv toLin')).toFun x✝² * (↑(congrLinearEquiv toLin')).toFun x✝¹).ofConv ∘ₗ
        LinearMap.single α (fun i ↦ α) i✝)
      1 x✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : CommSemiring α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝² x✝¹ : WithConv (Matrix m n α)
i✝ : n
x✝ : m
⊢ (((↑(congrLinearEquiv toLin')).toFun (x✝² * x✝¹)).ofConv ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝ =
    (((↑(congrLinearEquiv toLin')).toFun x✝² * (↑(congrLinearEquiv toLin')).toFun x✝¹).ofConv ∘ₗ
        LinearMap.single α (fun i ↦ α) i✝)
      1 x✝
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x y : Matrix m n α
i✝ : n
x✝ : m
⊢ (toLin' (x ⊙ y) ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝ =
    ((toConv (toLin' x) * toConv (toLin' y)).ofConv ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x y : Matrix m n α
i✝ : n
x✝ : m
⊢ (toLin' (x ⊙ y) ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝ =
    ((toConv (toLin' x) * toConv (toLin' y)).ofConv ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝³ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
i✝ : (i : ι) → κ i
⊢ ((((lift ((MultilinearMap.fromDFinsuppEquiv κ R) fun p ↦ (DFinsupp.lsingle p).compMultilinearMap (tprod R)) ∘ₗ
                (DFinsupp.lsum R) fun p ↦ lift ((map fun i ↦ DFinsupp.lsingle (p i)).compMultilinearMap (tprod R))) ∘ₗ
              DFinsupp.lsingle p).compMultilinearMap
          (tprod R))
        x)
      i✝ =
    (((LinearMap.id ∘ₗ DFinsupp.lsingle p).compMultilinearMap (tprod R)) x) i✝

Tactic:
;

Goal state after:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝³ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
i✝ : (i : ι) → κ i
⊢ ((((lift ((MultilinearMap.fromDFinsuppEquiv κ R) fun p ↦ (DFinsupp.lsingle p).compMultilinearMap (tprod R)) ∘ₗ
                (DFinsupp.lsum R) fun p ↦ lift ((map fun i ↦ DFinsupp.lsingle (p i)).compMultilinearMap (tprod R))) ∘ₗ
              DFinsupp.lsingle p).compMultilinearMap
          (tprod R))
        x)
      i✝ =
    (((LinearMap.id ∘ₗ DFinsupp.lsingle p).compMultilinearMap (tprod R)) x) i✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝³ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (κ i)
x : (i : ι) → κ i
x✝ : (i : ι) → M i (x i)
⊢ (((((DFinsupp.lsum R) fun p ↦ lift ((map fun i ↦ DFinsupp.lsingle (p i)).compMultilinearMap (tprod R))) ∘ₗ
                lift
                  ((MultilinearMap.fromDFinsuppEquiv κ R) fun p ↦
                    (DFinsupp.lsingle p).compMultilinearMap (tprod R))).compMultilinearMap
            (tprod R)).compLinearMap
        fun i ↦ DFinsupp.lsingle (x i))
      x✝ =
    ((LinearMap.id.compMultilinearMap (tprod R)).compLinearMap fun i ↦ DFinsupp.lsingle (x i)) x✝

Tactic:
;

Goal state after:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝³ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (κ i)
x : (i : ι) → κ i
x✝ : (i : ι) → M i (x i)
⊢ (((((DFinsupp.lsum R) fun p ↦ lift ((map fun i ↦ DFinsupp.lsingle (p i)).compMultilinearMap (tprod R))) ∘ₗ
                lift
                  ((MultilinearMap.fromDFinsuppEquiv κ R) fun p ↦
                    (DFinsupp.lsingle p).compMultilinearMap (tprod R))).compMultilinearMap
            (tprod R)).compLinearMap
        fun i ↦ DFinsupp.lsingle (x i))
      x✝ =
    ((LinearMap.id.compMultilinearMap (tprod R)).compLinearMap fun i ↦ DFinsupp.lsingle (x i)) x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: case e_n
R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
this :
  (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)
⊢ (subsingletonEquiv ())
      ((tprod R) fun i₂ ↦
        m ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm (Sum.inr i₂)))) =
    m i₀

Tactic:
;

Goal state after:
case e_n
R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
this :
  (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)
⊢ (subsingletonEquiv ())
      ((tprod R) fun i₂ ↦
        m ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm (Sum.inr i₂)))) =
    m i₀