mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
n₁ n₂ : ↑{n | n ≠ 0}
h : (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₁ = (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₂
⊢ n₁ = n₂

pp: case refine_2
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
χ : ↑s
⊢ ∃ a, (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) a = χ

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
n₁ n₂ : ↑{n | n ≠ 0}
h : (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₁ = (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₂
⊢ n₁ = n₂
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
χ : ↑s
⊢ ∃ a, (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) a = χ

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
χ : ↑s
⊢ ∃ a, (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) a = χ
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
this : (2 * X * U R (↑n + 1)).degree = ↑(n + 2)
⊢ (2 * X * U R (↑n + 1)).degree = ↑n + 2

pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
this : (2 * X * U R (↑n + 1)).degree = ↑(n + 2)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree

Tactic:
·

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
this : (2 * X * U R (↑n + 1)).degree = ↑(n + 2)
⊢ (2 * X * U R (↑n + 1)).degree = ↑n + 2
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
this : (2 * X * U R (↑n + 1)).degree = ↑(n + 2)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree

Tactic:
·

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
this : (2 * X * U R (↑n + 1)).degree = ↑(n + 2)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ (U R (↑(m + 1 + 1) - 2)).degree = (U R ↑m).degree

pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ (U R ↑m).degree = ↑((-↑(m + 1 + 1) + 1).natAbs - 1)

Tactic:
·

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ (U R (↑(m + 1 + 1) - 2)).degree = (U R ↑m).degree
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ (U R ↑m).degree = ↑((-↑(m + 1 + 1) + 1).natAbs - 1)

Tactic:
·

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ (U R ↑m).degree = ↑((-↑(m + 1 + 1) + 1).natAbs - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ 2 * 1 * 2 ^ (n + 1) = 2 ^ (n + 2)

pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree

Tactic:
·

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ 2 * 1 * 2 ^ (n + 1) = 2 ^ (n + 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree

Tactic:
·

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ eval (-x) (U R ↑(n + 2)) = ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))

pp: R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n)) =
    ↑↑(↑(n + 2)).negOnePow * eval x (U R ↑(n + 2))

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ eval (-x) (U R ↑(n + 2)) = ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n)) =
    ↑↑(↑(n + 2)).negOnePow * eval x (U R ↑(n + 2))

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n)) =
    ↑↑(↑(n + 2)).negOnePow * eval x (U R ↑(n + 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n + 1) = X * U R n + T R (n + 1)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [U_two, T_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := U_add_two R (n + 1)
    have h₂ := U_add_two R n
    have h₃ := T_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_add_two R (-n - 1)
    have h₂ := U_add_two R (-n)
    have h₃ := T_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ 2 • T R ↑(n + 2) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))

Tactic:
·

Goal state after:
case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ 2 • T R ↑(n + 2) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case «0»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨0, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨1, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨2, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
·

Goal state after:
case «0»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨0, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case «1»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨1, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨2, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
·

Goal state after:
case «1»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨1, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case «2»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨2, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
·

Goal state after:
case «2»
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨2, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
cf : K
hcf : hf.choose = cf • f
hce₀ : ce ≠ 0
hcf₀ : cf ≠ 0
x✝ : ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
c₁ c₂ c₃ : K
hx : x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
⊢ x = (c₁ * ce⁻¹) • ce • e + (c₂ * cf⁻¹) • cf • f + (c₃ * ce⁻¹ * cf⁻¹) • ⁅ce • e, cf • f⁆

Tactic:
·

Goal state after:
case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
cf : K
hcf : hf.choose = cf • f
hce₀ : ce ≠ 0
hcf₀ : cf ≠ 0
x✝ : ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
c₁ c₂ c₃ : K
hx : x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
⊢ x = (c₁ * ce⁻¹) • ce • e + (c₂ * cf⁻¹) • cf • f + (c₃ * ce⁻¹ * cf⁻¹) • ⁅ce • e, cf • f⁆
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ⁅↑h, c₁ • e + c₂ • f + c₃ • ⁅e, f⁆⁆ ∈ sl2SubalgebraOfRoot hα

Tactic:
rw [mem_sl2SubalgebraOfRoot_iff hα ht heα hfα, lie_add, lie_add, lie_smul, lie_smul, lie_smul]

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ∃ c₁_1 c₂_1 c₃_1, c₁ • ⁅↑h, e⁆ + c₂ • ⁅↑h, f⁆ + c₃ • ⁅↑h, ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hx : x ∈ sl2SubmoduleOfRoot hα
⊢ x ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α

pp: case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hx : x ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ x ∈ sl2SubmoduleOfRoot hα

Tactic:
·

Goal state after:
case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hx : x ∈ sl2SubmoduleOfRoot hα
⊢ x ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_1.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₁ • e ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α

pp: case refine_1.refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₂ • f ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α

pp: case refine_1.refine_3
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₃ • ⁅e, f⁆ ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α

Tactic:
·

Goal state after:
case refine_1.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₁ • e ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α