awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val : n₂
j : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inr val) j = A₁ᴴ.fromRows A₂ᴴ (Sum.inr val) j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
a : ∀ (i : n) (val : m₁), (A₁.fromRows A₂)ᴴ i (Sum.inl val) = A₁ᴴ.fromCols A₂ᴴ i (Sum.inl val)
a₁ : ∀ (i : n) (val : m₂), (A₁.fromRows A₂)ᴴ i (Sum.inr val) = A₁ᴴ.fromCols A₂ᴴ i (Sum.inr val)
⊢ (A₁.fromRows A₂)ᴴ = A₁ᴴ.fromCols A₂ᴴ

Tactic:
ext _ (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
val : m₁
⊢ (A₁.fromRows A₂)ᴴ i (Sum.inl val) = A₁ᴴ.fromCols A₂ᴴ i (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
val : m₂
⊢ (A₁.fromRows A₂)ᴴ i (Sum.inr val) = A₁ᴴ.fromCols A₂ᴴ i (Sum.inr val)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
inst_3 : One R
a :
  ∀ (i j : I × J),
    Eq.{u_5 + 1} (α := R) ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) 1 i j : R)
      (1 i j : R)
⊢ Eq (α := Matrix (I × J) (I × J) R) ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) 1) 1

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
inst_3 : One R
i j : I × J
a :
  if i = j then Eq.{u_5 + 1} (α := R) ((if i.1 = j.1 then 1 else 0) i.2 j.2) 1
  else Eq.{u_5 + 1} (α := R) ((if i.1 = j.1 then 1 else 0) i.2 j.2) 0
⊢ Eq.{u_5 + 1} (α := R) ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) 1 i j : R)
    (1 i j : R)

Tactic:
simp only [comp, Equiv.coe_fn_mk, one_apply, apply_ite]

Premises used: Matrix.comp, Matrix.one_apply, apply_ite, Equiv.coe_fn_mk
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
inst_3 : One R
i j : I × J
⊢ if i = j then Eq.{u_5 + 1} (α := R) ((if i.1 = j.1 then 1 else 0) i.2 j.2) 1
  else Eq.{u_5 + 1} (α := R) ((if i.1 = j.1 then 1 else 0) i.2 j.2) 0

