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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
S₁ : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₁_def : S₁ = {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ :
  Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j)) =
    Icc (-↑(chainTopCoeff i j) + -↑(chainBotCoeff i j)) 0
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
hS₂ : S₂ = Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j))
⊢ -↑(chainBotCoeff i (chainTopIdx i j)) ≤ ↑(chainTopCoeff i (chainTopIdx i j))

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
⊢ ↑(chainBotCoeff i j) + ↑(chainTopCoeff i j) = ↑(chainBotCoeff i (chainTopIdx i j))

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
⊢ ↑(chainBotCoeff i (chainTopIdx i j)) = ↑(chainBotCoeff i (chainTopIdx i j)) - ↑(chainTopCoeff i (chainTopIdx i j))

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_3
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
⊢ abv (a⁻¹ - b⁻¹) < ε

Tactic:
have a0 := K0.trans_le ha

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_3
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
⊢ abv (a⁻¹ - b⁻¹) < ε
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
q : ℚ
hq : q > 0
hq' : P.root j = q • P.root i
⊢ ¬(↑q = 0 ∧ -1 = 0)

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k : ι
⊢ ∀ (k_1 : ι),
    P.root k_1 = P.root j + P.root k →
      (∃ n f,
          range f ⊆ ↑b.support ∧
            P.root j = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root) →
        k ∈ b.support →
          ∃ n f,
            range f ⊆ ↑b.support ∧
              P.root k_1 = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root

Tactic:
l

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
⊢ P.root l = P.root j + P.root k →
    (∃ n f,
        range f ⊆ ↑b.support ∧ P.root j = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root) →
      k ∈ b.support →
        ∃ n f,
          range f ⊆ ↑b.support ∧ P.root l = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
⊢ ∃ n f, range f ⊆ ↑b.support ∧ P.root i = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root

Tactic:
apply hi.induction_on_add (fun j hj ↦ ⟨1, ![j], by simpa⟩)
  intro j k l h₁ ⟨n, f, h₂, h₃, h₄⟩ h₅
  refine ⟨n + 1, Fin.snoc f k, ?_, ?_, fun m ↦ ?_⟩
  · simpa using insert_subset h₅ h₂
  · simp [Fin.sum_univ_castSucc, h₁, h₃]
  · by_cases hm : m < n
    · have : m = (⟨m, hm⟩ : Fin n).castSucc := rfl
      rw [this, Fin.sum_Iic_castSucc]
      simp only [Fin.snoc_castSucc, h₄]
    · replace hm : m = n := by lia
      replace hm : Finset.Iic m = Finset.univ := by ext; simp [hm, Fin.le_def, Fin.is_le]
      simp [hm, Fin.sum_univ_castSucc, ← h₃, ← h₁]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
i : ι
⊢ P.root (-i) = -P.root i

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : CauSeq ℚ abs
⊢ mk (-f) = -mk f

Tactic:
by simp [mk, ← ofCauchy_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
aux : ∀ (i : ι), ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)
g : Dual ℚ N := f ∘ₗ ↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm)
hg₀ : ∀ (i : ι), g (P.coroot i) ≠ 0
hg : ∀ (i : ι), 0 < g (P.coroot i) ↔ 0 < f (P.root i)
⊢ P.coroot (-i) = -P.coroot i

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
_i : Module ℚ M := compHom M (algebraMap ℚ R)
f : Dual ℚ M
hf : ∀ (i : ι), f (P.root i) ≠ 0
this : InvolutiveNeg ι := P.indexNeg
i : ι
⊢ P.root (-i) = -P.root i

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
n : ℕ
⊢ ↑f n = ↑(f - const abv 0) n

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b

Tactic:
· refine Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) ?_
    rw [CauSeq.inf_idem]

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : ↑n ≠ -1
⊢ A ^ (↑n + 1) = A ^ ↑n * A

Tactic:
by simp only [pow_succ, ← Nat.cast_succ, zpow_natCast]

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (-[m+1] * -[n+1]) = ((A ^ (m + 1))⁻¹ ^ (n + 1))⁻¹

Tactic:
negSucc_mul_negSucc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (↑m.succ * ↑n.succ) = ((A ^ (m + 1))⁻¹ ^ (n + 1))⁻¹
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
⊢ ∀ (x : n →₀ R), 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * 0 i j * xj

Tactic:
by simp

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᵀ = Aᵀ ^ ↑n

Tactic:
rw [zpow_natCast, zpow_natCast, transpose_pow]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : DecidableEq n
inst✝² : NoZeroDivisors R
inst✝¹ : Nonempty n
inst✝ : Nontrivial R
d : ℕ
⊢ (∀ (i : n), 0 < ↑d) ↔ 0 < d

Tactic:
by simp

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : DecidableEq n
inst✝² : NoZeroDivisors R
inst✝¹ : Nonempty n
inst✝ : Nontrivial R
d : ℤ
⊢ (∀ (i : n), 0 < ↑d) ↔ 0 < d

Tactic:
by simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix m n R
⊢ (B * A * Bᴴ).PosSemidef

Tactic:
by
  simpa only [conjTranspose_conjTranspose] using hA.conjTranspose_mul_mul_same Bᴴ

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
i : ι
⊢ Finsupp.single i 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂), (⁅(x + y).1, z.1⁆, ⁅(x + y).2, z.2⁆) = (⁅x.1, z.1⁆, ⁅x.2, z.2⁆) + (⁅y.1, z.1⁆, ⁅y.2, z.2⁆)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂), (⁅x.1, (y + z).1⁆, ⁅x.2, (y + z).2⁆) = (⁅x.1, y.1⁆, ⁅x.2, y.2⁆) + (⁅x.1, z.1⁆, ⁅x.2, z.2⁆)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ (x : L₁ × L₂), (⁅x.1, x.1⁆, ⁅x.2, x.2⁆) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂),
    (⁅x.1, (⁅y.1, z.1⁆, ⁅y.2, z.2⁆).1⁆, ⁅x.2, (⁅y.1, z.1⁆, ⁅y.2, z.2⁆).2⁆) =
      (⁅(⁅x.1, y.1⁆, ⁅x.2, y.2⁆).1, z.1⁆, ⁅(⁅x.1, y.1⁆, ⁅x.2, y.2⁆).2, z.2⁆) +
        (⁅y.1, (⁅x.1, z.1⁆, ⁅x.2, z.2⁆).1⁆, ⁅y.2, (⁅x.1, z.1⁆, ⁅x.2, z.2⁆).2⁆)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
x✝² : R
x✝¹ x✝ : L₁ × L₂
⊢ ⁅x✝¹, x✝² • x✝⁆ = x✝² • ⁅x✝¹, x✝⁆

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₁ × L₂},
    (LinearMap.fst R L₁ L₂).toFun ⁅x, y⁆ = ⁅(LinearMap.fst R L₁ L₂).toFun x, (LinearMap.fst R L₁ L₂).toFun y⁆

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₁ × L₂},
    (LinearMap.snd R L₁ L₂).toFun ⁅x, y⁆ = ⁅(LinearMap.snd R L₁ L₂).toFun x, (LinearMap.snd R L₁ L₂).toFun y⁆

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₁},
    (LinearMap.inl R L₁ L₂).toFun ⁅x, y⁆ = ⁅(LinearMap.inl R L₁ L₂).toFun x, (LinearMap.inl R L₁ L₂).toFun y⁆

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₂},
    (LinearMap.inr R L₁ L₂).toFun ⁅x, y⁆ = ⁅(LinearMap.inr R L₁ L₂).toFun x, (LinearMap.inr R L₁ L₂).toFun y⁆

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
f : L →ₗ⁅R⁆ L₁
g : L →ₗ⁅R⁆ L₂
⊢ ∀ {x y : L}, ((↑f).prod ↑g).toFun ⁅x, y⁆ = ⁅((↑f).prod ↑g).toFun x, ((↑f).prod ↑g).toFun y⁆

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
x✝ : L₁
⊢ ∀ ⦃a₂ : L₁⦄, (inl R L₁ L₂) x✝ = (inl R L₁ L₂) a₂ → x✝ = a₂

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
x✝ : L₂
⊢ ∀ ⦃a₂ : L₂⦄, (inr R L₁ L₂) x✝ = (inr R L₁ L₂) a₂ → x✝ = a₂

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₁ × L₂},
    (↑(LinearEquiv.prodComm R L₁ L₂)).toFun ⁅x, y⁆ =
      ⁅(↑(LinearEquiv.prodComm R L₁ L₂)).toFun x, (↑(LinearEquiv.prodComm R L₁ L₂)).toFun y⁆

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
x : ↥H
⊢ (((toEnd K (↥H) L) x - (b.baseSupp i) x • 1) ^ 1) (b.e i) = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
χ : ↥root
this : H.IsCartanSubalgebra := isCartanSubalgebra b
n : ι → ℕ
i : ι
x✝ : i ∈ Finset.univ
⊢ b.baseSupp i ∈ ⇑(rootSystem H).root '' range b.baseSupp'

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
d : ↥b.support → ℤ
hd : ∀ (i : ↥b.support), 0 < d i
hdS : (Matrix.diagonal d * b.cartanMatrix).PosDef
⊢ ¬HasEigenvalue (toLin' b.cartanMatrix) 4

Tactic:
have aux (i j : b.support) : b.cartanMatrix i j ≤ if i = j then 2 else 0 := by
    rcases eq_or_ne i j with rfl | hij
    · simp
    · simpa [hij] using cartanMatrix_le_zero_of_ne b i j hij

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
d : ↥b.support → ℤ
hd : ∀ (i : ↥b.support), 0 < d i
hdS : (Matrix.diagonal d * b.cartanMatrix).PosDef
aux : ∀ (i j : ↥b.support), b.cartanMatrix i j ≤ if i = j then 2 else 0
⊢ ¬HasEigenvalue (toLin' b.cartanMatrix) 4
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
h_mem : ⁅b.e i, b.f i⁆ ∈ H
h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩
x✝ : ↥H
z : L
hz : z ∈ H
⊢ (((toEnd K (↥H) L) ⟨z, hz⟩ - (b.baseSupp i) ⟨z, hz⟩ • 1) ^ 1) (b.e i) = 0

Tactic:
by simp

Goal state after: