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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
this :
  b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (((TensorProduct.AlgebraTensorModule.curry
                    (((TensorProduct.AlgebraTensorModule.curry
                            ((Cohomology.d₂₃ R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R))
                              (twoCochainOfBilinear R A L Φ hΦs)) ∘ₗ
                          AddMonoidAlgebra.lsingle a)
                        1)
                      x) ∘ₗ
                  AddMonoidAlgebra.lsingle b)
                1)
              y) ∘ₗ
          AddMonoidAlgebra.lsingle c)
        1)
      z =
    ((TensorProduct.AlgebraTensorModule.curry
            (((TensorProduct.AlgebraTensorModule.curry
                    (((TensorProduct.AlgebraTensorModule.curry 0 ∘ₗ AddMonoidAlgebra.lsingle a) 1) x) ∘ₗ
                  AddMonoidAlgebra.lsingle b)
                1)
              y) ∘ₗ
          AddMonoidAlgebra.lsingle c)
        1)
      z

Tactic:
by

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

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x✝¹ : R
x✝ : L
⊢ E.toKer.symm ⟨s₁ (x✝¹ • x✝) - s₂ (x✝¹ • x✝), ⋯⟩ = (RingHom.id R) x✝¹ • E.toKer.symm ⟨s₁ x✝ - s₂ x✝, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s, ∃ (h : s.Nodup), s.formPerm h = f

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s, (↑s).formPerm ⋯ = f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
this : b • (Φ ⁅x, z⁆) y = c • (Φ ⁅x, y⁆) z + a • (Φ ⁅y, z⁆) x
⊢ b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ s x - s' x ∈ E.proj.ker

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
trace_T_U_zero : ∀ (w : A), (LinearMap.trace R ↥U) (T χ w) = 0
trace_za : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = χ ⁅z, a⁆ • ↑(finrank R ↥U)
⊢ v ∈ U

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ s' y - s y ∈ E.proj.ker

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ ⁅s x - s' x, s' y - s y⁆ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
trace_T_U_zero : ∀ (w : A), (LinearMap.trace R ↥U) (T χ w) = 0
trace_za : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = χ ⁅z, a⁆ • ↑(finrank R ↥U)
hvU : v ∈ U
⊢ ⟨v, hvU⟩ ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
this : ∀ {s' : L → E.L}, LeftInverse (⇑E.proj) s' → ⁅s x - s' x, s' y - s y⁆ = 0
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ -b ≠ a + c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ -c ≠ a + b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ -a ≠ b + c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : v ∈ weightSpace V χ
⊢ ⁅z, v⁆ ∈ weightSpace V χ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
i j : ℕ
⊢ BirdDet.get n A i j = A.getD (n * i + j) 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n lo : ℕ
f : ℕ → R
h : lo < n
⊢ BirdDet.sumFrom n lo f = f lo + BirdDet.sumFrom n (lo + 1) f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n lo : ℕ
f : ℕ → R
h : ¬lo < n
⊢ BirdDet.sumFrom n lo f = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
F : ℕ → ℕ → R
i j : ℕ
⊢ stepEntry n A F i j =
    (-BirdDet.sumFrom n (i + 1) fun k ↦ F k k) * BirdDet.get n A i j +
      BirdDet.sumFrom n (i + 1) fun k ↦ F i k * BirdDet.get n A k j

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
A : Array R
⊢ birdDet 0 A = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Array R
⊢ birdDet (k + 1) A = (-1) ^ k * (stepEntry (k + 1) A)^[k] (BirdDet.get (k + 1) A) 0 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n k : ℕ
A : Array R
hn : n = k + 1
⊢ birdDet n A = (-1) ^ k * (stepEntry n A)^[k] (BirdDet.get n A) 0 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A F : Matrix (Fin n) (Fin n) R
⊢ stepEntry A F = Matrix.of fun i j ↦ (-∑ k > i, F k k) * A i j + ∑ k > i, F i k * A k j

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 0) (Fin 0) R
⊢ birdDet A = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Matrix (Fin (k + 1)) (Fin (k + 1)) R
⊢ birdDet A = (-1) ^ k * (stepEntry A)^[k] A 0 0

Tactic:
by

