awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
M : Matrix ((i : o) × m' i) ((i : o) × n' i) α
k : o
i : m' k
j : n' k
⊢ M.blockDiag' (m' := m') (n' := n') k i j =
    M (Sigma.mk (β := fun (i : o) ↦ m' i) k i) (Sigma.mk (β := fun (i : o) ↦ n' i) k j)

Tactic:
rfl

Premises used: Matrix.blockDiag', rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
M : Matrix ((i : o) × m' i) ((i : o) × n' i) α
f : α → β
⊢ (M.map f).blockDiag' (m' := m') (n' := n') = fun (k : o) ↦ (M.blockDiag' (m' := m') (n' := n') k).map f

Tactic:
rfl

Premises used: Matrix.blockDiag', Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
M : Matrix ((i : o) × m' i) ((i : o) × n' i) α
k : o
⊢ Mᵀ.blockDiag' (m' := n') (n' := m') k = (M.blockDiag' (m' := m') (n' := n') k)ᵀ

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_14
inst : Star α
M : Matrix ((i : o) × m' i) ((i : o) × n' i) α
k : o
⊢ Mᴴ.blockDiag' (m' := n') (n' := m') k = (M.blockDiag' (m' := m') (n' := n') k)ᴴ

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : Zero α
⊢ Eq (α := (k : o) → Matrix.{u_7, u_8, u_12} (m' k) (n' k) α) (blockDiag' (m' := m') (n' := n') 0) 0

Tactic:
rfl

Premises used: Matrix.blockDiag', rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
inl :
  (diagonal d).blockDiag' (m' := m') (n' := m') k i i =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
inr :
  ∀ (hij : i ≠ j),
    (diagonal d).blockDiag' (m' := m') (n' := m') k i j =
      diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i j
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i j =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
inl :
  diagonal d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) (Sigma.mk (β := fun (i : o) ↦ m' i) k i) =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
inl₁ :
  d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
inl₂ inl₃ : d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) = d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i i =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i

Tactic:
rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq, Matrix.blockDiag'_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
rw : ∀ (h : Sigma.mk (β := fun (i : o) ↦ m' i) k i = Sigma.mk (β := fun (i : o) ↦ m' i) k j), i = j
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i j =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i j

Tactic:
rw [blockDiag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (fun h => ?_) hij)]

Premises used: mt, Matrix.blockDiag'_apply, Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : Sigma.mk (β := fun (i : o) ↦ m' i) k i = Sigma.mk (β := fun (i : o) ↦ m' i) k j
refl : ∀ (hij : i ≠ i), i = i
⊢ i = j

Tactic:
cases h
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
hij : i ≠ i
⊢ i = i

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
⊢ (blockDiagonal' (m' := m') (n' := n') M).blockDiag' (m' := m') (n' := n') = M

Tactic:
funext fun _ => ext fun _ _ => blockDiagonal'_apply_eq M _ _ _

Premises used: Matrix.blockDiagonal'_apply_eq, funext, Matrix.ext
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
⊢ Function.Injective (α := (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α) (blockDiagonal' (m' := m') (n' := n'))

Tactic:
Function.LeftInverse.injective blockDiag'_blockDiagonal'

Premises used: Function.LeftInverse.injective, Matrix.blockDiag'_blockDiagonal'
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
M N : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
⊢ blockDiagonal' (m' := m') (n' := n') M = blockDiagonal' (m' := m') (n' := n') N ↔ M = N

Tactic:
blockDiagonal'_injective.eq_iff

Premises used: Function.Injective.eq_iff, Matrix.blockDiagonal'_injective
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
inst_3 : One α
⊢ Eq (α := (k : o) → Matrix.{u_7, u_7, u_12} (m' k) (m' k) α) (blockDiag' (m' := m') (n' := m') 1) 1

Tactic:
funext <| blockDiag'_diagonal _

Premises used: Matrix.blockDiag'_diagonal, funext
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : Add α
M N : Matrix ((i : o) × m' i) ((i : o) × n' i) α
⊢ (M + N).blockDiag' (m' := m') (n' := n') = M.blockDiag' (m' := m') (n' := n') + N.blockDiag' (m' := m') (n' := n')

Tactic:
rfl

Premises used: Matrix.blockDiag', rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : AddGroup α
M : Matrix ((i : o) × m' i) ((i : o) × n' i) α
⊢ (-M).blockDiag' (m' := m') (n' := n') = -M.blockDiag' (m' := m') (n' := n')

Tactic:
map_neg (blockDiag'AddMonoidHom m' n' α) M

Premises used: Matrix.blockDiag'AddMonoidHom, map_neg, Matrix.blockDiag'
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : AddGroup α
M N : Matrix ((i : o) × m' i) ((i : o) × n' i) α
⊢ (M - N).blockDiag' (m' := m') (n' := n') = M.blockDiag' (m' := m') (n' := n') - N.blockDiag' (m' := m') (n' := n')

Tactic:
map_sub (blockDiag'AddMonoidHom m' n' α) M N

Premises used: map_sub, Matrix.blockDiag'AddMonoidHom, Matrix.blockDiag'
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
R : Type u_14
inst : SMul R α
x : R
M : Matrix ((i : o) × m' i) ((i : o) × n' i) α
⊢ (x • M).blockDiag' (m' := m') (n' := n') = x • M.blockDiag' (m' := m') (n' := n')

Tactic:
rfl

Premises used: Matrix.blockDiag', rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst_1 : Fintype n
p : m → Prop
q : k → Prop
A : Matrix m n R
B : Matrix n k R
a :
  ∀ (i : { a : m // p a }) (k_1 : { a : k // q a }),
    (A * B).toBlock p q i k_1 =
      HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ⊤ a } R) (β :=
        Matrix.{u_15, u_16, u_10} { a : n // ⊤ a } { a : k // q a } R) (A.toBlock p ⊤) (B.toBlock ⊤ q) i k_1
⊢ (A * B).toBlock p q =
    HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ⊤ a } R) (β :=
      Matrix.{u_15, u_16, u_10} { a : n // ⊤ a } { a : k // q a } R) (A.toBlock p ⊤) (B.toBlock ⊤ q)

Tactic:
ext i k
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // q a }
a :
  Eq.{u_10 + 1} (α := R) (∑ j : n, A (↑i : m) j * B j (↑k : k_1))
    (∑ x : { a : n // ⊤ a }, A (↑i : m) (↑x : n) * B (↑x : n) (↑k : k_1))
⊢ (A * B).toBlock p q i k =
    HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ⊤ a } R) (β :=
      Matrix.{u_15, u_16, u_10} { a : n // ⊤ a } { a : k_1 // q a } R) (A.toBlock p ⊤) (B.toBlock ⊤ q) i k

Tactic:
simp only [toBlock_apply, mul_apply]

Premises used: Matrix.mul_apply, Matrix.toBlock_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // q a }
a : ∀ (x : n), Membership.mem (γ := Finset n) Finset.univ x ↔ ⊤ x
⊢ Eq.{u_10 + 1} (α := R) (∑ j : n, A (↑i : m) j * B j (↑k : k_1))
    (∑ x : { a : n // ⊤ a }, A (↑i : m) (↑x : n) * B (↑x : n) (↑k : k_1))

Tactic:
rw [Finset.sum_subtype]

Premises used: Finset.sum_subtype
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // q a }
⊢ ∀ (x : n), Membership.mem (γ := Finset n) Finset.univ x ↔ ⊤ x

Tactic:
simp [Pi.top_apply, Prop.top_eq_true]

Premises used: Pi.top_apply, Prop.top_eq_true
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
a :
  ∀ (i : { a : m // p a }) (k_1 : { a : k // r a }),
    (A * B).toBlock p r i k_1 =
      (A.toBlock p q * B.toBlock q r +
          HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
            Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
            (B.toBlock (fun (i : n) ↦ ¬q i) r))
        i k_1
⊢ (A * B).toBlock p r =
    A.toBlock p q * B.toBlock q r +
      HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
        Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
        (B.toBlock (fun (i : n) ↦ ¬q i) r)

Tactic:
ext i k
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // r a }
a :
  ∑ j : n, A (↑i : m) j * B j (↑k : k_1) =
    (A.toBlock p q * B.toBlock q r +
        HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
          Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k_1 // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
          (B.toBlock (fun (i : n) ↦ ¬q i) r))
      i k
⊢ (A * B).toBlock p r i k =
    (A.toBlock p q * B.toBlock q r +
        HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
          Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k_1 // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
          (B.toBlock (fun (i : n) ↦ ¬q i) r))
      i k

Tactic:
simp only [toBlock_apply, mul_apply]

Premises used: Matrix.mul_apply, Matrix.toBlock_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // r a }
⊢ ∑ j : n, A (↑i : m) j * B j (↑k : k_1) =
    (A.toBlock p q * B.toBlock q r +
        HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
          Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k_1 // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
          (B.toBlock (fun (i : n) ↦ ¬q i) r))
      i k

Tactic:
(Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm

Premises used: Multiset.sum, Multiset.foldr, Matrix.submatrix, HMul.hMul, dotProduct, Matrix.toBlock, Eq.symm, Subtype.val, Fintype.sum_subtype_add_sum_subtype, Finset.sum, Multiset.filter
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // r a }
⊢ ∑ j : n, A (↑i : m) j * B j (↑k : k_1) =
    (A.toBlock p q * B.toBlock q r +
        HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
          Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k_1 // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
          (B.toBlock (fun (i : n) ↦ ¬q i) r))
      i k

Tactic:
exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm

Premises used: HMul.hMul, Eq.symm, Subtype.val, Fintype.sum_subtype_add_sum_subtype
-- Module: Mathlib.Data.Matrix.Block
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
a :
  ∀ (i : { a : m // p a }) (k_1 : { a : k // r a }),
    (A * B).toBlock p r i k_1 =
      (A.toBlock p q * B.toBlock q r +
          HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
            Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
            (B.toBlock (fun (i : n) ↦ ¬q i) r))
        i k_1
a₁ :
  ∀ (i : { a : m // p a }) (k_1 : { a : k // r a }),
    ∑ j : n, A (↑i : m) j * B j (↑k_1 : k) =
      (A.toBlock p q * B.toBlock q r +
          HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
            Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
            (B.toBlock (fun (i : n) ↦ ¬q i) r))
        i k_1
⊢ (A * B).toBlock p r =
    A.toBlock p q * B.toBlock q r +
      HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
        Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
        (B.toBlock (fun (i : n) ↦ ¬q i) r)

Tactic:
classical
    ext i k
    simp only [toBlock_apply, mul_apply]
    exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm

Premises used: Matrix.mul_apply, Matrix.toBlock_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
α : Type u_15
β : Type u_16
f : α → β
M : Matrix m m α
ι : Type u_18
b : m → ι
i : ι
⊢ (M.map f).toSquareBlock b i = (M.toSquareBlock b i).map f

Tactic:
submatrix_map _ _ _ _

Premises used: Matrix.toBlock, Matrix.submatrix_map, Matrix.toSquareBlockProp, Matrix.toSquareBlock
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
R : Type u_14
α : Type u_15
b : m → α
M : Matrix m m (Matrix n n R)
a : α
⊢ Eq (α := Matrix { a_1 : m × n // b a_1.1 = a } { a_1 : m × n // b a_1.1 = a } R)
    (toSquareBlock ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R) M)
      (fun (i : m × n) ↦ b i.1) a)
    ((reindex (Equiv.symm (Equiv.prodSubtypeFstEquivSubtypeProd.{u_3, u_2} (β := n) (p := fun (a_1 : m) ↦ b a_1 = a)))
          (Equiv.symm (Equiv.prodSubtypeFstEquivSubtypeProd.{u_3, u_2} (β := n) (p := fun (a_1 : m) ↦ b a_1 = a))) :
        (a_1 : Matrix ({ a_1 : m // b a_1 = a } × n) ({ a_1 : m // b a_1 = a } × n) R) →
          Matrix { s : m × n // b s.1 = a } { s : m × n // b s.1 = a } R)
      ((comp { a_1 : m // b a_1 = a } { a_1 : m // b a_1 = a } n n R :
          (a_1 : Matrix { a_1 : m // b a_1 = a } { a_1 : m // b a_1 = a } (Matrix n n R)) →
            Matrix ({ a_2 : m // b a_2 = a } × n) ({ a_2 : m // b a_2 = a } × n) R)
        (M.toSquareBlock b a)))

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.toBlock, Matrix.toSquareBlockProp, rfl, Matrix.toSquareBlock
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
R : Type u_14
inst : Zero R
inst_1 : DecidableEq m
d : m → Matrix n n R
a :
  ∀ (i j : m × n),
    Eq.{u_14 + 1} (α := R)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R) (diagonal d) i j : R)
      ((reindex (Equiv.prodComm n m) (Equiv.prodComm n m) : (a : Matrix (n × m) (n × m) R) → Matrix (m × n) (m × n) R)
          (blockDiagonal d) i j :
        R)
⊢ Eq (α := Matrix (m × n) (m × n) R)
    ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R) (diagonal d) :
      Matrix (m × n) (m × n) R)
    ((reindex (Equiv.prodComm n m) (Equiv.prodComm n m) : (a : Matrix (n × m) (n × m) R) → Matrix (m × n) (m × n) R)
        (blockDiagonal d) :
      Matrix (m × n) (m × n) R)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
R : Type u_14
inst : Zero R
inst_1 : DecidableEq m
d : m → Matrix n n R
i j : m × n
⊢ Eq.{u_14 + 1} (α := R)
    ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R) (diagonal d) i j : R)
    ((reindex (Equiv.prodComm n m) (Equiv.prodComm n m) : (a : Matrix (n × m) (n × m) R) → Matrix (m × n) (m × n) R)
        (blockDiagonal d) i j :
      R)

Tactic:
simp [diagonal, blockDiagonal, Matrix.ite_apply]

Premises used: Matrix.blockDiagonal, Matrix.ite_apply, Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
h : ∀ (x : Fin n), (A n).diag x = 2 x
⊢ (A n).diag = 2

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
x : Fin n
⊢ (A n).diag x = 2 x

Tactic:
simp [A]

Premises used: CartanMatrix.A
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i : Fin n
⊢ B n i i = 2

Tactic:
simp [B, Matrix.of_apply]

Premises used: Matrix.of_apply, CartanMatrix.B
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i : Fin n
⊢ C n i i = 2

Tactic:
simp [C, Matrix.of_apply]

Premises used: CartanMatrix.C, Matrix.of_apply
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i : Fin n
⊢ D n i i = 2

Tactic:
simp [D, Matrix.of_apply]

Premises used: Matrix.of_apply, CartanMatrix.D
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
simp : LE.le (α := ℤ) (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0) 0
⊢ A n i j ≤ 0

Tactic:
simp only [A, Matrix.of_apply]

Premises used: CartanMatrix.A, Matrix.of_apply
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) (-1) 0
neg : ¬i = j → ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ)) → LE.le (α := ℤ) 0 0
⊢ LE.le (α := ℤ) (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0) 0

Tactic:
split_ifs
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : i = j
⊢ LE.le (α := ℤ) 2 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ)
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ))
⊢ LE.le (α := ℤ) 0 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
simp :
  LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then if (↑j : ℕ) = n - 1 then -2 else -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
    0
⊢ B n i j ≤ 0

Tactic:
simp only [B, Matrix.of_apply]

Premises used: Matrix.of_apply, CartanMatrix.B
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
neg : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → ¬(↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-1) 0
pos₂ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) (-1) 0
neg₁ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → ¬(↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) 0 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then if (↑j : ℕ) = n - 1 then -2 else -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
    0

Tactic:
split_ifs
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : (↑i : ℕ) + 1 = (↑j : ℕ)
h_3 : (↑j : ℕ) = n - 1
⊢ LE.le (α := ℤ) (-2) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : (↑i : ℕ) + 1 = (↑j : ℕ)
h_3 : ¬(↑j : ℕ) = n - 1
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬(↑i : ℕ) + 1 = (↑j : ℕ)
h_3 : (↑j : ℕ) + 1 = (↑i : ℕ)
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬(↑i : ℕ) + 1 = (↑j : ℕ)
h_3 : ¬(↑j : ℕ) + 1 = (↑i : ℕ)
⊢ LE.le (α := ℤ) 0 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
simp :
  LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
    0
⊢ C n i j ≤ 0

Tactic:
simp only [C, Matrix.of_apply]

Premises used: CartanMatrix.C, Matrix.of_apply
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → LE.le (α := ℤ) (-1) 0
pos₂ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → (↑i : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
neg : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → ¬(↑i : ℕ) = n - 1 → LE.le (α := ℤ) (-1) 0
neg₁ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → ¬(↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) 0 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
    0

Tactic:
split_ifs
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : (↑i : ℕ) + 1 = (↑j : ℕ)
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬(↑i : ℕ) + 1 = (↑j : ℕ)
h_3 : (↑j : ℕ) + 1 = (↑i : ℕ)
h_4 : (↑i : ℕ) = n - 1
⊢ LE.le (α := ℤ) (-2) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬(↑i : ℕ) + 1 = (↑j : ℕ)
h_3 : (↑j : ℕ) + 1 = (↑i : ℕ)
h_4 : ¬(↑i : ℕ) = n - 1
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
simp :
  LE.le (α := ℤ)
    (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
          else
            if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
            else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
    0
⊢ D n i j ≤ 0

Tactic:
simp only [D, Matrix.of_apply]

Premises used: Matrix.of_apply, CartanMatrix.D