Tactic:
aesop
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
M : Matrix I J (Matrix K L R)
f : R → R'
⊢ Eq (α := Matrix (I × K) (J × L) R')
    ((comp I J K L R' : (a : Matrix I J (Matrix K L R')) → Matrix (I × K) (J × L) R')
        (M.map fun (M' : Matrix K L R) ↦ M'.map f) :
      Matrix (I × K) (J × L) R')
    (map ((comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) M) f :
      Matrix (I × K) (J × L) R')

Tactic:
rfl

Premises used: Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
a :
  ∀ (i' : I) (k' : K) (j' : J) (l' : L),
    (comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) (single i j (single k l r)) (i', k')
        (j', l') =
      single (i, k) (j, l) r (i', k') (j', l')
⊢ (comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) (single i j (single k l r)) =
    single (i, k) (j, l) r

Tactic:
ext ⟨i', k'⟩ ⟨j', l'⟩
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
a : single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
⊢ (comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) (single i j (single k l r)) (i', k')
      (j', l') =
    single (i, k) (j, l) r (i', k') (j', l')

Tactic:
dsimp [comp_apply]

Premises used: Matrix.comp_apply
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
a : ∀ (hi : i ≠ i'), single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
a₁ : single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')

Tactic:
obtain hi | rfl := ne_or_eq i i'

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
a : 0 k' l' = single (i, k) (j, l) r (i', k') (j', l')
a₁ : Eq.{u_5 + 1} (α := R) (0 k' l') 0
a₂ a₃ : Eq.{u_5 + 1} (α := R) 0 0
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')

Tactic:
rw [single_apply_of_row_ne hi,
      single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]

Premises used: Matrix.zero_apply, Matrix.single_apply_of_row_ne, ne_of_apply_ne, Prod.fst
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
a : ∀ (hj : j ≠ j'), single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
a₁ : single i j (single k l r) i j k' l' = single (i, k) (j, l) r (i, k') (j, l')
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')

Tactic:
obtain hj | rfl := ne_or_eq j j'

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
a : 0 k' l' = single (i, k) (j, l) r (i, k') (j', l')
a₁ : Eq.{u_5 + 1} (α := R) (0 k' l') 0
a₂ a₃ : Eq.{u_5 + 1} (α := R) 0 0
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')

Tactic:
rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]

Premises used: Matrix.zero_apply, ne_of_apply_ne, Prod.fst, Matrix.single_apply_of_col_ne
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
a : single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')
⊢ single i j (single k l r) i j k' l' = single (i, k) (j, l) r (i, k') (j, l')

Tactic:
rw [single_apply_same]

Premises used: Matrix.single_apply_same
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
a : ∀ (hk : k ≠ k'), single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')
a₁ : single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')

Tactic:
obtain hk | rfl := ne_or_eq k k'

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
hk : k ≠ k'
a : 0 = single (i, k) (j, l) r (i, k') (j, l')
a₁ a₂ : Eq.{u_5 + 1} (α := R) 0 0
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')

Tactic:
rw [single_apply_of_row_ne hk,
      single_apply_of_row_ne (ne_of_apply_ne Prod.snd hk)]

Premises used: Matrix.single_apply_of_row_ne, ne_of_apply_ne, Prod.snd
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
a : ∀ (hj : l ≠ l'), single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')
a₁ : single k l r k l = single (i, k) (j, l) r (i, k) (j, l)
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')

Tactic:
obtain hj | rfl := ne_or_eq l l'

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
hj : l ≠ l'
a : 0 = single (i, k) (j, l) r (i, k) (j, l')
a₁ a₂ : Eq.{u_5 + 1} (α := R) 0 0
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')

Tactic:
rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.snd hj)]

Premises used: ne_of_apply_ne, Prod.snd, Matrix.single_apply_of_col_ne
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
a : r = single (i, k) (j, l) r (i, k) (j, l)
a₁ a₂ : r = r
⊢ single k l r k l = single (i, k) (j, l) r (i, k) (j, l)

Tactic:
rw [single_apply_same, single_apply_same]

Premises used: Matrix.single_apply_same
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
ii : I × K
jj : J × L
r : R
⊢ ((comp I J K L R).symm : (a : Matrix (I × K) (J × L) R) → Matrix I J (Matrix K L R)) (single ii jj r) =
    single ii.1 jj.1 (single ii.2 jj.2 r)

Tactic:
(comp I J K L R).symm_apply_eq.2 <| comp_single_single _ _ _ _ _ |>.symm

Premises used: Iff.mpr, Matrix.comp, Matrix.comp_single_single, Equiv.symm_apply_eq, Eq.symm
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I → J → R
a :
  ∀ (i₁ : I) (j₁ : J) (i₂ : I) (j₂ : J),
    Eq.{u_5 + 1} (α := R)
      ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R)
          (diagonal fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) (i₁, j₁) (i₂, j₂) :
        R)
      (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂) : R)
⊢ Eq (α := Matrix (I × J) (I × J) R)
    ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R)
        (diagonal fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) :
      Matrix (I × J) (I × J) R)
    (diagonal fun (ij : I × J) ↦ d ij.1 ij.2 : Matrix (I × J) (I × J) R)

Tactic:
ext ⟨i₁, j₁⟩ ⟨i₂, j₂⟩
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
a :
  Eq.{u_5 + 1} (α := R) (diagonal (fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) i₁ i₂ j₁ j₂)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂))
⊢ Eq.{u_5 + 1} (α := R)
    ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R)
        (diagonal fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) (i₁, j₁) (i₂, j₂) :
      R)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂) : R)

Tactic:
dsimp [comp_apply]

Premises used: Matrix.comp_apply
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
a :
  ∀ (hi : i₁ ≠ i₂),
    Eq.{u_5 + 1} (α := R) (diagonal (fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) i₁ i₂ j₁ j₂)
      (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂))
a₁ :
  Eq.{u_5 + 1} (α := R) (diagonal (fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) i₁ i₁ j₁ j₂)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂))
⊢ Eq.{u_5 + 1} (α := R) (diagonal (fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) i₁ i₂ j₁ j₂)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂))

Tactic:
obtain hi | rfl := ne_or_eq i₁ i₂

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
hi : i₁ ≠ i₂
a : Eq.{u_5 + 1} (α := R) (0 j₁ j₂) (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂))
a₁ : Eq.{u_5 + 1} (α := R) (0 j₁ j₂) 0
a₂ a₃ : Eq.{u_5 + 1} (α := R) 0 0
⊢ Eq.{u_5 + 1} (α := R) (diagonal (fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) i₁ i₂ j₁ j₂)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂))

Tactic:
rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi),
      Matrix.zero_apply]

Premises used: Matrix.zero_apply, ne_of_apply_ne, Prod.fst, Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
a :
  Eq.{u_5 + 1} (α := R) (diagonal (fun (j : J) ↦ d i₁ j) j₁ j₂)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂))
⊢ Eq.{u_5 + 1} (α := R) (diagonal (fun (i : I) ↦ diagonal fun (j : J) ↦ d i j) i₁ i₁ j₁ j₂)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂))

Tactic:
rw [diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
a :
  ∀ (hj : j₁ ≠ j₂),
    Eq.{u_5 + 1} (α := R) (diagonal (fun (j : J) ↦ d i₁ j) j₁ j₂)
      (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂))
a₁ :
  Eq.{u_5 + 1} (α := R) (diagonal (fun (j : J) ↦ d i₁ j) j₁ j₁)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁))
⊢ Eq.{u_5 + 1} (α := R) (diagonal (fun (j : J) ↦ d i₁ j) j₁ j₂)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂))

Tactic:
obtain hj | rfl := ne_or_eq j₁ j₂

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
hj : j₁ ≠ j₂
a : Eq.{u_5 + 1} (α := R) 0 (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂))
a₁ a₂ : Eq.{u_5 + 1} (α := R) 0 0
⊢ Eq.{u_5 + 1} (α := R) (diagonal (fun (j : J) ↦ d i₁ j) j₁ j₂)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂))

Tactic:
rw [diagonal_apply_ne _ hj, diagonal_apply_ne _ (ne_of_apply_ne Prod.snd hj)]

Premises used: ne_of_apply_ne, Prod.snd, Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I → J → R
i₁ : I
j₁ : J
a : d i₁ j₁ = diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁)
a₁ a₂ : d i₁ j₁ = d (i₁, j₁).1 (i₁, j₁).2
⊢ Eq.{u_5 + 1} (α := R) (diagonal (fun (j : J) ↦ d i₁ j) j₁ j₁)
    (diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁))

Tactic:
rw [diagonal_apply_eq, diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
d : I × J → R
⊢ Eq (α := Matrix I I (Matrix J J R))
    (((comp I I J J R).symm : (a : Matrix (I × J) (I × J) R) → Matrix I I (Matrix J J R)) (diagonal d) :
      Matrix I I (Matrix J J R))
    (diagonal fun (i : I) ↦ diagonal fun (j : J) ↦ d (i, j) : Matrix I I (Matrix J J R))

Tactic:
(comp I I J J R).symm_apply_eq.2 <| (comp_diagonal_diagonal fun i j => d (i, j)).symm

Premises used: Matrix.comp_diagonal_diagonal, Iff.mpr, Matrix.comp, Equiv.symm_apply_eq, Prod.mk, Eq.symm
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
M : Matrix I J (Matrix K L R)
⊢ Eq (α := Matrix (J × K) (I × L) R)
    ((comp J I K L R : (a : Matrix J I (Matrix K L R)) → Matrix (J × K) (I × L) R) Mᵀ : Matrix (J × K) (I × L) R)
    (((comp I J L K R : (a : Matrix I J (Matrix L K R)) → Matrix (I × L) (J × K) R)
          (M.map fun (x : Matrix K L R) ↦ xᵀ))ᵀ :
      Matrix (J × K) (I × L) R)

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
M : Matrix I J (Matrix K L R)
⊢ Eq (α := Matrix (I × L) (J × K) R)
    ((comp I J L K R : (a : Matrix I J (Matrix L K R)) → Matrix (I × L) (J × K) R) (M.map fun (x : Matrix K L R) ↦ xᵀ) :
      Matrix (I × L) (J × K) R)
    (((comp J I K L R : (a : Matrix J I (Matrix K L R)) → Matrix (J × K) (I × L) R) Mᵀ)ᵀ : Matrix (I × L) (J × K) R)

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
M : Matrix (I × K) (J × L) R
⊢ Eq (α := Matrix J I (Matrix L K R))
    (((comp J I L K R).symm : (a : Matrix (J × L) (I × K) R) → Matrix J I (Matrix L K R)) Mᵀ :
      Matrix J I (Matrix L K R))
    ((map (((comp I J K L R).symm : (a : Matrix (I × K) (J × L) R) → Matrix I J (Matrix K L R)) M)
          fun (x : Matrix K L R) ↦ xᵀ)ᵀ :
      Matrix J I (Matrix L K R))

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
M : Matrix I J (Matrix K L R)
⊢ Eq (α := Matrix (J × L) (I × K) R) ((comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) M)ᵀ
    ((comp J I L K R : (a : Matrix J I (Matrix L K R)) → Matrix (J × L) (I × K) R) (Mᵀ.map fun (x : Matrix K L R) ↦ xᵀ))

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : Add R
M : Matrix I J (Matrix K L R)
⊢ Eq (α := Matrix (I × K) (J × L) R)
    ((compAddEquiv I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) M : Matrix (I × K) (J × L) R)
    ((comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) M : Matrix (I × K) (J × L) R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : Add R
M : Matrix (I × K) (J × L) R
⊢ Eq (α := Matrix I J (Matrix K L R))
    ((AddEquiv.symm (compAddEquiv I J K L R) : (a : Matrix (I × K) (J × L) R) → Matrix I J (Matrix K L R)) M :
      Matrix I J (Matrix K L R))
    (((comp I J K L R).symm : (a : Matrix (I × K) (J × L) R) → Matrix I J (Matrix K L R)) M : Matrix I J (Matrix K L R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype I
inst_3 : Fintype J
x x_1 : Matrix I I (Matrix J J R)
a :
  ∀ (i j : I × J),
    (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun (x * x_1) i j =
      ((AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun x * (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun x_1) i j
⊢ (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun (x * x_1) =
    (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun x * (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun x_1

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype I
inst_3 : Fintype J
x x_1 : Matrix I I (Matrix J J R)
i j : I × J
⊢ (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun (x * x_1) i j =
    ((AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun x * (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun x_1) i j

Tactic:
sum_apply .. |>.trans <| .symm <| Fintype.sum_prod_type ..

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.sum_apply, Eq.symm, Fintype.sum_prod_type, Finset.sum, Eq.trans
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype I
inst_3 : Fintype J
x x_1 : Matrix I I (Matrix J J R)
i j : I × J
⊢ (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun (x * x_1) i j =
    ((AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun x * (AddEquiv.toEquiv (compAddEquiv I I J J R)).toFun x_1) i j

Tactic:
exact sum_apply .. |>.trans <| .symm <| Fintype.sum_prod_type ..

Premises used: Matrix.sum_apply, Fintype.sum_prod_type, Eq.trans
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype I
inst_3 : Fintype J
M : Matrix I I (Matrix J J R)
⊢ Eq (α := Matrix (I × J) (I × J) R)
    ((compRingEquiv I J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) M : Matrix (I × J) (I × J) R)
    ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) M : Matrix (I × J) (I × J) R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype I
inst_3 : Fintype J
M : Matrix (I × J) (I × J) R
⊢ Eq (α := Matrix I I (Matrix J J R))
    ((RingEquiv.symm (compRingEquiv I J R) : (a : Matrix (I × J) (I × J) R) → Matrix I I (Matrix J J R)) M :
      Matrix I I (Matrix J J R))
    (((comp I I J J R).symm : (a : Matrix (I × J) (I × J) R) → Matrix I I (Matrix J J R)) M : Matrix I I (Matrix J J R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R_1 : Type u_5
R' : Type u_6
inst : AddCommMonoid R_1
inst_1 : Mul R_1
inst_2 : Fintype I
inst_3 : Fintype J
R : Type u_7
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : DecidableEq I
inst_7 : IsStablyFiniteRing R
⊢ IsStablyFiniteRing (Matrix I I R)

Tactic:
⟨fun n ↦ .of_injective (MonoidHom.mk ⟨_, comp_one⟩ (compRingEquiv (Fin n) I R).map_mul)
    (RingEquiv.injective _)⟩

Premises used: RingEquiv.map_mul, OneHom.mk, RingEquiv.injective, MonoidHom.mk, IsDedekindFiniteMonoid.of_injective, IsStablyFiniteRing.mk, Matrix.compRingEquiv, Fin, DFunLike.coe
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
K : Type u_7
inst : CommSemiring K
inst_1 : Semiring R
inst_2 : Fintype I
inst_3 : Fintype J
inst_4 : Algebra K R
inst_5 : DecidableEq I
inst_6 : DecidableEq J
M : Matrix I I (Matrix J J R)
⊢ Eq (α := Matrix (I × J) (I × J) R)
    ((compAlgEquiv I J R K : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) M : Matrix (I × J) (I × J) R)
    ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) M : Matrix (I × J) (I × J) R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
K : Type u_7
inst : CommSemiring K
inst_1 : Semiring R
inst_2 : Fintype I
inst_3 : Fintype J
inst_4 : Algebra K R
inst_5 : DecidableEq I
inst_6 : DecidableEq J
M : Matrix (I × J) (I × J) R
⊢ Eq (α := Matrix I I (Matrix J J R))
    ((AlgEquiv.symm (compAlgEquiv I J R K) : (a : Matrix (I × J) (I × J) R) → Matrix I I (Matrix J J R)) M :
      Matrix I I (Matrix J J R))
    (((comp I I J J R).symm : (a : Matrix (I × J) (I × J) R) → Matrix I I (Matrix J J R)) M : Matrix I I (Matrix J J R))

Tactic:
rfl

Premises used: rfl