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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
h₁ :
  ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (prodCartan eι b₁ b₂)) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
h₂ :
  (lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}).toSubmodule = span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}
x✝ : L₁
⊢ x✝ ∈ ⇑(LinearMap.fst R L₁ L₂) '' {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ↔ x✝ ∈ Set.range b₁.h

Tactic:
;

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
h₁ :
  ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (prodCartan eι b₁ b₂)) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
h₂ :
  (lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}).toSubmodule = span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}
x✝ : L₁
⊢ x✝ ∈ ⇑(LinearMap.fst R L₁ L₂) '' {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ↔ x✝ ∈ Set.range b₁.h
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g ∈ degreeLT R #s

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g ∈ degreeLT R #s
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this :
  lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
    lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
x✝ : ↥(prod eι b₁ b₂)
⊢ x✝ ∈ range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) ↔
    x✝ ∈
      Subtype.val ⁻¹'
        ({x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪
          {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x})

Tactic:
;

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this :
  lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
    lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
x✝ : ↥(prod eι b₁ b₂)
⊢ x✝ ∈ range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) ↔
    x✝ ∈
      Subtype.val ⁻¹'
        ({x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪
          {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x})
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (-1) ^ ↑0 * W 0 0 * (of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j).det =
    ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
det_mul_column,

Goal state after:
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (-1) ^ ↑0 * W 0 0 * ((∏ i, (v i.succ - r * w i.succ)) * (projVandermonde (v ∘ succ) (w ∘ succ)).det) =
    ∏ i, ∏ j > i, (v j * w i - v i * w j)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0

Tactic:
exact ⟨j, ⟨mem_erase.mpr ⟨hij.symm, hj⟩, eval_basisDivisor_right⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ degree 1 < ↑(#s)

Tactic:
degree_one,

Goal state after:
case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ 0 < ↑(#s)
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
i j : ι₁
⊢ ⁅prodH eι b₁ b₂ j, prodF eι b₁ b₂ i⁆ = -b₁.A i j • prodF eι b₁ b₂ i

Tactic:
by simp [Subtype.ext_iff, b₁.lie_h_f, b₂.lie_h_f, ← hA]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r r' : ι → F
hrr' : ∀ i ∈ s, r i = r' i
i : ι
hi : i ∈ s
⊢ C (r i) * Lagrange.basis s v i = C (r' i) * Lagrange.basis s v i

Tactic:
hrr' _ hi

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r r' : ι → F
hrr' : ∀ i ∈ s, r i = r' i
i : ι
hi : i ∈ s
⊢ C (r' i) * Lagrange.basis s v i = C (r' i) * Lagrange.basis s v i
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
f : F[X]
hf : f.degree < ↑(#s)
| f

Tactic:
;

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
f : F[X]
hf : f.degree < ↑(#s)
| f
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
⊢ ∀ (x : Fin n), (x ∈ univ ∧ ∃ a ∈ Ioi x, v a = v x) → ∃ i j, v i = v j ∧ i ≠ j

Tactic:
rintro i ⟨_, j, h₁, h₂⟩

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
i : Fin n
left✝ : i ∈ univ
j : Fin n
h₁ : j ∈ Ioi i
h₂ : v j = v i
⊢ ∃ i j, v i = v j ∧ i ≠ j
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₂
hy :
  (prodSymmEquiv eι b₁ b₂).symm y ∈
    lieSpan R (↥(prod eι.symm b₂ b₁))
      (⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})
x✝ : ↥(prod eι.symm b₂ b₁)
⊢ x✝ ∈ {x | ∃ i, ⟨(b₂.h i, b₁.h (eι.symm i)), ⋯⟩ = x} ↔
    x✝ ∈ ⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}

Tactic:
;

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₂
hy :
  (prodSymmEquiv eι b₁ b₂).symm y ∈
    lieSpan R (↥(prod eι.symm b₂ b₁))
      (⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})
x✝ : ↥(prod eι.symm b₂ b₁)
⊢ x✝ ∈ {x | ∃ i, ⟨(b₂.h i, b₁.h (eι.symm i)), ⋯⟩ = x} ↔
    x✝ ∈ ⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₂
hy :
  (prodSymmEquiv eι b₁ b₂).symm y ∈
    lieSpan R (↥(prod eι.symm b₂ b₁))
      (⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})
x✝ : ↥(prod eι.symm b₂ b₁)
⊢ (∃ i, ⟨(b₂.h i, b₁.h (eι.symm i)), ⋯⟩ = x✝) ↔ ∃ a, ⟨(b₂.h (eι a), b₁.h a), ⋯⟩ = x✝

Tactic:
;

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₂
hy :
  (prodSymmEquiv eι b₁ b₂).symm y ∈
    lieSpan R (↥(prod eι.symm b₂ b₁))
      (⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})
x✝ : ↥(prod eι.symm b₂ b₁)
⊢ (∃ i, ⟨(b₂.h i, b₁.h (eι.symm i)), ⋯⟩ = x✝) ↔ ∃ a, ⟨(b₂.h (eι a), b₁.h a), ⋯⟩ = x✝
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm : ((ad R L) x ^ m) y = 0
n : ℕ
hn : ((ad R L) x ^ n) z = 0
ij : ℕ × ℕ
hij : ij.1 + ij.2 = m + n
⊢ m ≤ ij.1 ∨ n ≤ ij.2

Tactic:
;

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm : ((ad R L) x ^ m) y = 0
n : ℕ
hn : ((ad R L) x ^ n) z = 0
ij : ℕ × ℕ
hij : ij.1 + ij.2 = m + n
⊢ m ≤ ij.1 ∨ n ≤ ij.2
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := ⋯
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := ⋯
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ (engel R x).toSubmodule

Tactic:
rw [Submodule.map_le_iff_le_comap]

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype (engel R x).toSubmodule
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
y : ↥N
hy : y ∈ (dx ^ (k + 1)).ker
⊢ ((ad R L) x ^ (k + 1)) (N.subtype y) = 0

Tactic:
;

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
y : ↥N
hy : y ∈ (dx ^ (k + 1)).ker
⊢ ((ad R L) x ^ (k + 1)) (N.subtype y) = 0
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h.zero.mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
val✝ : L
property✝ : val✝ ∈ N
⊢ ⟨val✝, property✝⟩ ∈ (dx ^ 0).ker → ((ad R L) x ^ 0) (N.subtype ⟨val✝, property✝⟩) = 0

Tactic:
;

Goal state after:
case h.zero.mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
val✝ : L
property✝ : val✝ ∈ N
⊢ ⟨val✝, property✝⟩ ∈ (dx ^ 0).ker → ((ad R L) x ^ 0) (N.subtype ⟨val✝, property✝⟩) = 0
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h.zero.mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
val✝ : L
property✝ : val✝ ∈ N
hy : ⟨val✝, property✝⟩ ∈ (dx ^ 0).ker
⊢ ((ad R L) x ^ 0) (N.subtype ⟨val✝, property✝⟩) = 0

Tactic:
;

Goal state after:
case h.zero.mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
val✝ : L
property✝ : val✝ ∈ N
hy : ⟨val✝, property✝⟩ ∈ (dx ^ 0).ker
⊢ ((ad R L) x ^ 0) (N.subtype ⟨val✝, property✝⟩) = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : P.degree = ⊥
⊢ ↑(#s) ≠ P.degree + 1

Tactic:
;

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : P.degree = ⊥
⊢ ↑(#s) ≠ P.degree + 1
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := ⋯
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := ⋯
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ Submodule.map N.subtype (dx ^ (k + 1)).range ≤ H.toSubmodule

Tactic:
rw [Submodule.map_le_iff_le_comap]

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype H.toSubmodule
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : #s = deg + 1
hdegree : P.degree = ↑(#s - 1)
⊢ ↑(#s - 1) < ↑(#s)

Tactic:
;

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : #s = deg + 1
hdegree : P.degree = ↑(#s - 1)
⊢ ↑(#s - 1) < ↑(#s)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : #s = deg + 1
hdegree : P.degree = ↑(#s - 1)
⊢ #s - 1 < #s

Tactic:
;

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : #s = deg + 1
hdegree : P.degree = ↑(#s - 1)
⊢ #s - 1 < #s
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ : Type u_6
x✝ : MvPolynomial α✝ R
⊢ id <$> x✝ = x✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ : Type u_6
x✝ : MvPolynomial α✝ R
⊢ id <$> x✝ = x✝
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ γ✝ : Type u_6
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : MvPolynomial α✝ R
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ γ✝ : Type u_6
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : MvPolynomial α✝ R
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝¹ : MvPolynomial α✝ R
x✝ : MvPolynomial β✝ R
⊢ (bind₁ fun a ↦ (bind₁ fun x ↦ X a) x✝) x✝¹ = (bind₁ ((fun y ↦ (rename y) x✝) ∘ Function.const β✝)) x✝¹

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝¹ : MvPolynomial α✝ R
x✝ : MvPolynomial β✝ R
⊢ (bind₁ fun a ↦ (bind₁ fun x ↦ X a) x✝) x✝¹ = (bind₁ ((fun y ↦ (rename y) x✝) ∘ Function.const β✝)) x✝¹
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝¹ : MvPolynomial α✝ R
x✝ : MvPolynomial β✝ R
⊢ (bind₁ fun a ↦ (bind₁ fun x ↦ X a) x✝) x✝¹ = (bind₁ ((fun y ↦ (aeval (X ∘ y)) x✝) ∘ Function.const β✝)) x✝¹

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝¹ : MvPolynomial α✝ R
x✝ : MvPolynomial β✝ R
⊢ (bind₁ fun a ↦ (bind₁ fun x ↦ X a) x✝) x✝¹ = (bind₁ ((fun y ↦ (aeval (X ∘ y)) x✝) ∘ Function.const β✝)) x✝¹
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ x✝ *> y✝ = Function.const α✝ id <$> x✝ <*> y✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ x✝ *> y✝ = Function.const α✝ id <$> x✝ <*> y✝
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ (bind₁ fun x ↦ y✝) x✝ = (bind₁ (Function.const α✝ y✝)) x✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ (bind₁ fun x ↦ y✝) x✝ = (bind₁ (Function.const α✝ y✝)) x✝
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
g✝ : α✝ → β✝
x✝ : MvPolynomial α✝ R
⊢ pure g✝ <*> x✝ = g✝ <$> x✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
g✝ : α✝ → β✝
x✝ : MvPolynomial α✝ R
⊢ pure g✝ <*> x✝ = g✝ <$> x✝
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝ : α✝
f✝ : α✝ → MvPolynomial β✝ R
⊢ pure x✝ >>= f✝ = f✝ x✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝ : α✝
f✝ : α✝ → MvPolynomial β✝ R
⊢ pure x✝ >>= f✝ = f✝ x✝
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ γ✝ : Type u_6
x✝ : MvPolynomial α✝ R
f✝ : α✝ → MvPolynomial β✝ R
g✝ : β✝ → MvPolynomial γ✝ R
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ γ✝ : Type u_6
x✝ : MvPolynomial α✝ R
f✝ : α✝ → MvPolynomial β✝ R
g✝ : β✝ → MvPolynomial γ✝ R
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