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

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (((k ∙ z).projectionOnto ↑A ⋯) x) • ⁅z, v⁆ = e (π₂ x) • ↑(((toEnd k L ↥W) z) ⟨v, hv⟩)

Tactic:
]

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (((k ∙ z).projectionOnto ↑A ⋯) x) • ⁅z, v⁆ = e (π₂ x) • ↑(((toEnd k L ↥W) z) ⟨v, hv⟩)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ x ∈ S (p + 1) i, pminor A x * A i j - ∑ x ∈ S (p + 1) i, ∑ t, bminor A i (x t) (t.removeNth x) * A (x t) j =
    ∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ α ∈ S (p + 1) i, ∑ t, bminor A i (α t) (t.removeNth α) * A (α t) j

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ x ∈ S p i ×ˢ Finset.Ioi i, bminor A i x.2 x.1 * A x.2 j =
    ∑ x ∈ S (p + 1) i ×ˢ Finset.univ, bminor A i (x.1 x.2) (x.2.removeNth x.1) * A (x.1 x.2) j

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ x ∈ S p i ×ˢ Finset.Ioi i, bminor A i x.2 x.1 * A x.2 j =
    ∑ x ∈ S (p + 1) i ×ˢ Finset.univ, bminor A i (x.1 x.2) (x.2.removeNth x.1) * A (x.1 x.2) j
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ↑(c • ⟨v, hv⟩) = e (π₂ x) • c • v

Tactic:
]

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ↑(c • ⟨v, hv⟩) = e (π₂ x) • c • v
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin (p + 1) → Fin n
k : Fin (p + 1)
hi : ∀ (j : Fin (p + 1)), i < α j
hiα : StrictMono α
α' : Fin (p + 1) → Fin n
k' : Fin (p + 1)
hj : ∀ (j : Fin (p + 1)), i < α' j
hiα' : StrictMono α'
hremove : k.removeNth α = k'.removeNth α'
hvalue : α k = α' k'
hrange : α = α'
⊢ α = α' ∧ k = k'

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin (p + 1) → Fin n
k : Fin (p + 1)
hi : ∀ (j : Fin (p + 1)), i < α j
hiα : StrictMono α
α' : Fin (p + 1) → Fin n
k' : Fin (p + 1)
hj : ∀ (j : Fin (p + 1)), i < α' j
hiα' : StrictMono α'
hremove : k.removeNth α = k'.removeNth α'
hvalue : α k = α' k'
hrange : α = α'
⊢ α = α' ∧ k = k'
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin (p + 1) → Fin n
k : Fin (p + 1)
hi : ∀ (j : Fin (p + 1)), i < α j
hiα : StrictMono α
α' : Fin (p + 1) → Fin n
k' : Fin (p + 1)
hj : ∀ (j : Fin (p + 1)), i < α' j
hiα' : StrictMono α'
hremove : k.removeNth α = k'.removeNth α'
hvalue : α k = α' k'
⊢ Set.range α = Set.range α

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin (p + 1) → Fin n
k : Fin (p + 1)
hi : ∀ (j : Fin (p + 1)), i < α j
hiα : StrictMono α
α' : Fin (p + 1) → Fin n
k' : Fin (p + 1)
hj : ∀ (j : Fin (p + 1)), i < α' j
hiα' : StrictMono α'
hremove : k.removeNth α = k'.removeNth α'
hvalue : α k = α' k'
⊢ Set.insert (α' k') (Set.range (k'.removeNth α')) = Set.insert (α' k') (Set.range (k'.removeNth α'))

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin (p + 1) → Fin n
k : Fin (p + 1)
hi : ∀ (j : Fin (p + 1)), i < α j
hiα : StrictMono α
α' : Fin (p + 1) → Fin n
k' : Fin (p + 1)
hj : ∀ (j : Fin (p + 1)), i < α' j
hiα' : StrictMono α'
hremove : k.removeNth α = k'.removeNth α'
hvalue : α k = α' k'
⊢ Set.range α' = Set.range α'

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin p → Fin n
k : Fin n
hnotmem :
  (α, k) ∉
    (fun x ↦
        match x with
        | (α, k) => (k.removeNth α, α k)) ''
      ↑(S (p + 1) i ×ˢ Finset.univ)
