mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
hker : ∀ (x : l → k), A' *ᵥ x = 0 → C' *ᵥ x = 0 → x = 0
Y : Matrix l l k
hY_symm : Y.IsSymm
hY_det : IsUnit (A' + Y * C')
X : Matrix l l R
hX_symm : X.IsSymm
hXY : X.map ⇑f = Y
⊢ (IsLocalRing.residue R) (A + X * C).det ≠ 0

Tactic:
rw [RingHom.map_det, map_add, map_mul, RingHom.mapMatrix_apply _ X, hXY]

Goal state after:
l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
hker : ∀ (x : l → k), A' *ᵥ x = 0 → C' *ᵥ x = 0 → x = 0
Y : Matrix l l k
hY_symm : Y.IsSymm
hY_det : IsUnit (A' + Y * C')
X : Matrix l l R
hX_symm : X.IsSymm
hXY : X.map ⇑f = Y
⊢ ((IsLocalRing.residue R).mapMatrix A + Y * (IsLocalRing.residue R).mapMatrix C).det ≠ 0
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
⊢ (fun F ↦ ⇑F ∘ of R)
      ((fun f ↦ { toFun := fun c ↦ Quot.liftOn c ⇑(liftAux R f) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }) f) =
    f

Tactic:
by
    ext x
    simp only [liftAux, of, LieHom.coe_mk, Function.comp_apply, lib.lift_of_apply]

Goal state after:
Module: Mathlib.Algebra.Lie.Graded

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : (decompose ℒ).symm b ∈ ℒ k
⊢ b ∈ (lof R ι (fun x ↦ ↥(ℒ x)) k).range

Tactic:
use ⟨(decompose ℒ).symm b, hb⟩
          simp [lof_eq_of, ← decompose_of_mem]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn✝ : 2 ≤ l.length
x : { x // x ∈ l }
hn : 2 ≤ l.attach.length
⊢ l.attach.Nodup

Tactic:
← nodup_attach

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn✝ : 2 ≤ l.length
x : { x // x ∈ l }
hn : 2 ≤ l.attach.length
⊢ l.attach.Nodup
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.attach.length
⊢ l.attach.formPerm.cycleType = {l.length}

Tactic:
← nodup_attach

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ l.attach.formPerm.cycleType = {l.length}
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ↑(map (Finset.card ∘ support) [l.attach.formPerm]) = {l.length}

Tactic:
simp only [map, Function.comp_apply]
    rw [support_formPerm_of_nodup _ hl, card_toFinset, dedup_eq_self.mpr hl]
    · simp
    · intro x h
      simp [h] at hn

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
key : Finset.univ.val = x ::ₘ Finset.univ.val.erase x
⊢ f.toCycle hf = ↑(f.toList x)

Tactic:
toCycle,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
key : Finset.univ.val = x ::ₘ Finset.univ.val.erase x
⊢ Finset.univ.val.recOn (Quot.mk ⇑(IsRotated.setoid α) []) (fun x x_1 l ↦ if f x = x then l else ↑(f.toList x)) ⋯ =
    ↑(f.toList x)
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case pos
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
⊢ b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x

pp: case neg
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x

Tactic:
· suffices b • Φ ⁅x, z⁆ y = c • Φ ⁅x, y⁆ z + a • Φ ⁅y, z⁆ x by
        simpa only [show a + b = -c by grind, show a + c = -b by grind, show b + c = -a by grind,
          Finsupp.single_eq_same]
      rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]

Goal state after:
case neg
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : LieRing L
inst✝¹⁰ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁹ : LieRingModule L A
inst✝⁸ : LieRinehartRing A L
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R A
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRinehartAlgebra R A L
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L M
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
coe_bracket_of_module,

Goal state after:
A : Type u_1
L : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : LieRing L
inst✝¹⁰ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁹ : LieRingModule L A
inst✝⁸ : LieRinehartRing A L
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R A
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRinehartAlgebra R A L
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L M
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅↑(t • x), m⁆ = t • ⁅x, m⁆
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ I.rootSpan ∈ (rootSystem H).invtRootSubmodule

Tactic:
by
  rw [RootPairing.mem_invtRootSubmodule_iff]
  intro β
  rw [Module.End.mem_invtSubmodule, rootSpan, Submodule.span_le]
  rintro - ⟨α, hα, rfl⟩
  rw [SetLike.mem_coe, Submodule.mem_comap, LinearEquiv.coe_coe, ← RootPairing.root_reflectionPerm]
  exact Submodule.subset_span ⟨_, (I.reflectionPerm_mem_rootSet_iff α β).mpr hα, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ p ^ ↑1 = p

Tactic:
rw [Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt, pow_one]

Goal state after:
case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ 1 < n + 1
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∀ {a b : R},
    a ∈ {x | (algebraMap R P) x ∈ J} → b ∈ {x | (algebraMap R P) x ∈ J} → a + b ∈ {x | (algebraMap R P) x ∈ J}

Tactic:
intro a b ha hb
      rw [mem_ofPred, map_add]
      exact J.val.add_mem ha hb

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
⊢ ↑(d ⟨p, ⋯⟩) ^ s ≤ n

Tactic:
by_cases hs : s = 0
  · simp [← Associates.bot_eq_one, hs]
  suffices (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ^ s =
      (d ⟨p ^ s, hs'⟩) by
    rw [this]
    apply Subtype.prop (d ⟨p ^ s, hs'⟩)
  obtain ⟨c₁, rfl, hc₁', hc₁''⟩ := exists_chain_of_prime_pow hs (prime_of_normalized_factor p hp)
  let c₂ : Fin (s + 1) → Associates N := fun t => d ⟨c₁ t, le_trans (hc₁''.2 ⟨t, by simp⟩) hs'⟩
  have c₂_def : ∀ t, c₂ t = d ⟨c₁ t, _⟩ := fun t => rfl
  rw [← c₂_def]
  refine (eq_pow_second_of_chain_of_has_chain hs (fun t u h => ?_)
    (@fun r => ⟨@fun hr => ?_, ?_⟩) ?_).symm
  · rw [c₂_def, c₂_def, Subtype.coe_lt_coe, d.lt_iff_lt, Subtype.mk_lt_mk, hc₁'.lt_iff_lt]
    exact h
  · have : r ≤ n := hr.trans (d ⟨c₁ 1 ^ s, _⟩).2
    suffices d.symm ⟨r, this⟩ ≤ ⟨c₁ 1 ^ s, hs'⟩ by
      obtain ⟨i, hi⟩ := hc₁''.1 this
      use i
      simp only [c₂_def, ← hi, d.apply_symm_apply, Subtype.coe_eta, Subtype.coe_mk]
    conv_rhs => rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]
    rw [d.symm.le_iff_le]
    simpa only [← Subtype.coe_le_coe, Subtype.coe_mk] using hr
  · rintro ⟨i, hr⟩
    rw [hr, c₂_def, Subtype.coe_le_coe, d.le_iff_le]
    simpa [Subtype.mk_le_mk] using hc₁''.2 ⟨i, rfl⟩
  exact ne_zero_of_dvd_ne_zero hn (Subtype.prop (d ⟨c₁ 1 ^ s, _⟩))

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«0»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«1»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«2»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«3»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«4»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«5»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«6»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«7»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«0»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«2»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«3»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«4»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«5»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«6»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«7»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«0»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«1»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«2»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«3»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«4»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«5»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«6»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«7»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«0»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«1»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«2»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«3»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«4»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«5»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«6»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«7»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4».«0»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4».«1»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4».«2»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4».«3»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4».«4»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4».«5»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4».«6»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4».«7»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5».«0»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5».«1»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5».«2»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5».«3»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5».«4»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5».«5»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5».«6»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5».«7»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6».«0»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6».«1»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6».«2»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6».«3»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6».«4»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6».«5»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6».«6»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6».«7»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «7».«0»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «7».«1»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «7».«2»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «7».«3»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «7».«4»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «7».«5»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₈]

Goal state after: