awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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)
⊢ 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))
have 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
Tactic: rw [pow_succ, pow_succ, mulLeftLinearMap_mul, Module.End.mul_eq_comp, pow_mulLeftLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ 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))
have 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
Tactic: rw [pow_succ, pow_succ, mulLeftLinearMap_mul, Module.End.mul_eq_comp, pow_mulLeftLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ 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))
have 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)
Tactic: rw [pow_succ, pow_succ, mulLeftLinearMap_mul, Module.End.mul_eq_comp, pow_mulLeftLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0 ↔ a = 0
have mp : Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0 → a = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0 ↔ a = 0
have mpr : a = 0 → Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R a) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ a = 0
have mp : ∀ (inhabited_h : Inhabited l), a = 0
Tactic: inhabit l
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ a = 0
have mp : ∀ (i : m) (j : n), a i j = 0 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (hypothesis)
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
⊢ a i j = 0 i j
have 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)
Tactic: replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ a i j = 0 i j
have 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
Tactic: classical
    replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)
    simpa using Matrix.ext_iff.2 h default j
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 a) 0
have mpr : Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R 0) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : ℕ
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (β := ℕ) (mulRightLinearMap l R a) 0 =
    mulRightLinearMap l R (HPow.hPow (β := ℕ) a 0)
have rw : Eq (α := Matrix l m A →ₗ[R] Matrix l m A) 1 (mulRightLinearMap l R (HPow.hPow (β := ℕ) a 0))
Tactic: rw [pow_zero, pow_zero, mulRightLinearMap_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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))
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (β := ℕ) (mulRightLinearMap l R a) 0 =
    mulRightLinearMap l R (HPow.hPow (β := ℕ) a 0)
have rw₁ : Eq (α := Matrix l m A →ₗ[R] Matrix l m A) 1 (mulRightLinearMap l R 1)
Tactic: rw [pow_zero, pow_zero, mulRightLinearMap_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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)
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (β := ℕ) (mulRightLinearMap l R a) 0 =
    mulRightLinearMap l R (HPow.hPow (β := ℕ) a 0)
have rw₂ : Eq (α := Matrix l m A →ₗ[R] Matrix l m A) 1 LinearMap.id
Tactic: rw [pow_zero, pow_zero, mulRightLinearMap_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (β := ℕ) (mulRightLinearMap l R a) 0 =
    mulRightLinearMap l R (HPow.hPow (β := ℕ) a 0)
have rw₃ : Eq (α := Matrix l m A →ₗ[R] Matrix l m A) LinearMap.id LinearMap.id
Tactic: rw [pow_zero, pow_zero, mulRightLinearMap_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : ℕ
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) (n + 1) =
    mulRightLinearMap l R (a ^ (n + 1))
have 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))
Tactic: rw [pow_succ, pow_succ', mulRightLinearMap_mul, Module.End.mul_eq_comp, pow_mulRightLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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))
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) (n + 1) =
    mulRightLinearMap l R (a ^ (n + 1))
have 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)
Tactic: rw [pow_succ, pow_succ', mulRightLinearMap_mul, Module.End.mul_eq_comp, pow_mulRightLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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)
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) (n + 1) =
    mulRightLinearMap l R (a ^ (n + 1))
have 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
Tactic: rw [pow_succ, pow_succ', mulRightLinearMap_mul, Module.End.mul_eq_comp, pow_mulRightLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) (n + 1) =
    mulRightLinearMap l R (a ^ (n + 1))
have 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
Tactic: rw [pow_succ, pow_succ', mulRightLinearMap_mul, Module.End.mul_eq_comp, pow_mulRightLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ HPow.hPow (α := Matrix l m A →ₗ[R] Matrix l m A) (mulRightLinearMap l R a) (n + 1) =
    mulRightLinearMap l R (a ^ (n + 1))
have 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)
Tactic: rw [pow_succ, pow_succ', mulRightLinearMap_mul, Module.End.mul_eq_comp, pow_mulRightLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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) α
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M
have a : ∀ (i : n ⊕ o) (j : l ⊕ m), fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j
have a : ∀ (val : n), fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) j = M (Sum.inl val) j
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j
have a₁ : ∀ (val : o), fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) j = M (Sum.inr val) j
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) j = M (Sum.inl val) j
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val) j = M (Sum.inl val) j
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) j = M (Sum.inr val) j
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val) j = M (Sum.inr val) j
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
h :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
⊢ A = B
have rw : fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ = B
Tactic: rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
h :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
rw : fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ = B
⊢ A = B
have rw₁ : fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
Tactic: rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
h :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
rw : fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ = B
rw₁ :
  fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
⊢ A = B
have rw₂ : fromBlocks B.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
Tactic: rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
h :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
rw : fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ = B
rw₁ :
  fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₂ :
  fromBlocks B.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
⊢ A = B
have rw₃ : fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
Tactic: rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
h :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
rw : fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ = B
rw₁ :
  fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₂ :
  fromBlocks B.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₃ :
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
⊢ A = B
have rw₄ : fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ A.toBlocks₂₂ =
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
Tactic: rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
h :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
rw : fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ = B
rw₁ :
  fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₂ :
  fromBlocks B.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₃ :
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₄ :
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
⊢ A = B
have rw₅ : fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂ =
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
Tactic: rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]