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

Goal state before:
pp: case pred
ι : 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
inst✝ : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + -↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hk : P.root k = P.root i + (-↑w - 1) • P.root j
hij : LinearIndependent R ![P.root j, P.root i]
l : ι
hl : P.root l = P.root i + -↑w • P.root j
⊢ b.IsPos k

Tactic:
replace hk : P.root k = P.root l - P.root j := by rw [hk, hl]; module

Goal state after:
case pred
ι : 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
inst✝ : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + -↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hij : LinearIndependent R ![P.root j, P.root i]
l : ι
hl : P.root l = P.root i + -↑w • P.root j
hk : P.root k = P.root l - P.root j
⊢ b.IsPos k
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:
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
⊢ ∀ (i j k : ι),
    P.root k = P.root i + P.root j →
      (∃ 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) →
        j ∈ b.support →
          ∃ n f,
            range f ⊆ ↑b.support ∧ P.root k = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root

Tactic:
intro j

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 : ι
⊢ ∀ (j_1 k : ι),
    P.root k = P.root j + P.root j_1 →
      (∃ 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) →
        j_1 ∈ b.support →
          ∃ n f,
            range f ⊆ ↑b.support ∧ P.root k = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
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:
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
x y : β
h : ofRat x = ofRat y
⊢ x = y

Tactic:
simpa [ofRat, mk_eq, ← const_sub, const_limZero, sub_eq_zero] using h

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ h - f = g - f + -(g - h)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ h - f = g - f + (h - g)

Tactic:
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
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:
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:
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:
simp

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

Goal state before:
pp: case inl
b : ℕ
ha : 0 ≤ 0
⊢ 0 * ↑b + 1 ≤ (0 + 1) ^ b

Tactic:
simp

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

Goal state before:
pp: case inr.zero
a : ℝ
ha' : 0 < a
⊢ a * ↑0 + 1 ≤ (a + 1) ^ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
inst✝ : MulOneClass α
A : Matrix m n α
i✝ : m
j✝ : n
⊢ (A ⊙ of 1) i✝ j✝ = A i✝ j✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
inst✝ : MulOneClass α
A : Matrix m n α
i✝ : m
j✝ : n
⊢ (of 1 ⊙ A) i✝ j✝ = A i✝ j✝

Tactic:
simp

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A⁻¹ ^ 0 = (A ^ 0)⁻¹

Tactic:
simp

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m : ℕ
⊢ A⁻¹ ^ m * A ^ 0 = A ^ 0 * A⁻¹ ^ m

Tactic:
simp

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

Goal state before:
pp: case succ.zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
⊢ A⁻¹ ^ 0 * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ 0

Tactic:
simp

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

Goal state before:
pp: case e'_1.e'_4.e'_8
α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ B = Bᴴᴴ

Tactic:
simp

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

Goal state before:
pp: case e'_2
α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ B = Bᴴᴴ

Tactic:
simp

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A ^ (-↑0) = (A ^ 0)⁻¹

Tactic:
simp

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ IsUnit (A ^ 0).det ↔ IsUnit A.det ∨ 0 = 0

Tactic:
simp

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

Goal state before:
pp: case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0

Tactic:
simp

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

Goal state before:
pp: case pred
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0

Tactic:
simp

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m : ℤ
⊢ A ^ (m + 0) = A ^ m * A ^ 0

Tactic:
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
⊢ ∀ (x : n →₀ R), 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * 0 i j * xj

Tactic:
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
ι : Type u_5
inst✝ : AddLeftMono R
x : ι → Matrix n n R
s : Finset ι
h : ∀ i ∈ s, (x i).PosSemidef
⊢ (∑ i ∈ s, x i).PosSemidef

Tactic:
refine ⟨isSelfAdjoint_sum s fun _ hi => h _ hi |>.1, fun y => ?_⟩
  simp [sum_apply, Finset.mul_sum, Finset.sum_mul, Finsupp.sum_finsetSum_comm,
    Finset.sum_nonneg fun _ hi => (h _ hi).2 _]

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:
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:
simp

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

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inl ⊕ᵥ x ∘ Sum.inr) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ∘ Sum.inl ⊕ᵥ x ∘ Sum.inr)

Tactic:
schur_complement_eq₁₁ B D _ _ hA.1

Goal state after:
case mpr
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) +
      star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case e'_1
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ B = Bᴴᴴ

Tactic:
simp

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

Goal state before:
pp: case e'_2
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ B = Bᴴᴴ

Tactic:
simp

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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
simp

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

Goal state before:
pp: case inl
ι : 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 ι
i : ↥b.support
⊢ |b.cartanMatrix i i| = (if i = i then 4 else 0) - b.cartanMatrix i i

Tactic:
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:
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:
simp

Goal state after: