awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
rw : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ (k + (l - k)) = 0
rw₁ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* (M ^ k * M ^ (l - k)) = 0
rw₂ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k ᵥ* M ^ (l - k) = 0
⊢ Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ l = 0
have rw₃ : 0 ᵥ* M ^ (l - k) = 0
Tactic: rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
rw : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ (k + (l - k)) = 0
rw₁ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* (M ^ k * M ^ (l - k)) = 0
rw₂ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k ᵥ* M ^ (l - k) = 0
rw₃ : 0 ᵥ* M ^ (l - k) = 0
⊢ Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ l = 0
have rw₄ : Eq (α := n → R) 0 0
Tactic: rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).col i = 0
h' : k ≤ l
⊢ (M ^ l).col i = 0
have h'₁ : l = l - k + k
Tactic: replace h' : l = (l - k) + k := by lia
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).col i = 0
h' : l = l - k + k
⊢ (M ^ l).col i = 0
have rw : ∀ (h : M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0) (h' : l = l - k + k),
  M ^ l *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
Tactic: rw [← mulVec_single_one] at h ⊢
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
h' : l = l - k + k
⊢ M ^ l *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
have rw : M ^ (l - k + k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
Tactic: rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
h' : l = l - k + k
rw : M ^ (l - k + k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
⊢ M ^ l *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
have rw₁ : (M ^ (l - k) * M ^ k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
Tactic: rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
h' : l = l - k + k
rw : M ^ (l - k + k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₁ : (M ^ (l - k) * M ^ k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
⊢ M ^ l *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
have rw₂ : M ^ (l - k) *ᵥ M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
Tactic: rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
h' : l = l - k + k
rw : M ^ (l - k + k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₁ : (M ^ (l - k) * M ^ k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₂ : M ^ (l - k) *ᵥ M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
⊢ M ^ l *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
have rw₃ : M ^ (l - k) *ᵥ 0 = 0
Tactic: rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
h' : l = l - k + k
rw : M ^ (l - k + k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₁ : (M ^ (l - k) * M ^ k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₂ : M ^ (l - k) *ᵥ M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₃ : M ^ (l - k) *ᵥ 0 = 0
⊢ M ^ l *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
have rw₄ : Eq (α := n → R) 0 0
Tactic: rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : AddCommMonoid α
inst_1 : CommMagma α
inst_2 : Fintype n
M : Matrix m n α
N : Matrix n l α
⊢ (M * N)ᵀ = Nᵀ * Mᵀ
have a : ∀ (i : l) (j : m), (M * N)ᵀ i j = (Nᵀ * Mᵀ) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : Mul α
inst_3 : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
⊢ HMul.hMul (β := Matrix n p α) (M.submatrix e₁ id) (N.submatrix (⇑e₂ : (a : n) → o) id) =
    HMul.hMul (α := Matrix l o α) (M.submatrix e₁ (⇑e₂.symm : (a : o) → n)) N
have a : ∀ (i : l) (j : p),
  HMul.hMul (β := Matrix n p α) (M.submatrix e₁ id) (N.submatrix (⇑e₂ : (a : n) → o) id) i j =
    HMul.hMul (α := Matrix l o α) (M.submatrix e₁ (⇑e₂.symm : (a : o) → n)) N i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : Mul α
inst_3 : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
⊢ HMul.hMul (α := Matrix m o α) (M.submatrix id (⇑e₂ : (a : o) → n)) (N.submatrix id e₁) =
    HMul.hMul (β := Matrix n l α) M (N.submatrix (⇑e₂.symm : (a : n) → o) e₁)
have a : ∀ (i : m) (j : l),
  HMul.hMul (α := Matrix m o α) (M.submatrix id (⇑e₂ : (a : o) → n)) (N.submatrix id e₁) i j =
    HMul.hMul (β := Matrix n l α) M (N.submatrix (⇑e₂.symm : (a : n) → o) e₁) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
⊢ HMul.hMul (β := Matrix n l α) M (submatrix (m := o) 1 (⇑e₁ : (a : n) → o) e₂) =
    M.submatrix id ((⇑e₁.symm : (a : o) → n) ∘ e₂)
have intro : ∀ (val : Fintype o),
  HMul.hMul (β := Matrix n l α) M (submatrix (m := o) 1 (⇑e₁ : (a : n) → o) e₂) =
    M.submatrix id ((⇑e₁.symm : (a : o) → n) ∘ e₂)
Tactic: cases nonempty_fintype o
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val : Fintype o
A : Matrix m o α := M.submatrix id (⇑e₁.symm : (a : o) → n)
⊢ HMul.hMul (β := Matrix n l α) M (submatrix (m := o) 1 (⇑e₁ : (a : n) → o) e₂) =
    M.submatrix id ((⇑e₁.symm : (a : o) → n) ∘ e₂)
have this : M = A.submatrix id (⇑e₁ : (a : n) → o)
Tactic: have : M = A.submatrix id e₁ := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val : Fintype o
A : Matrix m o α := M.submatrix id (⇑e₁.symm : (a : o) → n)
this : M = A.submatrix id (⇑e₁ : (a : n) → o)
⊢ HMul.hMul (β := Matrix n l α) M (submatrix (m := o) 1 (⇑e₁ : (a : n) → o) e₂) =
    M.submatrix id ((⇑e₁.symm : (a : o) → n) ∘ e₂)
have intro : (A * 1).submatrix id e₂ =
  submatrix.{v, u_2, u_2, u_3, u_1} (n := n) (A.submatrix id (⇑e₁ : (a : n) → o)) id ((⇑e₁.symm : (a : o) → n) ∘ e₂)
Tactic: rw [this, submatrix_mul_equiv]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype m
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
⊢ HMul.hMul (α := Matrix l m α) (submatrix (n := o) 1 e₁ (⇑e₂ : (a : m) → o)) M =
    M.submatrix ((⇑e₂.symm : (a : o) → m) ∘ e₁) id
have intro : ∀ (val : Fintype o),
  HMul.hMul (α := Matrix l m α) (submatrix (n := o) 1 e₁ (⇑e₂ : (a : m) → o)) M =
    M.submatrix ((⇑e₂.symm : (a : o) → m) ∘ e₁) id
Tactic: cases nonempty_fintype o
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype m
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm : (a : o) → m) id
⊢ HMul.hMul (α := Matrix l m α) (submatrix (n := o) 1 e₁ (⇑e₂ : (a : m) → o)) M =
    M.submatrix ((⇑e₂.symm : (a : o) → m) ∘ e₁) id
have this : M = A.submatrix (⇑e₂ : (a : m) → o) id
Tactic: have : M = A.submatrix e₂ id := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype m
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm : (a : o) → m) id
this : M = A.submatrix (⇑e₂ : (a : m) → o) id
⊢ HMul.hMul (α := Matrix l m α) (submatrix (n := o) 1 e₁ (⇑e₂ : (a : m) → o)) M =
    M.submatrix ((⇑e₂.symm : (a : o) → m) ∘ e₁) id
have intro : (1 * A).submatrix e₁ id =
  submatrix.{v, u_1, u_2, u_3, u_3} (m := m) (A.submatrix (⇑e₂ : (a : m) → o) id) ((⇑e₂.symm : (a : o) → m) ∘ e₁) id
Tactic: rw [this, submatrix_mul_equiv]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Fintype n
inst_2 : AddCommMonoid α
inst_3 : Mul α
e : m ≃ n
M : Matrix m n α
⊢ M.submatrix id (⇑e : (a : m) → n) * Mᵀ.submatrix (⇑e : (a : m) → n) id = M * Mᵀ
have rw : (M * Mᵀ).submatrix id id = M * Mᵀ
Tactic: rw [submatrix_mul_equiv, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Fintype n
inst_2 : AddCommMonoid α
inst_3 : Mul α
e : m ≃ n
M : Matrix m n α
rw : (M * Mᵀ).submatrix id id = M * Mᵀ
⊢ M.submatrix id (⇑e : (a : m) → n) * Mᵀ.submatrix (⇑e : (a : m) → n) id = M * Mᵀ
have rw₁ : M * Mᵀ = M * Mᵀ
Tactic: rw [submatrix_mul_equiv, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1
have rw : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
    ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
  B * A = 1
Tactic: rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
rw :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
    B * A = 1
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1
have rw₁ : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
    (submatrix.{u_12, u_11, u_10, u_10, u_11} (m := m) (n := m) 1 (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) ↔
  B * A = 1
Tactic: rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
rw :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
    B * A = 1
rw₁ :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      (submatrix.{u_12, u_11, u_10, u_10, u_11} (m := m) (n := m) 1 (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) ↔
    B * A = 1
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1
have rw₂ : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) 1 ↔ B * A = 1
Tactic: rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
rw :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
    B * A = 1
rw₁ :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      (submatrix.{u_12, u_11, u_10, u_10, u_11} (m := m) (n := m) 1 (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) ↔
    B * A = 1
rw₂ : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) 1 ↔ B * A = 1
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1
have rw₃ : HMul.hMul (α := Matrix n n R) (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
      (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m)) =
    1 ↔
  B * A = 1
Tactic: rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
rw :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
    B * A = 1
rw₁ :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      (submatrix.{u_12, u_11, u_10, u_10, u_11} (m := m) (n := m) 1 (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) ↔
    B * A = 1
rw₂ : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) 1 ↔ B * A = 1
rw₃ :
  HMul.hMul (α := Matrix n n R) (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m)) =
      1 ↔
    B * A = 1
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1
have rw₄ : HMul.hMul (α := Matrix n n R) (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m))
      (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n)) =
    1 ↔
  B * A = 1
Tactic: rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
rw :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
    B * A = 1
rw₁ :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      (submatrix.{u_12, u_11, u_10, u_10, u_11} (m := m) (n := m) 1 (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) ↔
    B * A = 1
rw₂ : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) 1 ↔ B * A = 1
rw₃ :
  HMul.hMul (α := Matrix n n R) (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m)) =
      1 ↔
    B * A = 1
rw₄ :
  HMul.hMul (α := Matrix n n R) (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m))
        (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n)) =
      1 ↔
    B * A = 1
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1
have rw₅ : Eq (α := Matrix n n R) ((B * A).submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑(Equiv.refl n) : (a : n) → n)) 1 ↔ B * A = 1
Tactic: rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
rw :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
    B * A = 1
rw₁ :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      (submatrix.{u_12, u_11, u_10, u_10, u_11} (m := m) (n := m) 1 (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) ↔
    B * A = 1
rw₂ : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) 1 ↔ B * A = 1
rw₃ :
  HMul.hMul (α := Matrix n n R) (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m)) =
      1 ↔
    B * A = 1
rw₄ :
  HMul.hMul (α := Matrix n n R) (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m))
        (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n)) =
      1 ↔
    B * A = 1
rw₅ :
  Eq (α := Matrix n n R) ((B * A).submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑(Equiv.refl n) : (a : n) → n)) 1 ↔
    B * A = 1
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1
have rw₆ : (B * A).submatrix id id = 1 ↔ B * A = 1
Tactic: rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
rw :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
    B * A = 1
rw₁ :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      (submatrix.{u_12, u_11, u_10, u_10, u_11} (m := m) (n := m) 1 (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) ↔
    B * A = 1
rw₂ : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) 1 ↔ B * A = 1
rw₃ :
  HMul.hMul (α := Matrix n n R) (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m)) =
      1 ↔
    B * A = 1
rw₄ :
  HMul.hMul (α := Matrix n n R) (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m))
        (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n)) =
      1 ↔
    B * A = 1
rw₅ :
  Eq (α := Matrix n n R) ((B * A).submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑(Equiv.refl n) : (a : n) → n)) 1 ↔
    B * A = 1
rw₆ : (B * A).submatrix id id = 1 ↔ B * A = 1
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1
have rw₇ : B * A = 1 ↔ B * A = 1
Tactic: rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
⊢ HMul.hMul (α := Matrix l m α) f.toMatrix M i j =
    Option.casesOn (motive := fun (x : Option m) ↦ α) ((f : (a : l) → Option m) i) 0 fun (fi : m) ↦ M fi j
have dsimp : Eq.{u_5 + 1} (α := α)
  (∑ j_1 : m, (if Membership.mem (γ := Option m) ((f : (a : l) → Option m) i : Option m) j_1 then 1 else 0) * M j_1 j :
    α)
  (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) ((f : (a : l) → Option m) i) : α)
Tactic: dsimp [toMatrix, Matrix.mul_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
⊢ Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m,
        (if Membership.mem (γ := Option m) ((f : (a : l) → Option m) i : Option m) j_1 then 1 else 0) * M j_1 j :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) ((f : (a : l) → Option m) i) : α)
have none : ∀ (h : Eq.{u_3 + 1} (α := Option m) ((f : (a : l) → Option m) i : Option m) (none : Option m)),
  Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if Membership.mem (γ := Option m) none j_1 then 1 else 0) * M j_1 j : α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) none : α)
Tactic: rcases h : f i with - | fi