awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
this :
  M =
    (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
      ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)
rw :
  HMul.hMul (β := Matrix p p 𝕜) (List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod
        ((reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
            ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M) :
          Matrix p p 𝕜) *
      (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))
⊢ (List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod * M *
      (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
this :
  M =
    (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
      ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)
simp :
  HMul.hMul (β := Matrix p p 𝕜)
      (HMul.hMul (α := Matrix p p 𝕜) (β := Matrix p p 𝕜)
        ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (List.map toMatrix L₀).prod : Matrix p p 𝕜)
        ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
            ((reindex e e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M) :
          Matrix p p 𝕜))
      ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (List.map toMatrix L₀').prod : Matrix p p 𝕜) =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))
⊢ HMul.hMul (β := Matrix p p 𝕜) (List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod
        ((reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
            ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M) :
          Matrix p p 𝕜) *
      (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))

Tactic:
simp only [toMatrix_reindexEquiv_prod, List.map_map, reindexAlgEquiv_apply]

Premises used: Matrix.TransvectionStruct.toMatrix_reindexEquiv_prod, List.map_map, Matrix.reindexAlgEquiv_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
this :
  M =
    (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
      ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)
simp :
  Eq (α := Matrix p p 𝕜) ((reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (diagonal D₀) : Matrix p p 𝕜)
    (diagonal (D₀ ∘ (⇑e : (a : p) → n)) : Matrix p p 𝕜)
⊢ HMul.hMul (β := Matrix p p 𝕜)
      (HMul.hMul (α := Matrix p p 𝕜) (β := Matrix p p 𝕜)
        ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (List.map toMatrix L₀).prod : Matrix p p 𝕜)
        ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
            ((reindex e e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M) :
          Matrix p p 𝕜))
      ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (List.map toMatrix L₀').prod : Matrix p p 𝕜) =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))

Tactic:
simp only [← reindexAlgEquiv_apply 𝕜, ← reindexAlgEquiv_mul, h₀]

Premises used: Matrix.reindexAlgEquiv_mul, Matrix.reindexAlgEquiv_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
this :
  M =
    (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
      ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)
⊢ Eq (α := Matrix p p 𝕜) ((reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (diagonal D₀) : Matrix p p 𝕜)
    (diagonal (D₀ ∘ (⇑e : (a : p) → n)) : Matrix p p 𝕜)

Tactic:
simp only [Equiv.symm_symm, reindex_apply, submatrix_diagonal_equiv, reindexAlgEquiv_apply]

Premises used: Matrix.reindex_apply, Equiv.symm_symm, Matrix.submatrix_diagonal_equiv, Matrix.reindexAlgEquiv_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
this :
  ∀ (cn : ℕ),
    Fintype.card n = cn →
      ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
        (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
this :
  ∀ (cn : ℕ),
    Fintype.card n = cn →
      ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
        (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
exact this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
suffices :
  ∀ (cn : ℕ),
    Fintype.card n = cn →
      ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
        (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
suffices ∀ cn, Fintype.card n = cn →
      ∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D by exact this _ rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
⟨List.nil, List.nil, fun _ => 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat, List.nil
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
zero : List.prod (List.map toMatrix []) * M * List.prod (List.map toMatrix []) = diagonal fun (x : n) ↦ 1
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
zero :
  ∀ (i j : n),
    HMul.hMul (β := Matrix n n 𝕜) (List.prod (List.map toMatrix []) * M) (List.prod (List.map toMatrix [])) i j =
      diagonal (fun (x : n) ↦ 1) i j
⊢ List.prod (List.map toMatrix []) * M * List.prod (List.map toMatrix []) = diagonal fun (x : n) ↦ 1

Tactic:
ext i j

Premises used: Matrix.TransvectionStruct.i, Matrix.TransvectionStruct.j
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
i j : n
zero :
  ∀ (hn : IsEmpty n) (i j : n),
    HMul.hMul (β := Matrix n n 𝕜) (List.prod (List.map toMatrix []) * M) (List.prod (List.map toMatrix [])) i j =
      diagonal (fun (x : n) ↦ 1) i j
⊢ HMul.hMul (β := Matrix n n 𝕜) (List.prod (List.map toMatrix []) * M) (List.prod (List.map toMatrix [])) i j =
    diagonal (fun (x : n) ↦ 1) i j

Tactic:
rw [Fintype.card_eq_zero_iff] at hn

Premises used: Fintype.card_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : IsEmpty n
i j : n
⊢ HMul.hMul (β := Matrix n n 𝕜) (List.prod (List.map toMatrix []) * M) (List.prod (List.map toMatrix [])) i j =
    diagonal (fun (x : n) ↦ 1) i j

Tactic:
hn.elim' i

Premises used: IsEmpty.elim'
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : IsEmpty n
i j : n
⊢ HMul.hMul (β := Matrix n n 𝕜) (List.prod (List.map toMatrix []) * M) (List.prod (List.map toMatrix [])) i j =
    diagonal (fun (x : n) ↦ 1) i j

Tactic:
exact hn.elim' i

Premises used: IsEmpty.elim'
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
refine : Fintype.card n = Fintype.card (Fin r ⊕ Unit)
⊢ n ≃ Fin r ⊕ Unit

Tactic:
refine Fintype.equivOfCardEq ?_

Premises used: Fintype.equivOfCardEq
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
rw : r + 1 = Fintype.card (Fin r ⊕ Unit)
⊢ Fintype.card n = Fintype.card (Fin r ⊕ Unit)

Tactic:
rw [hn]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
rw : r + 1 = Fintype.card (Fin r) + Fintype.card Unit
⊢ r + 1 = Fintype.card (Fin r ⊕ Unit)

Tactic:
rw [@Fintype.card_sum (Fin r) Unit _ _]

Premises used: Fintype.card_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ r + 1 = Fintype.card (Fin r) + Fintype.card Unit

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
succ :
  ∀ (e : n ≃ Fin r ⊕ Unit),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
have e : n ≃ Fin r ⊕ Unit := by
      refine Fintype.equivOfCardEq ?_
      rw [hn]
      rw [@Fintype.card_sum (Fin r) Unit _ _]
      simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
e : n ≃ Fin r ⊕ Unit
succ :
  ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D :
    Fin r ⊕ Unit → 𝕜),
    HMul.hMul (β := Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (List.map toMatrix L).prod
          ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix n n 𝕜) → Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) M :
            Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) *
        (List.map toMatrix L').prod =
      diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e

Premises used: Matrix.Pivot.reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
e : n ≃ Fin r ⊕ Unit
N : Matrix (Fin r) (Fin r) 𝕜
⊢ Fintype.card (Fin r) = r

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
e : n ≃ Fin r ⊕ Unit
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D :
    Fin r ⊕ Unit → 𝕜),
    HMul.hMul (β := Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (List.map toMatrix L).prod
          ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix n n 𝕜) → Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) M :
            Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) *
        (List.map toMatrix L').prod =
      diagonal D

Tactic:
apply
      exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction fun N =>
        IH (Fin r) N (by simp)

Premises used: Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction, Fin
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
cn : ℕ
hn : Fintype.card n = cn
zero :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = 0),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
succ :
  ∀ (r : ℕ)
    (IH :
      ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
        ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
          (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D)
    (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r + 1),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
induction cn generalizing n M with
  | zero =>
    refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩
    ext i j
    rw [Fintype.card_eq_zero_iff] at hn
    exact hn.elim' i
  | succ r IH =>
    have e : n ≃ Fin r ⊕ Unit := by
      refine Fintype.equivOfCardEq ?_
      rw [hn]
      rw [@Fintype.card_sum (Fin r) Unit _ _]
      simp
    apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e
    apply
      exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction fun N =>
        IH (Fin r) N (by simp)

Premises used: Matrix.TransvectionStruct.i, Matrix.TransvectionStruct.j, Fintype.card_eq_zero_iff, Matrix.zero
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
⊢ Fintype.card n = Fintype.card (Fin (Fintype.card n))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
have :
  ∀ (e : n ≃ Fin (Fintype.card n)),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
have e : n ≃ Fin (Fintype.card n) := Fintype.equivOfCardEq (by simp)
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card n)
apply :
  ∃ (L : List (TransvectionStruct (Fin (Fintype.card n)) 𝕜)) (L' : List (TransvectionStruct (Fin (Fintype.card n)) 𝕜))
    (D : Fin (Fintype.card n) → 𝕜),
    HMul.hMul (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) (List.map toMatrix L).prod
          ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix n n 𝕜) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) M :
            Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) *
        (List.map toMatrix L').prod =
      diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e

Premises used: Matrix.Pivot.reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card n)
⊢ ∃ (L : List (TransvectionStruct (Fin (Fintype.card n)) 𝕜)) (L' : List (TransvectionStruct (Fin (Fintype.card n)) 𝕜))
    (D : Fin (Fintype.card n) → 𝕜),
    HMul.hMul (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) (List.map toMatrix L).prod
          ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix n n 𝕜) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) M :
            Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) *
        (List.map toMatrix L').prod =
      diagonal D

Tactic:
apply exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux

Premises used: Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
rcases :
  ∀ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜)
    (h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod

Tactic:
rcases exists_list_transvec_mul_mul_list_transvec_eq_diagonal M with ⟨L, L', D, h⟩

Premises used: Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod

Tactic:
⟨L.reverse.map TransvectionStruct.inv, L'.reverse.map TransvectionStruct.inv, D, ?_⟩

Premises used: List.map, Matrix.TransvectionStruct.inv, Exists.intro, List.reverse
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
refine :
  M =
    (List.map toMatrix (List.map TransvectionStruct.inv L.reverse)).prod * diagonal D *
      (List.map toMatrix (List.map TransvectionStruct.inv L'.reverse)).prod
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod

Tactic:
refine ⟨L.reverse.map TransvectionStruct.inv, L'.reverse.map TransvectionStruct.inv, D, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
this :
  M =
    (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod * M *
      ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
⊢ M =
    (List.map toMatrix (List.map TransvectionStruct.inv L.reverse)).prod * diagonal D *
      (List.map toMatrix (List.map TransvectionStruct.inv L'.reverse)).prod

Tactic:
simpa [← h, Matrix.mul_assoc]

Premises used: Matrix.mul_assoc