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

Goal state before:
pp: case lie
L : Type u_2
M : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
R : Type u_4
inst✝³ : CommRing R
inst✝² : LieAlgebra R L
inst✝¹ : Module R M
inst✝ : LieModule R L M
s : Set L
hs : ∀ x ∈ s, (trace R M) ((toEnd R L M) x) = 0
x u v : L
hx✝ : u ∈ LieSubalgebra.lieSpan R L s
hy✝ : v ∈ LieSubalgebra.lieSpan R L s
a✝¹ : (trace R M) ((toEnd R L M) u) = 0
a✝ : (trace R M) ((toEnd R L M) v) = 0
⊢ (trace R M) ((toEnd R L M) ⁅u, v⁆) = 0

Tactic:
simp

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
w : A
x : V
hx : x ∈ (⨆ k, U' k).carrier
⊢ ⁅w, x⁆ = (T χ w) x + χ w • x

Tactic:
simp

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

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
⊢ (x :: y :: l).formPerm w ≠ w → (x :: y :: l).formPerm.SameCycle x w

Tactic:
hw

Goal state after:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : (x :: y :: l).formPerm w ≠ w
⊢ (x :: y :: l).formPerm.SameCycle x w
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
hl : (x :: l).Nodup
hn : 2 ≤ (x :: l).length
⊢ (x :: l).formPerm.IsCycle

Tactic:
induction l generalizing x with

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
E : Extension R M L
x : E.L
y : M
⊢ E.proj ⁅x, E.incl y⁆ = 0

Tactic:
LieHom.map_lie,

Goal state after:
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
E : Extension R M L
x : E.L
y : M
⊢ ⁅E.proj x, E.proj (E.incl y)⁆ = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ↑[l.attach.length] = {l.length}

Tactic:
simp

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
x✝¹ x✝ : M
⊢ ⟨E.incl (x✝¹ + x✝), ⋯⟩ = ⟨E.incl x✝¹, ⋯⟩ + ⟨E.incl x✝, ⋯⟩

Tactic:
simp

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
x✝¹ : R
x✝ : M
⊢ ⟨E.incl (x✝¹ • x✝), ⋯⟩ = (RingHom.id R) x✝¹ • ⟨E.incl x✝, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: case h0
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ [l.attach.formPerm].prod = l.attach.formPerm

Tactic:
simp

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

Goal state before:
pp: case h2
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ Pairwise Perm.Disjoint [l.attach.formPerm]

Tactic:
simp

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

Goal state before:
pp: case mk.nil
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : [].length ≤ 1
⊢ [].formPerm = 1

Tactic:
simp

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

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s✝ : Cycle α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) s) h).support = toFinset (Quot.mk (⇑(IsRotated.setoid α)) s)

Tactic:
refine support_formPerm_of_nodup s h ?_

Goal state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s✝ : Cycle α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ ∀ (x : α), s ≠ [x]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ 2 ≤ (p.toList x).length ↔ x ∈ p.support

Tactic:
simp

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

Goal state before:
pp: case neg.zero.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
hn✝ : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
hm✝ : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ 0) x = (p.cycleOf x ^ 0) x → 0 = 0

Tactic:
simp

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
this : LieRingModule L M := E.ringModuleOf
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
r : R
x : L
m : M
⊢ ⁅x, r • m⁆ = r • ⁅x, m⁆

Tactic:
simp

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
x : ↥E.proj.ker
y : L
⊢ E.toKer ⁅y, E.toKer.symm x⁆ = ⁅Exists.choose ⋯ y, x⁆

Tactic:
simp

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 : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x x✝¹ x✝ : L
⊢ ⟨⁅s x, s (x✝¹ + x✝)⁆ - s ⁅x, x✝¹ + x✝⁆, ⋯⟩ = ⟨⁅s x, s x✝¹⁆ - s ⁅x, x✝¹⁆, ⋯⟩ + ⟨⁅s x, s x✝⁆ - s ⁅x, x✝⁆, ⋯⟩

Tactic:
simp

Goal state after:
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 : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x x✝¹ x✝ : L
⊢ ⁅s x, s x✝¹⁆ + ⁅s x, s x✝⁆ - (s ⁅x, x✝¹⁆ + s ⁅x, x✝⁆) = ⁅s x, s x✝¹⁆ - s ⁅x, x✝¹⁆ + (⁅s x, s x✝⁆ - s ⁅x, x✝⁆)
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 : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y x✝ : L
⊢ ↑({ toFun := fun y_1 ↦ ⟨⁅s (x + y), s y_1⁆ - s ⁅x + y, y_1⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x✝) =
    ↑(({ toFun := fun y ↦ ⟨⁅s x, s y⁆ - s ⁅x, y⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := fun y_1 ↦ ⟨⁅s y, s y_1⁆ - s ⁅y, y_1⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ })
        x✝)

Tactic:
simp

Goal state after:
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 : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y x✝ : L
⊢ ⁅s x, s x✝⁆ + ⁅s y, s x✝⁆ - (s ⁅x, x✝⁆ + s ⁅y, x✝⁆) = ⁅s x, s x✝⁆ - s ⁅x, x✝⁆ + (⁅s y, s x✝⁆ - s ⁅y, x✝⁆)
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
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
⊢ (E.twoCocycleAux hs).compr₂ ↑E.toKer.symm.toLinearEquiv ∈ twoCochain R L M

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ [].formPerm.toList x = []

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : α
⊢ [x].formPerm.toList y = []

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xj : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
⊢ ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) 0,
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x✝ : α
hl : 2 ≤ [x✝].length
hn : [x✝].Nodup
hc : [x✝].formPerm.IsCycle
⊢ False

Tactic:
simp at hl

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

Goal state before:
pp: case tmul.zero
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
x : ↥(AddMonoidAlgebra.grade R i)
y : L
⊢ ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) 0⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
y v : L
x : AddMonoidAlgebra R A
hx : x ∈ AddMonoidAlgebra.grade R i
u : AddMonoidAlgebra R A
hu : u ∈ AddMonoidAlgebra.grade R j
⊢ (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) (⟨x * u, ⋯⟩ ⊗ₜ[R] ⁅y, v⁆) =
    ⁅↑⟨x, hx⟩ ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) (⟨u, hu⟩ ⊗ₜ[R] v)⁆

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ (iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length).length = l.length

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ l.rotate ↑k ~r l

Tactic:
simp

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✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xi : ↥(AddMonoidAlgebra.grade R i) ⊗[R] L
xj : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
⊢ ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) xi,
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
induction xi using TensorProduct.induction_on with

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✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A := (F x).support ∪ (F y).support
hu₁ : (F x).support ⊆ u
hu₂ : (F y).support ⊆ u
hu₃ : (F (x + y)).support ⊆ u
⊢ ∀ i ∈ u, i • (Φ ((F f) (-i))) 0 = 0

Tactic:
simp

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✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
r : R
x : loopAlgebra R A L
⊢ ∀ i ∈ (F x).support, i • (Φ ((F f) (-i))) 0 = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
⊢ Finset.univ.val = x ::ₘ Finset.univ.val.erase x

Tactic:
simp

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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
⊢ ∀ i ∈ s, i • (Φ ((F f) (-i))) 0 = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : f x ≠ x
⊢ x = (f ^ 0) x

Tactic:
simp

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

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝¹ : α
val✝ : Cycle α
x x✝ : α
hn✝ : Cycle.Nodup (Quot.mk ⇑(IsRotated.setoid α) [x✝])
ht : Cycle.Nontrivial (Quot.mk ⇑(IsRotated.setoid α) [x✝])
hl : 2 ≤ [x✝].length
hn : [x✝].Nodup
hx : x ∈ [x✝]
⊢ False

