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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, x✝.left⁆ + ⁅x✝¹.left, x✝.left⁆ + ((ψ x✝².right) x✝.left + (ψ x✝¹.right) x✝.left) -
      ((ψ x✝.right) x✝².left + (ψ x✝.right) x✝¹.left) =
    ⁅x✝².left, x✝.left⁆ + (ψ x✝².right) x✝.left - (ψ x✝.right) x✝².left +
      (⁅x✝¹.left, x✝.left⁆ + (ψ x✝¹.right) x✝.left - (ψ x✝.right) x✝¹.left)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, x✝.left⁆ + ⁅x✝¹.left, x✝.left⁆ + ((ψ x✝².right) x✝.left + (ψ x✝¹.right) x✝.left) -
      ((ψ x✝.right) x✝².left + (ψ x✝.right) x✝¹.left) =
    ⁅x✝².left, x✝.left⁆ + (ψ x✝².right) x✝.left - (ψ x✝.right) x✝².left +
      (⁅x✝¹.left, x✝.left⁆ + (ψ x✝¹.right) x✝.left - (ψ x✝.right) x✝¹.left)
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, x✝¹.left⁆ + ⁅x✝².left, x✝.left⁆ + ((ψ x✝².right) x✝¹.left + (ψ x✝².right) x✝.left) -
      ((ψ x✝¹.right) x✝².left + (ψ x✝.right) x✝².left) =
    ⁅x✝².left, x✝¹.left⁆ + (ψ x✝².right) x✝¹.left - (ψ x✝¹.right) x✝².left +
      (⁅x✝².left, x✝.left⁆ + (ψ x✝².right) x✝.left - (ψ x✝.right) x✝².left)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, x✝¹.left⁆ + ⁅x✝².left, x✝.left⁆ + ((ψ x✝².right) x✝¹.left + (ψ x✝².right) x✝.left) -
      ((ψ x✝¹.right) x✝².left + (ψ x✝.right) x✝².left) =
    ⁅x✝².left, x✝¹.left⁆ + (ψ x✝².right) x✝¹.left - (ψ x✝¹.right) x✝².left +
      (⁅x✝².left, x✝.left⁆ + (ψ x✝².right) x✝.left - (ψ x✝.right) x✝².left)
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, ⁅x✝¹.left, x✝.left⁆⁆ + ⁅x✝².left, (ψ x✝¹.right) x✝.left⁆ - ⁅x✝².left, (ψ x✝.right) x✝¹.left⁆ +
        (⁅x✝¹.left, (ψ x✝².right) x✝.left⁆ - ⁅x✝.left, (ψ x✝².right) x✝¹.left⁆ + (ψ x✝².right) ((ψ x✝¹.right) x✝.left) -
          (ψ x✝².right) ((ψ x✝.right) x✝¹.left)) -
      ((ψ x✝¹.right) ((ψ x✝.right) x✝².left) - (ψ x✝.right) ((ψ x✝¹.right) x✝².left)) =
    ⁅x✝².left, ⁅x✝¹.left, x✝.left⁆⁆ - ⁅x✝¹.left, ⁅x✝².left, x✝.left⁆⁆ + ⁅(ψ x✝².right) x✝¹.left, x✝.left⁆ -
            ⁅(ψ x✝¹.right) x✝².left, x✝.left⁆ +
          ((ψ x✝².right) ((ψ x✝¹.right) x✝.left) - (ψ x✝¹.right) ((ψ x✝².right) x✝.left)) -
        (⁅x✝².left, (ψ x✝.right) x✝¹.left⁆ - ⁅x✝¹.left, (ψ x✝.right) x✝².left⁆ + (ψ x✝.right) ((ψ x✝².right) x✝¹.left) -
          (ψ x✝.right) ((ψ x✝¹.right) x✝².left)) +
      (⁅x✝¹.left, ⁅x✝².left, x✝.left⁆⁆ + ⁅x✝¹.left, (ψ x✝².right) x✝.left⁆ - ⁅x✝¹.left, (ψ x✝.right) x✝².left⁆ +
          (⁅x✝².left, (ψ x✝¹.right) x✝.left⁆ - ⁅x✝.left, (ψ x✝¹.right) x✝².left⁆ +
              (ψ x✝¹.right) ((ψ x✝².right) x✝.left) -
            (ψ x✝¹.right) ((ψ x✝.right) x✝².left)) -
        ((ψ x✝².right) ((ψ x✝.right) x✝¹.left) - (ψ x✝.right) ((ψ x✝².right) x✝¹.left)))

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, ⁅x✝¹.left, x✝.left⁆⁆ + ⁅x✝².left, (ψ x✝¹.right) x✝.left⁆ - ⁅x✝².left, (ψ x✝.right) x✝¹.left⁆ +
        (⁅x✝¹.left, (ψ x✝².right) x✝.left⁆ - ⁅x✝.left, (ψ x✝².right) x✝¹.left⁆ + (ψ x✝².right) ((ψ x✝¹.right) x✝.left) -
          (ψ x✝².right) ((ψ x✝.right) x✝¹.left)) -
      ((ψ x✝¹.right) ((ψ x✝.right) x✝².left) - (ψ x✝.right) ((ψ x✝¹.right) x✝².left)) =
    ⁅x✝².left, ⁅x✝¹.left, x✝.left⁆⁆ - ⁅x✝¹.left, ⁅x✝².left, x✝.left⁆⁆ + ⁅(ψ x✝².right) x✝¹.left, x✝.left⁆ -
            ⁅(ψ x✝¹.right) x✝².left, x✝.left⁆ +
          ((ψ x✝².right) ((ψ x✝¹.right) x✝.left) - (ψ x✝¹.right) ((ψ x✝².right) x✝.left)) -
        (⁅x✝².left, (ψ x✝.right) x✝¹.left⁆ - ⁅x✝¹.left, (ψ x✝.right) x✝².left⁆ + (ψ x✝.right) ((ψ x✝².right) x✝¹.left) -
          (ψ x✝.right) ((ψ x✝¹.right) x✝².left)) +
      (⁅x✝¹.left, ⁅x✝².left, x✝.left⁆⁆ + ⁅x✝¹.left, (ψ x✝².right) x✝.left⁆ - ⁅x✝¹.left, (ψ x✝.right) x✝².left⁆ +
          (⁅x✝².left, (ψ x✝¹.right) x✝.left⁆ - ⁅x✝.left, (ψ x✝¹.right) x✝².left⁆ +
              (ψ x✝¹.right) ((ψ x✝².right) x✝.left) -
            (ψ x✝¹.right) ((ψ x✝.right) x✝².left)) -
        ((ψ x✝².right) ((ψ x✝.right) x✝¹.left) - (ψ x✝.right) ((ψ x✝².right) x✝¹.left)))
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
a₁✝ : K
⊢ ∀ ⦃a₂ : K⦄, (inl ψ) a₁✝ = (inl ψ) a₂ → a₁✝ = a₂

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
a₁✝ : K
⊢ ∀ ⦃a₂ : K⦄, (inl ψ) a₁✝ = (inl ψ) a₂ → a₁✝ = a₂
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x : K
y : L
⊢ { left := x, right := y } ∈ (inl ψ).range ↔
    { left := x, right := y } ∈ LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x : K
y : L
⊢ { left := x, right := y } ∈ (inl ψ).range ↔
    { left := x, right := y } ∈ LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker
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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
x✝¹ x✝ : ofTwoCocycle c
⊢ ((ofProd c).symm x✝¹).2 + ((ofProd c).symm x✝).2 - (x ((ofProd c).symm x✝¹).1 + x ((ofProd c).symm x✝).1) =
    ((ofProd c).symm x✝¹).2 - x ((ofProd c).symm x✝¹).1 + (((ofProd c).symm x✝).2 - x ((ofProd c).symm x✝).1)

Tactic:
;

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
x✝¹ x✝ : ofTwoCocycle c
⊢ ((ofProd c).symm x✝¹).2 + ((ofProd c).symm x✝).2 - (x ((ofProd c).symm x✝¹).1 + x ((ofProd c).symm x✝).1) =
    ((ofProd c).symm x✝¹).2 - x ((ofProd c).symm x✝¹).1 + (((ofProd c).symm x✝).2 - x ((ofProd c).symm x✝).1)
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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
x✝ y✝ : ofTwoCocycle c
⊢ (↑c ((ofProd c).symm x✝).1) ((ofProd c).symm y✝).1 + ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).2⁆ -
        ⁅((ofProd c).symm y✝).1, ((ofProd c).symm x✝).2⁆ -
      x ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).1⁆ =
    (↑c ((ofProd c).symm x✝).1) ((ofProd c).symm y✝).1 +
          (⁅((ofProd c).symm x✝).1, x ((ofProd c).symm y✝).1⁆ - ⁅((ofProd c).symm y✝).1, x ((ofProd c).symm x✝).1⁆ -
            x ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).1⁆) +
        (⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).2⁆ - ⁅((ofProd c).symm x✝).1, x ((ofProd c).symm y✝).1⁆) -
      (⁅((ofProd c).symm y✝).1, ((ofProd c).symm x✝).2⁆ - ⁅((ofProd c).symm y✝).1, x ((ofProd c).symm x✝).1⁆)

Tactic:
;

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
x✝ y✝ : ofTwoCocycle c
⊢ (↑c ((ofProd c).symm x✝).1) ((ofProd c).symm y✝).1 + ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).2⁆ -
        ⁅((ofProd c).symm y✝).1, ((ofProd c).symm x✝).2⁆ -
      x ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).1⁆ =
    (↑c ((ofProd c).symm x✝).1) ((ofProd c).symm y✝).1 +
          (⁅((ofProd c).symm x✝).1, x ((ofProd c).symm y✝).1⁆ - ⁅((ofProd c).symm y✝).1, x ((ofProd c).symm x✝).1⁆ -
            x ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).1⁆) +
        (⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).2⁆ - ⁅((ofProd c).symm x✝).1, x ((ofProd c).symm y✝).1⁆) -
      (⁅((ofProd c).symm y✝).1, ((ofProd c).symm x✝).2⁆ - ⁅((ofProd c).symm y✝).1, x ((ofProd c).symm x✝).1⁆)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∉ l'
