awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨0, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨0, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨0, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
i j : Fin 2
h : i ≠ j
0 : ∀ (h : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j), G₂ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j ≤ 0
1 : ∀ (h : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j), G₂ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j ≤ 0
⊢ G₂ i j ≤ 0

Tactic:
fin_cases i
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
j : Fin 2
h : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
0 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    G₂ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ≤ 0
h_1 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    G₂ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ≤ 0
⊢ G₂ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j ≤ 0

Tactic:
fin_cases j
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
j : Fin 2
h : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    G₂ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ≤ 0
h_1 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    G₂ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ≤ 0
⊢ G₂ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j ≤ 0

Tactic:
fin_cases j
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ G₂ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ≤ 0

Tactic:
simp_all [G₂]

Premises used: CartanMatrix.G₂
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ G₂ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ≤ 0

Tactic:
simp_all [G₂]

Premises used: CartanMatrix.G₂
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ G₂ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ≤ 0

Tactic:
simp_all [G₂]

Premises used: CartanMatrix.G₂
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ G₂ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ≤ 0

Tactic:
simp_all [G₂]

Premises used: CartanMatrix.G₂
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₆ᵀ = E₆

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇ᵀ = E₇

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ᵀ = E₈

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₆.IsSymm

Tactic:
E₆_transpose

Premises used: CartanMatrix.E₆_transpose, Matrix.IsSymm
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇.IsSymm

Tactic:
E₇_transpose

Premises used: Matrix.IsSymm, CartanMatrix.E₇_transpose
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈.IsSymm

Tactic:
E₈_transpose

Premises used: Matrix.IsSymm, CartanMatrix.E₈_transpose
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ G₂.det = 1

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ F₄.det = 1

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
inst : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
mp : A.IsSimplyLaced → ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
mpr : (∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1) → A.IsSimplyLaced
⊢ A.IsSimplyLaced ↔ ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1

Tactic:
constructor
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
inst : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : A.IsSimplyLaced
i j : ι
hij : j < i
⊢ A i j = 0 ∨ A i j = -1

Tactic:
h hij.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
inst : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : A.IsSimplyLaced
i j : ι
hij : j < i
⊢ A i j = 0 ∨ A i j = -1

Tactic:
exact h hij.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
inst : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij : i ≠ j
mpr : ∀ (hij : i < j), A i j = 0 ∨ A i j = -1
mpr₁ : ∀ (hij : j < i), A i j = 0 ∨ A i j = -1
⊢ A i j = 0 ∨ A i j = -1

Tactic:
obtain hij | hij := hij.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
inst : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij_1 : i ≠ j
hij : i < j
⊢ A i j = 0 ∨ A i j = -1

Tactic:
simpa only [hA.apply i j] using h hij

Premises used: Matrix.IsSymm.apply
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
inst : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij_1 : i ≠ j
hij : j < i
⊢ A i j = 0 ∨ A i j = -1

Tactic:
h hij
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
inst : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij_1 : i ≠ j
hij : j < i
⊢ A i j = 0 ∨ A i j = -1

Tactic:
exact h hij
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
A : Matrix ι ι ℤ
rw : (∀ (b a : ι), a ≠ b → Aᵀ a b = 0 ∨ Aᵀ a b = -1) ↔ ∀ ⦃i j : ι⦄, i ≠ j → A i j = 0 ∨ A i j = -1
⊢ Aᵀ.IsSimplyLaced ↔ A.IsSimplyLaced

Tactic:
rw [IsSimplyLaced, IsSimplyLaced, Pairwise, Pairwise, forall_comm]

Premises used: forall_comm, Matrix.IsSimplyLaced, Pairwise
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
ι : Type u_1
A : Matrix ι ι ℤ
⊢ (∀ (b a : ι), a ≠ b → Aᵀ a b = 0 ∨ Aᵀ a b = -1) ↔ ∀ ⦃i j : ι⦄, i ≠ j → A i j = 0 ∨ A i j = -1

Tactic:
aesop
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
simp :
  Eq (α := ℤ) (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0) 0 ∨
    Eq (α := ℤ) (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0) (-1)
⊢ A n i j = 0 ∨ A n i j = -1

Tactic:
simp only [A, of_apply]

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

Tactic:
grind
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
simp :
  Eq (α := ℤ)
      (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 ∨
    Eq (α := ℤ)
      (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)
      (-1)
⊢ D n i j = 0 ∨ D n i j = -1

Tactic:
simp only [D, of_apply]

Premises used: Matrix.of_apply, CartanMatrix.D
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ Eq (α := ℤ)
      (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 ∨
    Eq (α := ℤ)
      (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)
      (-1)

Tactic:
grind
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
rw : ∀ ⦃i j : Fin 6⦄, j < i → E₆ i j = 0 ∨ E₆ i j = -1
⊢ E₆.IsSimplyLaced

Tactic:
rw [Matrix.isSimplyLaced_iff_of_linearOrder E₆ E₆_isSymm]

Premises used: CartanMatrix.E₆, Matrix.isSimplyLaced_iff_of_linearOrder, CartanMatrix.E₆_isSymm
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ ∀ ⦃i j : Fin 6⦄, j < i → E₆ i j = 0 ∨ E₆ i j = -1

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
rw : ∀ ⦃i j : Fin 7⦄, j < i → E₇ i j = 0 ∨ E₇ i j = -1
⊢ E₇.IsSimplyLaced

Tactic:
rw [Matrix.isSimplyLaced_iff_of_linearOrder E₇ E₇_isSymm]

Premises used: CartanMatrix.E₇, CartanMatrix.E₇_isSymm, Matrix.isSimplyLaced_iff_of_linearOrder
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ ∀ ⦃i j : Fin 7⦄, j < i → E₇ i j = 0 ∨ E₇ i j = -1

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
rw : ∀ ⦃i j : Fin 8⦄, j < i → E₈ i j = 0 ∨ E₈ i j = -1
⊢ E₈.IsSimplyLaced

Tactic:
rw [Matrix.isSimplyLaced_iff_of_linearOrder E₈ E₈_isSymm]

Premises used: CartanMatrix.E₈, CartanMatrix.E₈_isSymm, Matrix.isSimplyLaced_iff_of_linearOrder
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ ∀ ⦃i j : Fin 8⦄, j < i → E₈ i j = 0 ∨ E₈ i j = -1

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ ¬F₄.IsSimplyLaced

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ ¬G₂.IsSimplyLaced

Tactic:
decide
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₁
j : n
⊢ A₁.fromRows A₂ (Sum.inl i) j = A₁ i j

Tactic:
rfl

Premises used: Matrix.fromRows, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₂
j : n
⊢ A₁.fromRows A₂ (Sum.inr i) j = A₂ i j

Tactic:
rfl

Premises used: Matrix.fromRows, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : m
j : n₁
⊢ A₁.fromCols A₂ i (Sum.inl j) = A₁ i j

Tactic:
rfl

Premises used: Matrix.fromCols, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : m
j : n₂
⊢ A₁.fromCols A₂ i (Sum.inr j) = A₂ i j

Tactic:
rfl

Premises used: Matrix.fromCols, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₁
j : n
⊢ A.toRows₁ i j = A (Sum.inl i) j

Tactic:
rfl

Premises used: Matrix.toRows₁, rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₂
j : n
⊢ A.toRows₂ i j = A (Sum.inr i) j

Tactic:
rfl

Premises used: Matrix.toRows₂, rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (A₁.fromRows A₂).toRows₁ = A₁

Tactic:
rfl

Premises used: Matrix.fromRows, Matrix.toRows₁, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (A₁.fromRows A₂).toRows₂ = A₂

Tactic:
rfl

Premises used: Matrix.toRows₂, Matrix.fromRows, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₁
⊢ A.toCols₁ i j = A i (Sum.inl j)

Tactic:
rfl

Premises used: rfl, Matrix.toCols₁
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₂
⊢ A.toCols₂ i j = A i (Sum.inr j)

Tactic:
rfl

Premises used: Matrix.toCols₂, rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂).toCols₁ = A₁

Tactic:
rfl

Premises used: Matrix.fromCols, rfl, Sum.elim, Matrix.toCols₁
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂).toCols₂ = A₂

Tactic:
rfl

Premises used: Matrix.fromCols, Matrix.toCols₂, rfl, Sum.elim
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
a : ∀ (i : m) (j : n₁), A.toCols₁.fromCols A.toCols₂ i (Sum.inl j) = A i (Sum.inl j)
a₁ : ∀ (i : m) (j : n₂), A.toCols₁.fromCols A.toCols₂ i (Sum.inr j) = A i (Sum.inr j)
⊢ A.toCols₁.fromCols A.toCols₂ = A

Tactic:
ext i (j | j)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₁
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inl j) = A i (Sum.inl j)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₂
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inr j) = A i (Sum.inr j)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
a : ∀ (i : m₁) (j : n), A.toRows₁.fromRows A.toRows₂ (Sum.inl i) j = A (Sum.inl i) j
a₁ : ∀ (i : m₂) (j : n), A.toRows₁.fromRows A.toRows₂ (Sum.inr i) j = A (Sum.inr i) j
⊢ A.toRows₁.fromRows A.toRows₂ = A

Tactic:
ext (i | i) j
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₁
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inl i) j = A (Sum.inl i) j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₂
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inr i) j = A (Sum.inr i) j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
x1 x2 : Matrix m₁ n R
y1 y2 : Matrix m₂ n R
⊢ x1.fromRows y1 = x2.fromRows y2 → x1 = x2 ∧ y1 = y2

Tactic:
simp [← Matrix.ext_iff]

Premises used: Matrix.ext_iff
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
simp :
  (∀ (i : m) (j : n₁ ⊕ n₂), x1.fromCols y1 i j = x2.fromCols y2 i j) →
    (∀ (i : m) (j : n₁), x1 i j = x2 i j) ∧ ∀ (i : m) (j : n₂), y1 i j = y2 i j
⊢ x1.fromCols y1 = x2.fromCols y2 → x1 = x2 ∧ y1 = y2

Tactic:
simp only [← Matrix.ext_iff]

Premises used: Matrix.ext_iff
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ (∀ (i : m) (j : n₁ ⊕ n₂), x1.fromCols y1 i j = x2.fromCols y2 i j) →
    (∀ (i : m) (j : n₁), x1 i j = x2 i j) ∧ ∀ (i : m) (j : n₂), y1 i j = y2 i j

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
⊢ A₁.fromCols A₂ = B₁.fromCols B₂ ↔ A₁ = B₁ ∧ A₂ = B₂

Tactic:
fromCols_inj.eq_iff

Premises used: Matrix.fromCols_inj, Function.Injective2.eq_iff
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
⊢ A₁.fromRows A₂ = B₁.fromRows B₂ ↔ A₁ = B₁ ∧ A₂ = B₂

Tactic:
fromRows_inj.eq_iff

Premises used: Function.Injective2.eq_iff, Matrix.fromRows_inj
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
a : ∀ (i : n₁) (j : m), (A₁.fromCols A₂)ᵀ (Sum.inl i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inl i) j
a₁ : ∀ (i : n₂) (j : m), (A₁.fromCols A₂)ᵀ (Sum.inr i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inr i) j
⊢ (A₁.fromCols A₂)ᵀ = A₁ᵀ.fromRows A₂ᵀ

Tactic:
ext (i | i) j
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₁
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inl i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inl i) j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₂
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inr i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inr i) j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
a : ∀ (i : n) (j : m₁), (A₁.fromRows A₂)ᵀ i (Sum.inl j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inl j)
a₁ : ∀ (i : n) (j : m₂), (A₁.fromRows A₂)ᵀ i (Sum.inr j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inr j)
⊢ (A₁.fromRows A₂)ᵀ = A₁ᵀ.fromCols A₂ᵀ

Tactic:
ext i (j | j)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₁
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inl j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inl j)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₂
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inr j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inr j)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
a : ∀ (val : m₁) (j : n), (A₁.fromRows A₂).map f (Sum.inl val) j = (A₁.map f).fromRows (A₂.map f) (Sum.inl val) j
a₁ : ∀ (val : m₂) (j : n), (A₁.fromRows A₂).map f (Sum.inr val) j = (A₁.map f).fromRows (A₂.map f) (Sum.inr val) j
⊢ (A₁.fromRows A₂).map f = (A₁.map f).fromRows (A₂.map f)

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val : m₁
j : n
⊢ (A₁.fromRows A₂).map f (Sum.inl val) j = (A₁.map f).fromRows (A₂.map f) (Sum.inl val) j

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val : m₂
j : n
⊢ (A₁.fromRows A₂).map f (Sum.inr val) j = (A₁.map f).fromRows (A₂.map f) (Sum.inr val) j

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
a : ∀ (i : m) (val : n₁), (A₁.fromCols A₂).map f i (Sum.inl val) = (A₁.map f).fromCols (A₂.map f) i (Sum.inl val)
a₁ : ∀ (i : m) (val : n₂), (A₁.fromCols A₂).map f i (Sum.inr val) = (A₁.map f).fromCols (A₂.map f) i (Sum.inr val)
⊢ (A₁.fromCols A₂).map f = (A₁.map f).fromCols (A₂.map f)

Tactic:
ext _ (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
i : m
val : n₁
⊢ (A₁.fromCols A₂).map f i (Sum.inl val) = (A₁.map f).fromCols (A₂.map f) i (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
i : m
val : n₂
⊢ (A₁.fromCols A₂).map f i (Sum.inr val) = (A₁.map f).fromCols (A₂.map f) i (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
a : ∀ (i : m₁) (j : n), (-A₁.fromRows A₂) (Sum.inl i) j = (-A₁).fromRows (-A₂) (Sum.inl i) j
a₁ : ∀ (i : m₂) (j : n), (-A₁.fromRows A₂) (Sum.inr i) j = (-A₁).fromRows (-A₂) (Sum.inr i) j
⊢ -A₁.fromRows A₂ = (-A₁).fromRows (-A₂)

Tactic:
ext (i | i) j
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₁
j : n
⊢ (-A₁.fromRows A₂) (Sum.inl i) j = (-A₁).fromRows (-A₂) (Sum.inl i) j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₂
j : n
⊢ (-A₁.fromRows A₂) (Sum.inr i) j = (-A₁).fromRows (-A₂) (Sum.inr i) j

Tactic:
simp