mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ (s.sup fun b ↦ (Lagrange.basis s v b).degree) < ↑(#s)

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)

pp: case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∀ i ∈ s, eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1

Tactic:
·

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ (s.sup fun b ↦ (Lagrange.basis s v b).degree) < ↑(#s)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ (s.sup fun b ↦ (Lagrange.basis s v b).degree) < ↑(#s)

Tactic:
rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #s)]

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∀ b ∈ s, (Lagrange.basis s v b).degree < ↑(#s)
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)

pp: case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∀ i ∈ s, eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1

Tactic:
·

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
⊢ degree 1 < ↑(#s)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∀ i ∈ s, eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1

Tactic:
·

Goal state after:
case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∀ i ∈ s, eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: case hx
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodE eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))

pp: case hy
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodF eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))

Tactic:
·

Goal state after:
case hx
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodE eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: case hy
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodF eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))

Tactic:
·

Goal state after:
case hy
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodF eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : ¬r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : ¬r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Tactic:
·

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : ¬r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ ((interpolate ∅ v) r).degree < ↑(#∅)

pp: case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ((interpolate s v) r).degree < ↑(#s)

Tactic:
·

Goal state after:
case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ ((interpolate ∅ v) r).degree < ↑(#∅)
Module: Mathlib.LinearAlgebra.Lagrange

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

Tactic:
·

Goal state after:
case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ((interpolate s v) r).degree < ↑(#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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
⊢ Surjective ⇑((LieHom.snd R L₁ L₂).comp L.incl)

Tactic:
set p₂ : L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl

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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
⊢ Surjective ⇑p₂
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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ Surjective ⇑p₂

Tactic:
rw [← LieHom.range_eq_top, eq_top_iff, ← b₂.span_ef, map_top,
    ← b₁.basisProd_aux eι b₂, map_lieSpan, image_union, h₁, h₂]

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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₂ (range (⇑p₂ ∘ prodE eι b₁ b₂) ∪ range (⇑p₂ ∘ prodF eι b₁ b₂)) ≤
    lieSpan R L₂ (⇑p₂ '' range (prodE eι b₁ b₂) ∪ ⇑p₂ '' range (prodF eι b₁ b₂))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v) r

pp: case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i

Tactic:
·

Goal state after:
case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v) r
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i

Tactic:
·

Goal state after:
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
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
⊢ (vandermonde v).det = 0 → ∃ i j, v i = v j ∧ i ≠ j

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → (vandermonde v).det = 0

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
⊢ (vandermonde v).det = 0 → ∃ i j, v i = v j ∧ i ≠ j
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → (vandermonde v).det = 0

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → (vandermonde v).det = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
⊢ (s.sup fun b ↦ ((interpolate (insert b (t \ s)) v) r * Lagrange.basis s v b).degree) < ↑(#t)

pp: case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
⊢ eval (v i) (∑ i ∈ s, (interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i) = r i

Tactic:
·

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
⊢ (s.sup fun b ↦ ((interpolate (insert b (t \ s)) v) r * Lagrange.basis s v b).degree) < ↑(#t)
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ j > 0, (↑↑j - ↑↑0) = ↑n.succ.factorial

pp: case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑n.superFactorial

Tactic:
·

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ j > 0, (↑↑j - ↑↑0) = ↑n.succ.factorial
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑n.superFactorial

Tactic:
·

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑n.superFactorial
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
⊢ eval (v i) (∑ i ∈ s, (interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i) = r i

Tactic:
·

Goal state after:
case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
⊢ eval (v i) (∑ i ∈ s, (interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i) = r i
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e'_2
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ eval (↑(v x✝¹)) (descPochhammer ℤ ↑x✝) = ↑(↑x✝).factorial * of (fun i j ↦ ↑((v i).choose ↑j)) x✝¹ x✝

pp: case e'_3.e'_5
n : ℕ
v : Fin n → ℕ
⊢ ↑(∏ i, (↑i).factorial) = ∏ i, ↑(↑i).factorial

Tactic:
·

Goal state after:
case e'_2
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ eval (↑(v x✝¹)) (descPochhammer ℤ ↑x✝) = ↑(↑x✝).factorial * of (fun i j ↦ ↑((v i).choose ↑j)) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i

pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e'_3.e'_5
n : ℕ
v : Fin n → ℕ
⊢ ↑(∏ i, (↑i).factorial) = ∏ i, ↑(↑i).factorial

Tactic:
·

Goal state after:
case e'_3.e'_5
n : ℕ
v : Fin n → ℕ
⊢ ↑(∏ i, (↑i).factorial) = ∏ i, ↑(↑i).factorial
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i

Tactic:
·

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ engel R 0

Tactic:
rw [mem_engel_iff, map_zero]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∃ n, (0 ^ n) x = 0
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₂
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieAlgebra K L₁
inst✝³ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝² : LieAlgebra K L₂
inst✝¹ : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
f : ↥H₁ × ↥H₂ →ₗ[K] ↥(prodCartan eι b₁ b₂) := { toFun := fun x ↦ ⟨⟨(↑x.1, ↑x.2), ⋯⟩, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
f_inj : Injective ⇑f
g : ↥H₁ × ↥H₂ →ₗ[K] ↥H₁ := ↑(prodCartanEquiv eι b₁ b₂) ∘ₗ f
⊢ Injective ⇑g

Tactic:
simpa [g]

Goal state after:
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
⊢ (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)

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
⊢ (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)

Tactic:
·

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 := ⋯
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
⊢ (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)
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
⊢ (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)

Tactic:
·

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 := ⋯
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
⊢ (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
i j : I
⊢ ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)

Tactic:
rw [instLieRingModule_eq, v.lie_end_of_apply_eq_smul μ s hsv]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
v_def : v = fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
i : ι
h : ∃ i_1, x i_1 = x i
⊢ y h.choose = y i

pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
v_def : v = fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
i : ι
h : ¬∃ i_1, x i_1 = x i
⊢ 0 = y i

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
v_def : v = fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
i : ι
h : ∃ i_1, x i_1 = x i
⊢ y h.choose = y i
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
v_def : v = fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
i : ι
h : ¬∃ i_1, x i_1 = x i
⊢ 0 = y i

Tactic:
·

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
v_def : v = fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
i : ι
h : ¬∃ i_1, x i_1 = x i
⊢ 0 = y i
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
v : ι → R
inst✝ : Nontrivial R
⊢ nodal ∅ v ≠ 0

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ nodal s v ≠ 0

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
v : ι → R
inst✝ : Nontrivial R
⊢ nodal ∅ v ≠ 0