hα : α ∈ S p i
hk : i < k
hoccurs : k ∈ Set.range α
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inl.inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : derivedSeries k L 1 = ⊤
h✝ : Nontrivial L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
]

Goal state after:
case inl.inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : derivedSeries k L 1 = ⊤
h✝ : Nontrivial L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p✝ p : ℕ
ih : Eq1 A p
i j : Fin n
⊢ (-1) ^ (p + 1) *
      (∑ α ∈ S (p + 1) i, pminor A α * A i j -
        ∑ α' ∈ S (p + 1) i, ∑ t, bminor A i (α' t) (t.removeNth α') * A (α' t) j) =
    (-1) ^ (p + 1) *
      (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ α ∈ S (p + 1) i, ∑ t, bminor A i (α t) (t.removeNth α) * A (α t) j)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Matrix (Fin (k + 1)) (Fin (k + 1)) R
this : ∑ α ∈ S k 0, bminor A 0 0 α = A.det
⊢ A.det = (-1) ^ (k + k) * ∑ α ∈ S k 0, bminor A 0 0 α

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Matrix (Fin (k + 1)) (Fin (k + 1)) R
this : ∑ α ∈ S k 0, bminor A 0 0 α = A.det
⊢ A.det = (-1) ^ (k + k) * ∑ α ∈ S k 0, bminor A 0 0 α
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
⊢ Spec.birdDet (Matrix.ofArray A hA) = Spec.birdDet (Matrix.ofArray A ?hA)

pp: case hA
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
⊢ A.size = n * n

Tactic:
]

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

Goal state before:
pp: case h.refine_1
k : Type u_1
inst✝¹¹ : Field k
L : Type u_2
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : LieRingModule L V
inst✝⁵ : LieModule k L V
inst✝⁴ : CharZero k
inst✝³ : Module.Finite k V
inst✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
v : V
hv✝ : v ∈ weightSpace V ⇑χ
hv : ∀ (x : ↥imL), ⁅x, v⁆ = χ x • v
hv0 : ⟨v, hv✝⟩ ≠ 0
⊢ ∀ (x : L), ⁅x, v⁆ = (χ ∘ₗ toEndo) x • v

Tactic:
]

Goal state after:
case h.refine_1
k : Type u_1
inst✝¹¹ : Field k
L : Type u_2
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : LieRingModule L V
inst✝⁵ : LieModule k L V
inst✝⁴ : CharZero k
inst✝³ : Module.Finite k V
inst✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
v : V
hv✝ : v ∈ weightSpace V ⇑χ
hv : ∀ (x : ↥imL), ⁅x, v⁆ = χ x • v
hv0 : ⟨v, hv✝⟩ ≠ 0
⊢ ∀ (x : L), ⁅x, v⁆ = (χ ∘ₗ toEndo) x • v
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₁' L₂' : LieRinehartSubalgebra A L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ L₁' = L₂'

Tactic:
]

Goal state after:
A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ L₁' = L₂'
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₁' L₂' : LieRinehartSubalgebra A L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ ↑L₁' = ↑L₂'

Tactic:
]

Goal state after:
A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ ↑L₁' = ↑L₂'
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
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
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑((fun L' ↦ L'.toLieSubalgebra R) L₁') = ↑((fun L' ↦ L'.toLieSubalgebra R) L₂')
⊢ L₁' = L₂'

Tactic:
]

Goal state after:
A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module 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
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑((fun L' ↦ L'.toLieSubalgebra R) L₁') = ↑((fun L' ↦ L'.toLieSubalgebra R) L₂')
⊢ L₁' = L₂'
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
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
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑((fun L' ↦ L'.toLieSubalgebra R) L₁') = ↑((fun L' ↦ L'.toLieSubalgebra R) L₂')
⊢ ↑L₁' = ↑L₂'

Tactic:
]

Goal state after:
A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module 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
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑((fun L' ↦ L'.toLieSubalgebra R) L₁') = ↑((fun L' ↦ L'.toLieSubalgebra R) L₂')
⊢ ↑L₁' = ↑L₂'
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:
]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ B n i i = 2

Tactic:
by simp [B, Matrix.of_apply]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : ℕ
⊢ (if h : n + E.order < E.order then init ⟨n + E.order, h⟩
    else
      ∑ k,
        have x := ⋯;
        E.coeffs k * E.mkSol init (n + E.order - E.order + ↑k)) =
    ∑ i, E.coeffs i * E.mkSol init (n + ↑i)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : ℕ
⊢ (if h : n + E.order < E.order then init ⟨n + E.order, h⟩
    else
      ∑ k,
        have x := ⋯;
        E.coeffs k * E.mkSol init (n + E.order - E.order + ↑k)) =
    ∑ i, E.coeffs i * E.mkSol init (n + ↑i)
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
⊢ (C n)ᵀ = (C n)ᵀ

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : Fin E.order
⊢ (if h : ↑n < E.order then init ⟨↑n, h⟩
    else
      ∑ k,
        have x := ⋯;
        E.coeffs k * E.mkSol init (↑n - E.order + ↑k)) =
    init n

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : Fin E.order
⊢ (if h : ↑n < E.order then init ⟨↑n, h⟩
    else
      ∑ k,
        have x := ⋯;
        E.coeffs k * E.mkSol init (↑n - E.order + ↑k)) =
    init n
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n =
    if h : n < E.order then init ⟨n, h⟩
    else
      ∑ k,
        have x := ⋯;
        E.coeffs k * E.mkSol init (n - E.order + ↑k)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n =
    if h : n < E.order then init ⟨n, h⟩
    else
      ∑ k,
        have x := ⋯;
        E.coeffs k * E.mkSol init (n - E.order + ↑k)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ ∑ i, E.coeffs i * u (n - E.order + ↑i) = ∑ k, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ ∑ i, E.coeffs i * u (n - E.order + ↑i) = ∑ k, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case neg.e_f
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.coeffs k * E.mkSol init (n - E.order + ↑k) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Tactic:
]

Goal state after:
case neg.e_f
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.coeffs k * E.mkSol init (n - E.order + ↑k) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩ ↔ Set.EqOn u v ↑(range E.order)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩ ↔ Set.EqOn u v ↑(range E.order)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ((monomial E.order) 1).degree = ↑E.order

pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ((monomial E.order) 1).degree

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ((monomial E.order) 1).degree = ↑E.order

R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ((monomial E.order) 1).degree
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ↑E.order = ↑E.order

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ↑E.order

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ↑E.order
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
⊢ ∑ b, ((monomial ↑b) (E.coeffs b)).coeff E.order = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
⊢ ∑ b, ((monomial ↑b) (E.coeffs b)).coeff E.order = 0
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ ↑↑x✝¹ < ↑E.order

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ ↑↑x✝¹ < ↑E.order
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) ↔ eval₂ (RingHom.id R) q ((monomial E.order) 1 - ∑ i, (monomial ↑i) (E.coeffs i)) = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) ↔ eval₂ (RingHom.id R) q ((monomial E.order) 1 - ∑ i, (monomial ↑i) (E.coeffs i)) = 0
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
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : a ∈ corootSpace ⇑α
hx : H.toLieSubmodule.incl a ∈ corootSubmodule α
this : ↑⟨↑a, ⋯⟩ ∈ Submodule.span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
⊢ H.toLieSubmodule.incl a ∈ LieSubmodule.restr I H

Tactic:
]

Goal state after:
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
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : a ∈ corootSpace ⇑α
hx : H.toLieSubmodule.incl a ∈ corootSubmodule α
this : ↑⟨↑a, ⋯⟩ ∈ Submodule.span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
⊢ H.toLieSubmodule.incl a ∈ LieSubmodule.restr I H
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
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
⊢ ⁅coroot α, y⁆ ∈ ↑I

Tactic:
]

Goal state after:
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
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
⊢ ⁅coroot α, y⁆ ∈ ↑I
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
h : q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0
n : ℕ
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ q ^ n * (E.coeffs x✝¹ * q ^ ↑x✝¹) = E.coeffs x✝¹ * (q ^ n * q ^ ↑x✝¹)

Tactic:
by ring

Goal state after: