awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
have 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')
Tactic: obtain hj | rfl := ne_or_eq j j'
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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')
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
have a₁ : 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'
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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'
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
have a : 0 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]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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')
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
have a₁ : Eq.{u_5 + 1} (α := R) (0 k' l') 0
Tactic: rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
have a₂ : Eq.{u_5 + 1} (α := R) 0 0
Tactic: rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ single i j (single k l r) i j k' l' = single (i, k) (j, l) r (i, k') (j, l')
have a : single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')
Tactic: rw [single_apply_same]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')
have a : ∀ (hk : k ≠ k'), 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'
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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')
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')
have a₁ : 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'
Cleared hypotheses: k'
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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'
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')
have a : 0 = 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)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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')
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')
have a₁ : Eq.{u_5 + 1} (α := R) 0 0
Tactic: rw [single_apply_of_row_ne hk,
      single_apply_of_row_ne (ne_of_apply_ne Prod.snd hk)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')
have a : ∀ (hj : l ≠ 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'
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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')
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')
have a₁ : 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'
Cleared hypotheses: l'
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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'
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')
have a : 0 = 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)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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')
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')
have a₁ : Eq.{u_5 + 1} (α := R) 0 0
Tactic: rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.snd hj)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ single k l r k l = single (i, k) (j, l) r (i, k) (j, l)
have a : r = single (i, k) (j, l) r (i, k) (j, l)
Tactic: rw [single_apply_same, single_apply_same]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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)
⊢ single k l r k l = single (i, k) (j, l) r (i, k) (j, l)
have a₁ : r = r
Tactic: rw [single_apply_same, single_apply_same]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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 × 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)
have 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)
Tactic: ext ⟨i₁, j₁⟩ ⟨i₂, j₂⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ 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)
have 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₂))
Tactic: dsimp [comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ 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₂))
have 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₂))
Tactic: obtain hi | rfl := ne_or_eq i₁ i₂
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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₂))
⊢ 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₂))
have 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₂))
Tactic: obtain hi | rfl := ne_or_eq i₁ i₂
Cleared hypotheses: i₂
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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₂
⊢ 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₂))
have a : Eq.{u_5 + 1} (α := R) (0 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]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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₂))
⊢ 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₂))
have a₁ : Eq.{u_5 + 1} (α := R) (0 j₁ j₂) 0
Tactic: rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi),
      Matrix.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ 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₂))
have a₂ : Eq.{u_5 + 1} (α := R) 0 0
Tactic: rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi),
      Matrix.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ 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₂))
have 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₂))
Tactic: rw [diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ 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₂))
have 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₂))
Tactic: obtain hj | rfl := ne_or_eq j₁ j₂
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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₂))
⊢ 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₂))
have 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₁))
Tactic: obtain hj | rfl := ne_or_eq j₁ j₂
Cleared hypotheses: j₂
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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₂
⊢ 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₂))
have a : Eq.{u_5 + 1} (α := R) 0 (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)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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₂))
⊢ 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₂))
have a₁ : Eq.{u_5 + 1} (α := R) 0 0
Tactic: rw [diagonal_apply_ne _ hj, diagonal_apply_ne _ (ne_of_apply_ne Prod.snd hj)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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
⊢ 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₁))
have a : d i₁ j₁ = diagonal (fun (ij : I × J) ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁)
Tactic: rw [diagonal_apply_eq, diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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₁)
⊢ 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₁))
have a₁ : d i₁ j₁ = d (i₁, j₁).1 (i₁, j₁).2
Tactic: rw [diagonal_apply_eq, diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
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)
⊢ (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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.DMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
⊢ (M.map (α := α) (β := β) f).map (α := β) (β := γ) g =
    M.map (α := α) (β := fun (x : m) (x_1 : n) ↦ γ x x_1) fun (x : m) (x_1 : n) (x_2 : α x x_1) ↦ g (f x_2)
have a : ∀ (i : m) (j : n),
  (M.map (α := α) (β := β) f).map (α := β) (β := γ) g i j =
    M.map (α := α) (β := fun (x : m) (x_1 : n) ↦ γ x x_1) (fun (x : m) (x_1 : n) (x_2 : α x x_1) ↦ g (f x_2)) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.DMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), Eq (α := β i j) (f 0) 0
⊢ map (α := α) 0 (β := β) f = 0
have a : ∀ (i : m) (j : n), map (α := α) 0 (β := β) f i j = 0 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.DMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → AddMonoidHom.{v, w} (α i j) (β i j)
M N : DMatrix m n α
⊢ ((M + N).map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) =
    HAdd.hAdd (α := DMatrix m n β) (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
      (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
have a : ∀ (i : m) (j : n),
  (M + N).map (α := α) (β := β) (fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j =
    HAdd.hAdd (α := DMatrix m n β) (β := DMatrix m n β)
      (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
      (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.DMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → AddMonoidHom.{v, w} (α i j) (β i j)
M N : DMatrix m n α
⊢ ((M - N).map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) =
    HSub.hSub (α := DMatrix m n β) (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
      (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
have a : ∀ (i : m) (j : n),
  (M - N).map (α := α) (β := β) (fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j =
    HSub.hSub (α := DMatrix m n β) (β := DMatrix m n β)
      (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
      (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.DMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : IsEmpty m
M N : DMatrix m n α
⊢ M = N
have a : ∀ (i : m) (j : n), M i j = N i j
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Matrix.DMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : IsEmpty n
M N : DMatrix m n α
⊢ M = N
have a : ∀ (i : m) (j : n), M i j = N i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d₁ d₂ : n → α
h : ∀ (i : n), d₁ i = d₂ i
⊢ diagonal d₁ = diagonal d₂
have rw : diagonal d₂ = diagonal d₂
Tactic: rw [show d₁ = d₂ from funext h]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ 0) 0
have a : ∀ (i j : n), Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ 0) i j) (0 i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
⊢ (diagonal v)ᵀ = diagonal v
have a : ∀ (i j : n), (diagonal v)ᵀ i j = diagonal v i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i j : n
⊢ (diagonal v)ᵀ i j = diagonal v i j
have pos : ∀ (h : i = j), (diagonal v)ᵀ i j = diagonal v i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i j : n
pos : ∀ (h : i = j), (diagonal v)ᵀ i j = diagonal v i j
⊢ (diagonal v)ᵀ i j = diagonal v i j
have neg : ∀ (h : ¬i = j), (diagonal v)ᵀ i j = diagonal v i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddZeroClass α
d₁ d₂ : n → α
⊢ diagonal d₁ + diagonal d₂ = diagonal fun (i : n) ↦ d₁ i + d₂ i
have a : ∀ (i j : n), (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddZeroClass α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
have pos : ∀ (h : i = j), (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddZeroClass α
d₁ d₂ : n → α
i j : n
pos : ∀ (h : i = j), (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
have neg : ∀ (h : ¬i = j), (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
R : Type u_7
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : SMulZeroClass R α
r : R
d : n → α
⊢ diagonal (r • d) = r • diagonal d
have a : ∀ (i j : n), diagonal (r • d) i j = (r • diagonal d) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
R : Type u_7
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : SMulZeroClass R α
r : R
d : n → α
i j : n
⊢ diagonal (r • d) i j = (r • diagonal d) i j
have pos : ∀ (h : i = j), diagonal (r • d) i j = (r • diagonal d) i j
Tactic: by_cases h : i = j