awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
h :
  ∀ (x : Matrix l m A) (i : l) (j : o),
    Eq.{u_6 + 1} (α := A) ((mulRightLinearMap l R (a * b) : (a : Matrix l m A) → Matrix l o A) x i j : A)
      ((mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a : (a : Matrix l m A) → Matrix l o A) x i j : A)
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l o A) (mulRightLinearMap l R (a * b))
    (mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
x : Matrix l m A
i : l
j : o
⊢ Eq.{u_6 + 1} (α := A) ((mulRightLinearMap l R (a * b) : (a : Matrix l m A) → Matrix l o A) x i j : A)
    ((mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a : (a : Matrix l m A) → Matrix l o A) x i j : A)

Tactic:
simp only [mulRightLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]

Premises used: Matrix.mul_assoc, LinearMap.comp_apply, mulRightLinearMap_apply
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : CommSemiring R
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
a : Matrix l m A
b : Matrix n o A
h :
  ∀ (c : Matrix m n A),
    Eq (α := Matrix l o A)
      ((mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b : (a : Matrix m n A) → Matrix l o A) c : Matrix l o A)
      ((mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l o A) c : Matrix l o A)
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l o A) (mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b)
    (mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a)

Tactic:
ext c : 1
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : CommSemiring R
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
a : Matrix l m A
b : Matrix n o A
c : Matrix m n A
⊢ Eq (α := Matrix l o A)
    ((mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b : (a : Matrix m n A) → Matrix l o A) c : Matrix l o A)
    ((mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l o A) c : Matrix l o A)

Tactic:
(Matrix.mul_assoc a c b).symm

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mul_assoc, Eq.symm, Finset.sum
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : CommSemiring R
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
a : Matrix l m A
b : Matrix n o A
c : Matrix m n A
⊢ Eq (α := Matrix l o A)
    ((mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b : (a : Matrix m n A) → Matrix l o A) c : Matrix l o A)
    ((mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l o A) c : Matrix l o A)

Tactic:
exact (Matrix.mul_assoc a c b).symm

Premises used: Matrix.mul_assoc, Eq.symm
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix m n A) (mulLeftLinearMap n R 1) LinearMap.id

Tactic:
LinearMap.ext fun _ => Matrix.one_mul _

Premises used: LinearMap.ext, Matrix.one_mul
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
mp : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0 → a = 0
mpr : a = 0 → Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0 ↔ a = 0

Tactic:
constructor
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
mp : ∀ (inhabited_h : Inhabited n), a = 0
⊢ a = 0

Tactic:
inhabit n
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
inhabited_h : Inhabited n
mp : ∀ (i : l) (j : m), a i j = 0 i j
⊢ a = 0

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
inhabited_h : Inhabited n
i : l
j : m
⊢ Eq (α := Matrix l n A)
    ((mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)
    ((0 : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)

Tactic:
replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
inhabited_h : Inhabited n
i : l
j : m
h :
  Eq (α := Matrix l n A)
    ((mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)
    ((0 : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)
⊢ a i j = 0 i j

Tactic:
simpa using Matrix.ext_iff.2 h i default

Premises used: Iff.mpr, Inhabited.default, Matrix.ext_iff
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
inhabited_h : Inhabited n
i : l
j : m
mp mp₁ mp₂ :
  ∀
    (h :
      Eq (α := Matrix l n A)
        ((mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)
        ((0 : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)),
    a i j = 0 i j
⊢ a i j = 0 i j

Tactic:
classical
    replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)
    simpa using Matrix.ext_iff.2 h i default

Premises used: Iff.mpr, Inhabited.default, Matrix.ext_iff
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : a = 0
mpr : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R 0) 0
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0

Tactic:
rw [h]
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : a = 0
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R 0) 0

Tactic:
mulLeftLinearMap_zero_eq_zero _ _

Premises used: mulLeftLinearMap_zero_eq_zero
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : a = 0
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R 0) 0

Tactic:
exact mulLeftLinearMap_zero_eq_zero _ _

Premises used: mulLeftLinearMap_zero_eq_zero
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix m m A
k : ℕ
rw : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R 1)
rw₂ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 LinearMap.id
rw₃ rw₄ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) LinearMap.id LinearMap.id
⊢ HPow.hPow (α := Matrix m n A →ₗ[R] Matrix m n A) (β := ℕ) (mulLeftLinearMap n R a) 0 =
    mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0)

Tactic:
rw [pow_zero, pow_zero, mulLeftLinearMap_one, Module.End.one_eq_id]

Premises used: Module.End.one_eq_id, pow_zero, mulLeftLinearMap_one
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
m : Type u_2
n_1 : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix m m A
k n : ℕ
rw :
  HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) n * mulLeftLinearMap n_1 R a =
    mulLeftLinearMap n_1 R (a ^ (n + 1))
rw₁ :
  HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) n * mulLeftLinearMap n_1 R a =
    mulLeftLinearMap n_1 R (a ^ n * a)
rw₂ :
  HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) n * mulLeftLinearMap n_1 R a =
    mulLeftLinearMap n_1 R (a ^ n) ∘ₗ mulLeftLinearMap n_1 R a
rw₃ :
  HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) n ∘ₗ mulLeftLinearMap n_1 R a =
    mulLeftLinearMap n_1 R (a ^ n) ∘ₗ mulLeftLinearMap n_1 R a
rw₄ rw₅ :
  Eq (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R (a ^ n) ∘ₗ mulLeftLinearMap n_1 R a)
    (mulLeftLinearMap n_1 R (a ^ n) ∘ₗ mulLeftLinearMap n_1 R a)
⊢ HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) (n + 1) =
    mulLeftLinearMap n_1 R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, mulLeftLinearMap_mul, Module.End.mul_eq_comp, pow_mulLeftLinearMap]

Premises used: Module.End.mul_eq_comp, pow_succ, mulLeftLinearMap_mul
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R 1) LinearMap.id

Tactic:
LinearMap.ext fun _ => Matrix.mul_one _

Premises used: LinearMap.ext, Matrix.mul_one
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
mp : Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0 → a = 0
mpr : a = 0 → Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0 ↔ a = 0

Tactic:
constructor
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
h : Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0
mp : ∀ (inhabited_h : Inhabited l), a = 0
⊢ a = 0

Tactic:
inhabit l
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
h : Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0
inhabited_h : Inhabited l
mp : ∀ (i : m) (j : n), a i j = 0 i j
⊢ a = 0

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
h : Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0
inhabited_h : Inhabited l
i : m
j : n
⊢ Eq (α := Matrix l n A)
    ((mulRightLinearMap l R a : (a : Matrix l m A) → Matrix l n A) (Matrix.single default i 1) : Matrix l n A)
    ((0 : (a : Matrix l m A) → Matrix l n A) (Matrix.single default i 1) : Matrix l n A)

Tactic:
replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
inhabited_h : Inhabited l
i : m
j : n
h :
  Eq (α := Matrix l n A)
    ((mulRightLinearMap l R a : (a : Matrix l m A) → Matrix l n A) (Matrix.single default i 1) : Matrix l n A)
    ((0 : (a : Matrix l m A) → Matrix l n A) (Matrix.single default i 1) : Matrix l n A)
⊢ a i j = 0 i j

Tactic:
simpa using Matrix.ext_iff.2 h default j

Premises used: Iff.mpr, Inhabited.default, Matrix.ext_iff
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
h : Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0
inhabited_h : Inhabited l
i : m
j : n
mp mp₁ mp₂ :
  ∀
    (h :
      Eq (α := Matrix l n A)
        ((mulRightLinearMap l R a : (a : Matrix l m A) → Matrix l n A) (Matrix.single default i 1) : Matrix l n A)
        ((0 : (a : Matrix l m A) → Matrix l n A) (Matrix.single default i 1) : Matrix l n A)),
    a i j = 0 i j
⊢ a i j = 0 i j

Tactic:
classical
    replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)
    simpa using Matrix.ext_iff.2 h default j

Premises used: Iff.mpr, Inhabited.default, Matrix.ext_iff
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
h : a = 0
mpr : Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R 0) 0
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0

Tactic:
rw [h]
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
h : a = 0
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R 0) 0

Tactic:
mulRightLinearMap_zero_eq_zero _ _

Premises used: mulRightLinearMap_zero_eq_zero
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
a : Matrix m n A
inst_5 : Nonempty l
h : a = 0
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R 0) 0

Tactic:
exact mulRightLinearMap_zero_eq_zero _ _

Premises used: mulRightLinearMap_zero_eq_zero
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
a : Matrix m m A
k : ℕ
rw : Eq (α := Matrix l m A →ₗ[R] Matrix l m A) 1 (mulRightLinearMap l R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq (α := Matrix l m A →ₗ[R] Matrix l m A) 1 (mulRightLinearMap l R 1)
rw₂ : Eq (α := Matrix l m A →ₗ[R] Matrix l m A) 1 LinearMap.id
rw₃ rw₄ : Eq (α := Matrix l m A →ₗ[R] Matrix l m A) LinearMap.id LinearMap.id
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (β := ℕ) (mulRightLinearMap l R a) 0 =
    mulRightLinearMap l R (HPow.hPow (β := ℕ) a 0)

Tactic:
rw [pow_zero, pow_zero, mulRightLinearMap_one, Module.End.one_eq_id]

Premises used: mulRightLinearMap_one, Module.End.one_eq_id, pow_zero
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
a : Matrix m m A
k n : ℕ
rw :
  HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) n * mulRightLinearMap l R a =
    mulRightLinearMap l R (a ^ (n + 1))
rw₁ :
  HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) n * mulRightLinearMap l R a =
    mulRightLinearMap l R (a * a ^ n)
rw₂ :
  HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) n * mulRightLinearMap l R a =
    mulRightLinearMap l R (a ^ n) ∘ₗ mulRightLinearMap l R a
rw₃ :
  HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) n ∘ₗ mulRightLinearMap l R a =
    mulRightLinearMap l R (a ^ n) ∘ₗ mulRightLinearMap l R a
rw₄ rw₅ :
  Eq (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R (a ^ n) ∘ₗ mulRightLinearMap l R a)
    (mulRightLinearMap l R (a ^ n) ∘ₗ mulRightLinearMap l R a)
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) (n + 1) =
    mulRightLinearMap l R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ', mulRightLinearMap_mul, Module.End.mul_eq_comp, pow_mulRightLinearMap]

Premises used: Module.End.mul_eq_comp, pow_succ, mulRightLinearMap_mul, pow_succ'
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
α : Type u_12
inst : Fintype m
inst_1 : Fintype n
inst_2 : Mul α
inst_3 : AddCommMonoid α
v w : m ⊕ n → α
⊢ v ⬝ᵥ w = v ∘ Sum.inl ⬝ᵥ w ∘ Sum.inl + v ∘ Sum.inr ⬝ᵥ w ∘ Sum.inr

Tactic:
Fintype.sum_sum_type _

Premises used: dotProduct, Fintype.sum_sum_type
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n
j : l
⊢ fromBlocks A B C D (Sum.inl i) (Sum.inl j) = A i j

Tactic:
rfl

Premises used: Matrix.fromBlocks, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n
j : m
⊢ fromBlocks A B C D (Sum.inl i) (Sum.inr j) = B i j

Tactic:
rfl

Premises used: Matrix.fromBlocks, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : o
j : l
⊢ fromBlocks A B C D (Sum.inr i) (Sum.inl j) = C i j

Tactic:
rfl

Premises used: Matrix.fromBlocks, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : o
j : m
⊢ fromBlocks A B C D (Sum.inr i) (Sum.inr j) = D i j

Tactic:
rfl

Premises used: Matrix.fromBlocks, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
a : ∀ (i : n ⊕ o) (j : l ⊕ m), fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
i : n ⊕ o
j : l ⊕ m
a : ∀ (val : n), fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) j = M (Sum.inl val) j
a₁ : ∀ (val : o), fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) j = M (Sum.inr val) j
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j

Tactic:
rcases i with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val : n
a :
  ∀ (val_1 : l),
    fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) (Sum.inl val_1) =
      M (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) (Sum.inr val_1) =
      M (Sum.inl val) (Sum.inr val_1)
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) j = M (Sum.inl val) j

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val : o
a :
  ∀ (val_1 : l),
    fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) (Sum.inl val_1) =
      M (Sum.inr val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) (Sum.inr val_1) =
      M (Sum.inr val) (Sum.inr val_1)
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) j = M (Sum.inr val) j

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val : n
val_1 : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) (Sum.inl val_1) =
    M (Sum.inl val) (Sum.inl val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val : n
val_1 : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) (Sum.inr val_1) =
    M (Sum.inl val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val : o
val_1 : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) (Sum.inl val_1) =
    M (Sum.inr val) (Sum.inl val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val : o
val_1 : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) (Sum.inr val_1) =
    M (Sum.inr val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D).toBlocks₁₁ = A

Tactic:
rfl

Premises used: Matrix.fromBlocks, Matrix.toBlocks₁₁, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D).toBlocks₁₂ = B

Tactic:
rfl

Premises used: Matrix.fromBlocks, Matrix.toBlocks₁₂, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D).toBlocks₂₁ = C

Tactic:
rfl

Premises used: Matrix.fromBlocks, Matrix.toBlocks₂₁, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D).toBlocks₂₂ = D

Tactic:
rfl

Premises used: Matrix.fromBlocks, Matrix.toBlocks₂₂, rfl, Sum.elim