this : l'.formPerm x = x
⊢ l.formPerm x = x ∨ l'.formPerm x = x

Tactic:
;

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∉ l'
this : l'.formPerm x = x
⊢ l.formPerm x = x ∨ l'.formPerm x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∉ l
this : l.formPerm x = x
⊢ l.formPerm x = x ∨ l'.formPerm x = x

Tactic:
;

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∉ l
this : l.formPerm x = x
⊢ l.formPerm x = x ∨ l'.formPerm 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
x y : M
⊢ ↑⟨E.incl ⁅x, y⁆, ⋯⟩ = ↑⁅⟨E.incl x, ⋯⟩, ⟨E.incl y, ⋯⟩⁆

Tactic:
;

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
x y : M
⊢ ↑⟨E.incl ⁅x, y⁆, ⋯⟩ = ↑⁅⟨E.incl x, ⋯⟩, ⟨E.incl y, ⋯⟩⁆
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
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
z : ↥E.proj.ker
⊢ ⁅⁅Exists.choose h x, Exists.choose h y⁆ - Exists.choose h ⁅x, y⁆, z⁆ = 0

Tactic:
exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ z

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✝¹⁆ + ⁅s x, s x✝⁆ - (s ⁅x, x✝¹⁆ + s ⁅x, x✝⁆) = ⁅s x, s x✝¹⁆ - s ⁅x, x✝¹⁆ + (⁅s x, s x✝⁆ - s ⁅x, x✝⁆)

Tactic:
;

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.LieTheorem

Goal state before:
pp: case h
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
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
x : ↥U
this : ∃ k, (T χ w ^ k) ↑x = 0
n : ℕ
hn : (T χ w ^ n) ↑x = 0
⊢ ↑((T χ w ^ n) x) = (T χ w ^ n) ↑x

Tactic:
;

Goal state after:
case h
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
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
x : ↥U
this : ∃ k, (T χ w ^ k) ↑x = 0
n : ℕ
hn : (T χ w ^ n) ↑x = 0
⊢ ↑((T χ w ^ n) x) = (T χ w ^ n) ↑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:
;

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
⊢ ↑({ 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✝)
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
⊢ ⁅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✝⁆)

Tactic:
;

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

Tactic:
;

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✝² : R
x✝¹ x✝ : L
⊢ ↑({ toFun := fun y ↦ ⟨⁅s (x✝² • x✝¹), s y⁆ - s ⁅x✝² • x✝¹, y⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x✝) =
    ↑(((RingHom.id R) x✝² • { toFun := fun y ↦ ⟨⁅s x✝¹, s y⁆ - s ⁅x✝¹, y⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }) x✝)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : f.SameCycle x y
⊢ (f.toList x).formPerm y = (f.cycleOf x) y

Tactic:
obtain ⟨k, _, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx)

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f.toList x).formPerm ((f ^ k) x) = (f.cycleOf x) ((f ^ k) x)
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
x y : loopAlgebra R A L
x✝¹ : A
x✝ : L
⊢ ((TensorProduct.AlgebraTensorModule.curry
            { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) (x + y)) (-a))) v,
              map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ({ toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) x) (-a))) v,
                map_add' := ⋯, map_smul' := ⋯ } +
              { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) y) (-a))) v,
                map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
;

Goal state after:
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
x y : loopAlgebra R A L
x✝¹ : A
x✝ : L
⊢ ((TensorProduct.AlgebraTensorModule.curry
            { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) (x + y)) (-a))) v,
              map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ({ toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) x) (-a))) v,
                map_add' := ⋯, map_smul' := ⋯ } +
              { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) y) (-a))) v,
                map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝
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
r : R
x : loopAlgebra R A L
x✝¹ : A
x✝ : L
⊢ ((TensorProduct.AlgebraTensorModule.curry
            { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) (r • x)) (-a))) v,
              map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((RingHom.id R) r •
              { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) x) (-a))) v,
                map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
;

Goal state after:
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
r : R
x : loopAlgebra R A L
x✝¹ : A
x✝ : L
⊢ ((TensorProduct.AlgebraTensorModule.curry
            { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) (r • x)) (-a))) v,
              map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((RingHom.id R) r •
              { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) x) (-a))) v,
                map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case e_s
R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ Finset.Ico (↑i + 1) n = {x ∈ Finset.range n | ↑i < x}

Tactic:
;

Goal state after:
case e_s
R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ Finset.Ico (↑i + 1) n = {x ∈ Finset.range n | ↑i < x}
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case e_s
R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
a✝ : ℕ
⊢ a✝ ∈ Finset.Ico (↑i + 1) n ↔ a✝ ∈ {x ∈ Finset.range n | ↑i < x}

Tactic:
;

Goal state after:
case e_s
R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
a✝ : ℕ
⊢ a✝ ∈ Finset.Ico (↑i + 1) n ↔ a✝ ∈ {x ∈ Finset.range n | ↑i < x}