mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case h.refine_1.refine_1
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin p
x : Fin (p + 1)
hjx : j.castSucc < x
h : ∀ (i : Fin p), k < α i → x ≤ i.castSucc
⊢ α j < k

pp: case h.refine_1.refine_2
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin p
h : ∀ (b : Fin (p + 1)), j.castSucc < b → ∃ i, k < α i ∧ i.castSucc < b
⊢ k < α j

Tactic:
·

Goal state after:
case h.refine_1.refine_1
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin p
x : Fin (p + 1)
hjx : j.castSucc < x
h : ∀ (i : Fin p), k < α i → x ≤ i.castSucc
⊢ α j < k
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case h.refine_1.refine_2
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin p
h : ∀ (b : Fin (p + 1)), j.castSucc < b → ∃ i, k < α i ∧ i.castSucc < b
⊢ k < α j

Tactic:
·

Goal state after:
case h.refine_1.refine_2
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin p
h : ∀ (b : Fin (p + 1)), j.castSucc < b → ∃ i, k < α i ∧ i.castSucc < b
⊢ k < α j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case h.refine_2
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ i < t.insertNth k α t

pp: case h.refine_3
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ ∀ (j : Fin p), i < t.insertNth k α (t.succAbove j)

Tactic:
·

Goal state after:
case h.refine_2
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ i < t.insertNth k α t
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case h.refine_3
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ ∀ (j : Fin p), i < t.insertNth k α (t.succAbove j)

Tactic:
·

Goal state after:
case h.refine_3
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ ∀ (j : Fin p), i < t.insertNth k α (t.succAbove j)
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 : Fin n
hEq1 : Eq1 A p
⊢ (-1) ^ (p + 1) * ∑ k > i, ∑ α ∈ S p k, bminor A k k α =
    (-1) ^ (p + 1) * ∑ x > i, ∑ i ∈ Finset.image (Fin.cons x) (S p x), pminor A i

pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ (↑(Finset.Ioi i)).PairwiseDisjoint fun k ↦ Finset.image (Fin.cons k) (S p k)

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ (-1) ^ (p + 1) * ∑ k > i, ∑ α ∈ S p k, bminor A k k α =
    (-1) ^ (p + 1) * ∑ x > i, ∑ i ∈ Finset.image (Fin.cons x) (S p x), pminor A i
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 : Fin n
hEq1 : Eq1 A p
⊢ (↑(Finset.Ioi i)).PairwiseDisjoint fun k ↦ Finset.image (Fin.cons k) (S p k)

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ (↑(Finset.Ioi i)).PairwiseDisjoint fun k ↦ Finset.image (Fin.cons k) (S p k)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.InjOn
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ)

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.MapsTo
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ) ↑(S p i ×ˢ Finset.Ioi i)

pp: case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S p i ×ˢ Finset.Ioi i,
    i_1 ∉
        (fun x ↦
            match x with
            | (α, k) => (k.removeNth α, α k)) ''
          ↑(S (p + 1) i ×ˢ Finset.univ) →
      bminor A i i_1.2 i_1.1 * A i_1.2 j = 0

pp: case refine_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S (p + 1) i ×ˢ Finset.univ,
    bminor A i (i_1.1 i_1.2) (i_1.2.removeNth i_1.1) * A (i_1.1 i_1.2) j =
      bminor A i
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).1 *
        A
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          j

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.InjOn
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ)
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⟩) = (c • e (π₂ x)) • v

Tactic:
by rw [smul_assoc, smul_comm]; rfl

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.MapsTo
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ) ↑(S p i ×ˢ Finset.Ioi i)

pp: case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S p i ×ˢ Finset.Ioi i,
    i_1 ∉
        (fun x ↦
            match x with
            | (α, k) => (k.removeNth α, α k)) ''
          ↑(S (p + 1) i ×ˢ Finset.univ) →
      bminor A i i_1.2 i_1.1 * A i_1.2 j = 0

pp: case refine_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S (p + 1) i ×ˢ Finset.univ,
    bminor A i (i_1.1 i_1.2) (i_1.2.removeNth i_1.1) * A (i_1.1 i_1.2) j =
      bminor A i
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).1 *
        A
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          j

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.MapsTo
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ) ↑(S p i ×ˢ Finset.Ioi i)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S p i ×ˢ Finset.Ioi i,
    i_1 ∉
        (fun x ↦
            match x with
            | (α, k) => (k.removeNth α, α k)) ''
          ↑(S (p + 1) i ×ˢ Finset.univ) →
      bminor A i i_1.2 i_1.1 * A i_1.2 j = 0

pp: case refine_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S (p + 1) i ×ˢ Finset.univ,
    bminor A i (i_1.1 i_1.2) (i_1.2.removeNth i_1.1) * A (i_1.1 i_1.2) j =
      bminor A i
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).1 *
        A
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          j

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S p i ×ˢ Finset.Ioi i,
    i_1 ∉
        (fun x ↦
            match x with
            | (α, k) => (k.removeNth α, α k)) ''
          ↑(S (p + 1) i ×ˢ Finset.univ) →
      bminor A i i_1.2 i_1.1 * A i_1.2 j = 0
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case h.refine_2
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
⊢ ⟨v, ⋯⟩ ≠ 0

Tactic:
·

Goal state after:
case h.refine_2
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
⊢ ⟨v, ⋯⟩ ≠ 0
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 α
⊢ bminor A i (α, k).2 (α, k).1 * A (α, k).2 j = 0

pp: case neg
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 α
⊢ bminor A i (α, k).2 (α, k).1 * A (α, k).2 j = 0

Tactic:
·

Goal state after:
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 α
⊢ bminor A i (α, k).2 (α, k).1 * A (α, k).2 j = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case neg
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 α
⊢ bminor A i (α, k).2 (α, k).1 * A (α, k).2 j = 0

Tactic:
·

Goal state after:
case neg
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 α
⊢ bminor A i (α, k).2 (α, k).1 * A (α, k).2 j = 0
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inl
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) = ⊤
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

pp: case 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
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
·

Goal state after:
case inl
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) = ⊤
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inl.inl
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✝ : Subsingleton L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

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.inl
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✝ : Subsingleton L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case h
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✝ : Subsingleton L
⊢ Nontrivial ↥(weightSpace V ⇑0)

Tactic:
simpa [trivial_lie_zero, mem_weightSpace, nontrivial_iff] using exists_pair_ne V

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S (p + 1) i ×ˢ Finset.univ,
    bminor A i (i_1.1 i_1.2) (i_1.2.removeNth i_1.1) * A (i_1.1 i_1.2) j =
      bminor A i
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).1 *
        A
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          j

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S (p + 1) i ×ˢ Finset.univ,
    bminor A i (i_1.1 i_1.2) (i_1.2.removeNth i_1.1) * A (i_1.1 i_1.2) j =
      bminor A i
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).1 *
        A
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          j
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.Algebra.Lie.LieTheorem

Goal state before:
pp: 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
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∀ {x m : L}, m ∈ A → ⁅x, m⁆ ∈ A

pp: case 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
A : LieSubmodule k L L
hA : IsCoatom ↑A
hAL : ↑(derivedSeries k L 1) ≤ ↑A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
·

Goal state after:
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
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∀ {x m : L}, m ∈ A → ⁅x, m⁆ ∈ A
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ (Spec.stepEntry A)^[0] A i j = Matrix.of (fun i j ↦ (-1) ^ 0 * ∑ α ∈ S 0 i, bminor A i j α) i j

Tactic:
simp [iterate_zero_apply, S_zero, bminor]

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 ⇑χ
hv0 : ⟨v, hv⟩ ≠ 0
⊢ v ∈ weightSpace V ⇑(χ ∘ₗ toEndo)

pp: case h.refine_2
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 ⇑χ
hv0 : ⟨v, hv⟩ ≠ 0
⊢ ⟨v, ?h.refine_1⟩ ≠ 0

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 ⇑χ
hv0 : ⟨v, hv⟩ ≠ 0
⊢ v ∈ weightSpace V ⇑(χ ∘ₗ toEndo)