Goal state after:
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
⊢ z ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n lo : ℕ
f : ℕ → R
⊢ BirdDet.sumFrom n lo f = ∑ k ∈ Finset.Ico lo n, f k

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ BirdDet.sumFrom n (↑i + 1) f = ∑ k ∈ Finset.Ico (↑i + 1) n, f k

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ ∑ k ∈ Finset.Ico (↑i + 1) n, f k = ∑ k ∈ Finset.range n with ↑i < k, f k

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ ∑ k ∈ Finset.range n with ↑i < k, f k = ∑ k ∈ Finset.range n, if ↑i < k then f k else 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ (∑ k ∈ Finset.range n, if ↑i < k then f k else 0) = ∑ k, if ↑i < ↑k then f ↑k else 0

Tactic:
by

Goal state after:
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
⊢ ∀ (x : ↥(k ∙ z)), e x • z = ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
⊢ twoCochainOfBilinear R A L Φ hΦs ∈
    Cohomology.twoCocycle R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ (∑ k, if ↑i < ↑k then f ↑k else 0) = ∑ k > i, f ↑k

Tactic:
by

Goal state after:
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, ((toEnd k L ↥W) z).HasEigenvalue c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
⊢ (d₁₂ R L M) (E.oneCochainOfTwoSplitting hs₁ hs₂) = ↑(E.twoCocycleOf hs₁) - ↑(E.twoCocycleOf hs₂)

Tactic:
by

Goal state after:
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
t : ℕ
i j : Fin n
⊢ (stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j = (Spec.stepEntry (Matrix.ofArray A hA))^[t] (Matrix.ofArray A hA) i j

Tactic:
by

Goal state after:
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⟩
⊢ ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v

Tactic:
by

Goal state after:
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
⊢ birdDet n A = Spec.birdDet (Matrix.ofArray A hA)

Tactic:
by

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 : ℕ
α : Fin (p + 1) → Fin n
i : Fin n
s : Fin (p + 1)
⊢ (A.submatrix (Fin.cons i (s.removeNth α)) α).det =
    (-1) ^ ↑s * ((A.submatrix (Fin.cons i (s.removeNth α)) α).submatrix id ⇑(Equiv.symm s.cycleRange)).det

Tactic:
by

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 : ℕ
α : Fin (p + 1) → Fin n
i : Fin n
s : Fin (p + 1)
⊢ (-1) ^ ↑s * ((A.submatrix (Fin.cons i (s.removeNth α)) α).submatrix id ⇑(Equiv.symm s.cycleRange)).det =
    (-1) ^ ↑s * bminor A i (α s) (s.removeNth α)

Tactic:
by

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 : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ bminor A i j α =
    A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det

Tactic:
by

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 : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det =
    pminor A α * A i j + ∑ s, (-1) ^ (↑s + 1) * (A.submatrix (Fin.cons i (s.removeNth α)) α).det * A (α s) j

Tactic:
by

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 : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ pminor A α * A i j + ∑ s, (-1) ^ (↑s + 1) * (A.submatrix (Fin.cons i (s.removeNth α)) α).det * A (α s) j =
    pminor A α * A i j + ∑ s, -(bminor A i (α s) (s.removeNth α) * A (α s) j)

Tactic:
by

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 : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ pminor A α * A i j + ∑ s, -(bminor A i (α s) (s.removeNth α) * A (α s) j) =
    pminor A α * A i j - ∑ s, bminor A i (α s) (s.removeNth α) * A (α s) j

Tactic:
by

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 : ℕ
α : Fin p → Fin n
i : Fin n
q : Fin p
⊢ ∀ (k : Fin (p + 1)),
    A.submatrix (Fin.cons i α) (Fin.cons (α q) α) k q.succ = A.submatrix (Fin.cons i α) (Fin.cons (α q) α) k 0

Tactic:
by

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 : ℕ
k : Fin n
α : Fin p → Fin n
i : Fin n
hk : k ∈ Set.range α
⊢ bminor A i k α = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ S 0 i = {![]}

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ S p 0 = {Fin.succ}

Tactic:
by

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

Goal state before:
pp: n p : ℕ
i : Fin n
⊢ S (p + 1) i = (Finset.Ioi i).biUnion fun k ↦ Finset.image (Fin.cons k) (S p k)

Tactic:
by

Goal state after:
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
this : ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = (c • e (π₂ x)) • v
⊢ ⁅π₁ x, v⁆ + ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v

Tactic:
by

Goal state after:
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
this : ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = (c • e (π₂ x)) • v
⊢ χ₀ (π₁ x) • v + (c • e (π₂ x)) • v = (χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂) x • v

Tactic:
by

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

Goal state before:
pp: n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hα : α ∈ S p i
hik : i < k
hk : k ∉ Set.range α
⊢ ∃ t, t.insertNth k α ∈ S (p + 1) i

Tactic:
by

Goal state after: