awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ Commute t.toMatrix M

Tactic:
(Commute.one_left M).add_left ?_

Premises used: Matrix.TransvectionStruct.toMatrix, Matrix.transvection, Commute.add_left, Commute.one_left
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
refine : Commute (single t.i t.j t.c) M
⊢ Commute t.toMatrix M

Tactic:
refine (Commute.one_left M).add_left ?_

Premises used: Commute.add_left, Commute.one_left
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ Commute (HSMul.hSMul (β := Matrix n n R) t.c (single t.i t.j 1)) M

Tactic:
(h _ _ t.hij).smul_left t.c

Premises used: Matrix.TransvectionStruct.hij, Commute.smul_left, Matrix.TransvectionStruct.c
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
h₁ : single t.i t.j t.c = HSMul.hSMul (β := Matrix n n R) t.c (single t.i t.j 1)
⊢ Commute (single t.i t.j t.c) M

Tactic:
convert! (h _ _ t.hij).smul_left t.c using 1

Premises used: Matrix.TransvectionStruct.hij, Commute.smul_left, Matrix.TransvectionStruct.c
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
h₁ : single t.i t.j t.c = single t.i t.j (HSMul.hSMul (β := R) t.c 1)
h₂ : single t.i t.j t.c = single t.i t.j (t.c * 1)
h₃ h₄ : single t.i t.j t.c = single t.i t.j t.c
⊢ single t.i t.j t.c = HSMul.hSMul (β := Matrix n n R) t.c (single t.i t.j 1)

Tactic:
rw [smul_single, smul_eq_mul, mul_one]

Premises used: smul_eq_mul, Matrix.smul_single, mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : CommRing R
i j : n
t : TransvectionStruct n R
⊢ Ne (α := n ⊕ p) (inl t.i) (inl t.j)

Tactic:
simp [t.hij]

Premises used: Matrix.TransvectionStruct.hij
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
t : TransvectionStruct n R
mk :
  ∀ (i j : n) (hij : i ≠ j) (c : R),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix =
      fromBlocks { i := i, j := j, hij := hij, c := c }.toMatrix 0 0 1
⊢ (sumInl p t).toMatrix = fromBlocks t.toMatrix 0 0 1

Tactic:
cases t
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
mk :
  ∀ (a b : n ⊕ p),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
      fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 a b
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix =
    fromBlocks { i := i, j := j, hij := hij, c := c }.toMatrix 0 0 1

Tactic:
ext a b
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : n ⊕ p
mk :
  ∀ (a : n),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) b =
      fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) b
mk₁ :
  ∀ (a : p),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) b =
      fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) b
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 a b

Tactic:
rcases a with a | a
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
b : n ⊕ p
a : n
mk :
  ∀ (b : n),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
      fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
        { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
mk₁ :
  ∀ (b : p),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inr b) =
      fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inr b)
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) b =
    fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) b

Tactic:
rcases b with b | b
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
b : n ⊕ p
a : p
mk :
  ∀ (b : n),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inl b) =
      fromBlocks (m := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inl b)
mk₁ :
  ∀ (b : p),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
      fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) b =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) b

Tactic:
rcases b with b | b
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : n
pos :
  ∀ (h : a = b),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
      fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
        { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
neg :
  ∀ (h : ¬a = b),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
      fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
        { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
    fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
      { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)

Tactic:
by_cases h : a = b
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : n
h : a = b
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
    fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
      { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)

Tactic:
simp [TransvectionStruct.sumInl, transvection, h, single]

Premises used: Matrix.TransvectionStruct.sumInl, Matrix.transvection, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : n
h : ¬a = b
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
    fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
      { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)

Tactic:
simp [TransvectionStruct.sumInl, transvection, h, single]

Premises used: Matrix.TransvectionStruct.sumInl, Matrix.transvection, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a : n
b : p
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inr b) =
    fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inr b)

Tactic:
simp [TransvectionStruct.sumInl, transvection]

Premises used: Matrix.TransvectionStruct.sumInl, Matrix.transvection
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a : p
b : n
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inl b) =
    fromBlocks (m := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inl b)

Tactic:
simp [TransvectionStruct.sumInl, transvection]

Premises used: Matrix.TransvectionStruct.sumInl, Matrix.transvection
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : p
pos :
  ∀ (h : a = b),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
      fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
neg :
  ∀ (h : ¬a = b),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
      fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
by_cases h : a = b
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : p
h : a = b
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
simp [TransvectionStruct.sumInl, transvection, h]

Premises used: Matrix.TransvectionStruct.sumInl, Matrix.transvection
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : p
h : ¬a = b
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
simp [TransvectionStruct.sumInl, transvection, h]

Premises used: Matrix.TransvectionStruct.sumInl, Matrix.transvection
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
N : Matrix p p R
⊢ List.prod (List.map (toMatrix ∘ sumInl p) []) * fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix []) * M) 0 0 N

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
N : Matrix p p R
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ sumInl p) L).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix L).prod * M) 0 0 N
⊢ (List.map (toMatrix ∘ sumInl p) (t :: L)).prod * fromBlocks M 0 0 N =
    fromBlocks ((List.map toMatrix (t :: L)).prod * M) 0 0 N

Tactic:
simp [Matrix.mul_assoc, IH, toMatrix_sumInl, fromBlocks_multiply]

Premises used: Matrix.mul_assoc, Matrix.fromBlocks_multiply, Matrix.TransvectionStruct.toMatrix_sumInl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
nil :
  List.prod (List.map (toMatrix ∘ sumInl p) []) * fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix []) * M) 0 0 N
cons :
  ∀ (t : TransvectionStruct n R) (L : List (TransvectionStruct n R))
    (IH :
      (List.map (toMatrix ∘ sumInl p) L).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix L).prod * M) 0 0 N),
    (List.map (toMatrix ∘ sumInl p) (t :: L)).prod * fromBlocks M 0 0 N =
      fromBlocks ((List.map toMatrix (t :: L)).prod * M) 0 0 N
⊢ (List.map (toMatrix ∘ sumInl p) L).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix L).prod * M) 0 0 N

Tactic:
induction L with
  | nil => simp
  | cons t L IH => simp [Matrix.mul_assoc, IH, toMatrix_sumInl, fromBlocks_multiply]

Premises used: Matrix.mul_assoc, Matrix.fromBlocks_multiply, Matrix.TransvectionStruct.toMatrix_sumInl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N * List.prod (List.map (toMatrix ∘ sumInl p) []) =
    fromBlocks (M * List.prod (List.map toMatrix [])) 0 0 N

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH :
  ∀ (M : Matrix n n R) (N : Matrix p p R),
    fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) (t :: L)).prod =
    fromBlocks (M * (List.map toMatrix (t :: L)).prod) 0 0 N

Tactic:
simp [IH, toMatrix_sumInl, fromBlocks_multiply]

Premises used: Matrix.fromBlocks_multiply, Matrix.TransvectionStruct.toMatrix_sumInl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
nil :
  ∀ (M : Matrix n n R) (N : Matrix p p R),
    fromBlocks M 0 0 N * List.prod (List.map (toMatrix ∘ sumInl p) []) =
      fromBlocks (M * List.prod (List.map toMatrix [])) 0 0 N
cons :
  ∀ (t : TransvectionStruct n R) (L : List (TransvectionStruct n R))
    (IH :
      ∀ (M : Matrix n n R) (N : Matrix p p R),
        fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod =
          fromBlocks (M * (List.map toMatrix L).prod) 0 0 N)
    (M : Matrix n n R) (N : Matrix p p R),
    fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) (t :: L)).prod =
      fromBlocks (M * (List.map toMatrix (t :: L)).prod) 0 0 N
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N

Tactic:
induction L generalizing M N with
  | nil => simp
  | cons t L IH => simp [IH, toMatrix_sumInl, fromBlocks_multiply]

Premises used: Matrix.fromBlocks_multiply, Matrix.TransvectionStruct.toMatrix_sumInl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : CommRing R
i j : n
e : n ≃ p
t : TransvectionStruct n R
⊢ Ne.{u_2 + 1} (α := p) ((e : (a : n) → p) t.i : p) ((e : (a : n) → p) t.j : p)

Tactic:
simp [t.hij]

Premises used: Matrix.TransvectionStruct.hij
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t : TransvectionStruct n R
rcases :
  ∀ (t_i t_j : n) (hij : t_i ≠ t_j) (c : R),
    (reindexEquiv e { i := t_i, j := t_j, hij := hij, c := c : TransvectionStruct n R }).toMatrix =
      (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) { i := t_i, j := t_j, hij := hij, c := c }.toMatrix
⊢ (reindexEquiv e t).toMatrix = (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) t.toMatrix

Tactic:
rcases t with ⟨t_i, t_j, _⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a :
  ∀ (a b : p),
    (reindexEquiv e { i := t_i, j := t_j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
      (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) { i := t_i, j := t_j, hij := hij, c := c }.toMatrix a
        b
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij, c := c : TransvectionStruct n R }).toMatrix =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) { i := t_i, j := t_j, hij := hij, c := c }.toMatrix

Tactic:
ext a b
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
a₁ :
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) { i := t_i, j := t_j, hij := hij, c := c }.toMatrix a b

Tactic:
simp only [reindexEquiv, transvection, toMatrix_mk,
    submatrix_apply, reindex_apply, reindexAlgEquiv_apply]

Premises used: Matrix.reindex_apply, Matrix.transvection, Matrix.TransvectionStruct.toMatrix_mk, Matrix.reindexAlgEquiv_apply, Matrix.TransvectionStruct.reindexEquiv, Matrix.submatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
pos :
  ∀ (ha : (e : (a : n) → p) t_i = a),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
neg :
  ∀ (ha : ¬(e : (a : n) → p) t_i = a),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)

Tactic:
by_cases ha : e t_i = a

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : (e : (a : n) → p) t_i = a
pos :
  ∀ (hb : (e : (a : n) → p) t_j = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
neg :
  ∀ (hb : ¬(e : (a : n) → p) t_j = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)

Tactic:
by_cases hb : e t_j = b

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : ¬(e : (a : n) → p) t_i = a
pos :
  ∀ (hb : (e : (a : n) → p) t_j = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
neg :
  ∀ (hb : ¬(e : (a : n) → p) t_j = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)

Tactic:
by_cases hb : e t_j = b

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : (e : (a : n) → p) t_i = a
hb : (e : (a : n) → p) t_j = b
pos :
  ∀ (hab : a = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
neg :
  ∀ (hab : ¬a = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)

Tactic:
by_cases hab : a = b