Tactic:
simp at hl

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:
subst hn
  exact birdDet_succ k A

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:
rw [Matrix.det_permute']
      simp [← mul_assoc, ← pow_add]

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
⊢ (-1) ^ ↑0 * A.submatrix (Fin.cons i α) (Fin.cons j α) 0 0 *
        ((A.submatrix (Fin.cons i α) (Fin.cons j α)).submatrix (Fin.succAbove 0) Fin.succ).det +
      ∑ i_1,
        (-1) ^ ↑i_1.succ * A.submatrix (Fin.cons i α) (Fin.cons j α) i_1.succ 0 *
          ((A.submatrix (Fin.cons i α) (Fin.cons j α)).submatrix i_1.succ.succAbove Fin.succ).det =
    A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det

Tactic:
simp

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

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 ⇑χ₀)
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
obtain ⟨z, -, hz⟩ := SetLike.exists_of_lt (hA.lt_top)
  let e : (k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z <| by aesop).symm
  have he : ∀ x, e x • z = x := by simp [e]
  have hA : IsCompl A.toSubmodule (k ∙ z) := isCompl_span_singleton_of_isCoatom_of_notMem hA hz
  let π₁ : L →ₗ[k] A       := A.toSubmodule.projectionOnto (k ∙ z) hA
  let π₂ : L →ₗ[k] (k ∙ z) := (k ∙ z).projectionOnto ↑A hA.symm
  set W : LieSubmodule k L V := weightSpaceOfIsLieTower k V χ₀
  obtain ⟨c, hc⟩ : ∃ c, (toEnd k _ W z).HasEigenvalue c := by
    have : Nontrivial W := inferInstanceAs (Nontrivial (weightSpace V χ₀))
    apply Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top
    exact LieModule.IsTriangularizable.maxGenEigenspace_eq_top z
  obtain ⟨⟨v, hv⟩, hvc⟩ := hc.exists_hasEigenvector
  have hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v := by
    simpa [W, weightSpaceOfIsLieTower, mem_weightSpace] using hv
  use (χ₀.comp π₁) + c • (e.comp π₂)
  refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
  · rw [mem_weightSpace]
    intro x
    have hπ : (π₁ x : L) + π₂ x = x := projection_add_projection_eq_self hA x
    suffices ⁅projection _ _ hA.symm x, v⁆ = (c • e (π₂ x)) • v by
      calc ⁅x, v⁆
          = ⁅π₁ x, v⁆ + ⁅projection _ _ hA.symm x, v⁆ := congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _
        _ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v    := by rw [hv' (π₁ x), this]
        _ = _ := by simp [add_smul]
    calc ⁅projection _ _ hA.symm x, v⁆
        = e (π₂ x) • ↑(c • ⟨v, hv⟩ : W) := by
          rw [projection_apply, ← he, smul_lie, ← hvc.apply_eq_smul]; rfl
      _ = (c • e (π₂ x)) • v            := by rw [smul_assoc, smul_comm]; rfl
  · simpa [ne_eq, LieSubmodule.mk_eq_zero] using hvc.right

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 → Fin n
k : Fin n
hα : α ∈ S p i
hk : i < k
hoccurs : k ∉ Set.range α
hnotmem : ¬bminor A i (α, k).2 (α, k).1 * A (α, k).2 j = 0
t : Fin (p + 1)
ht : t.insertNth k α ∈ S (p + 1) i
⊢ (fun x ↦
        match x with
        | (α, k) => (k.removeNth α, α k))
      (t.insertNth k α, t) =
    (α, k)

Tactic:
simp

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

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

Goal state before:
pp: R : Type u_1
M : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
e : M ≃+ L
x✝² x✝¹ x✝ : M
⊢ e.symm ⁅e (x✝² + x✝¹), e x✝⁆ = e.symm ⁅e x✝², e x✝⁆ + e.symm ⁅e x✝¹, e x✝⁆

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
e : M ≃+ L
x✝² x✝¹ x✝ : M
⊢ e.symm ⁅e x✝², e (x✝¹ + x✝)⁆ = e.symm ⁅e x✝², e x✝¹⁆ + e.symm ⁅e x✝², e x✝⁆

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
e : M ≃+ L
x✝ : M
⊢ e.symm ⁅e x✝, e x✝⁆ = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
e : M ≃+ L
x✝² x✝¹ x✝ : M
⊢ e.symm ⁅e x✝², e (e.symm ⁅e x✝¹, e x✝⁆)⁆ =
    e.symm ⁅e (e.symm ⁅e x✝², e x✝¹⁆), e x✝⁆ + e.symm ⁅e x✝¹, e (e.symm ⁅e x✝², e x✝⁆)⁆

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 0) (Fin 0) R
⊢ A.det = Spec.birdDet A

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² : Derivation R A₁ A₁
x✝¹ x✝ : A₁
⊢ ⁅x✝², x✝¹ * x✝⁆ = x✝¹ • ⁅x✝², x✝⁆ + ⁅x✝², x✝¹⁆ * x✝

Tactic:
simp

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² : Derivation R A₁ A₁
x✝¹ x✝ : A₁
⊢ x✝ * x✝² x✝¹ = x✝² x✝¹ * x✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝¹ : A₁
x✝ : L₁
⊢ LieHom.id (x✝¹ • x✝) = (AlgHom.id R A₁) x✝¹ • LieHom.id x✝

Tactic:
simp

Goal state after: