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
i : ι
hi : i ∈ s
⊢ #s - 1 < #s

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
i : ι
hi : i ∈ s
⊢ #s - 1 < #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
⊢ 0 < #s

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
⊢ 0 < #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 : ι
hi : i ∈ s
⊢ ∑ i_1 ∈ s, eval (v i) (Lagrange.basis s v i_1) = eval (v i) 1

Tactic:
eval_one,

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 : ι
hi : i ∈ s
⊢ ∑ i_1 ∈ s, eval (v i) (Lagrange.basis s v i_1) = 1
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 : ι
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, eval (v i) (Lagrange.basis s v x) = 0

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 : ι
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, eval (v i) (Lagrange.basis s v x) = 0
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 : ι
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right✝ : j ∈ s
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = basisDivisor x y + basisDivisor y x

Tactic:
]

Goal state after:
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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ ⁅prodE 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:
ι₁ : 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, 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: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s✝ t : Finset ι
i j : ι
v✝ r r' : ι → F
s : Finset ι
v f g : ι → F
h :
  (fun x ↦ C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) = fun x ↦
    C ((f + g) x) * Lagrange.basis s v x
⊢ ∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i = ∑ x ∈ s, C ((f + g) x) * Lagrange.basis s v x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
⊢ 0 = 0

Tactic:
]

Goal state after:
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
j : Fin n
a✝ : j.succ ∈ univ
hj0 : j.succ ≠ 0
⊢ ((-1) ^ ↑j.succ = 0 ∨ W 0 j.succ = 0) ∨ (W.submatrix succ j.succ.succAbove).det = 0

Tactic:
]

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
j : Fin n
a✝ : j.succ ∈ univ
hj0 : j.succ ≠ 0
⊢ ((-1) ^ ↑j.succ = 0 ∨ W 0 j.succ = 0) ∨ (W.submatrix succ j.succ.succAbove).det = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
i : ι
v r : ι → F
⊢ C (r i) = C (r i)

Tactic:
]

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 ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (C (r i) * Lagrange.basis s v i) + ∑ x ∈ s.erase i, eval (v i) (C (r x) * Lagrange.basis s v x) = r i

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (C (r i) * Lagrange.basis s v i) + ∑ x ∈ s.erase i, eval (v i) (C (r x) * Lagrange.basis s v x) = r i
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ 0 = 0

Tactic:
]

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 : ι → F
hvs : Set.InjOn v ↑s
⊢ ∀ b ∈ s, (C (r b) * Lagrange.basis s v b).degree ≤ ↑(#s - 1)

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ ∀ b ∈ s, (C (r b) * Lagrange.basis s v b).degree ≤ ↑(#s - 1)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: 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
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Tactic:
]

Goal state after:
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
⊢ (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
⊢ ↑(#s - 1) ≤ ↑(#s - 1)

Tactic:
]

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 : ι → F
hvs : Set.InjOn v ↑s
⊢ ((interpolate s v) r).degree < ↑(#s)

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ ((interpolate s v) r).degree < ↑(#s)
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 ↑∅
⊢ ⊥ < ↑0

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 ↑∅
⊢ ⊥ < ↑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₂
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.fst 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₂))

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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅R⁆ L₁ := (LieHom.fst 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 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
⊢ #s - 1 < #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
⊢ #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 ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ((interpolate (s.erase i) v) r).degree < ↑(#(s.erase i))

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ((interpolate (s.erase i) v) r).degree < ↑(#(s.erase i))
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
hvs : Set.InjOn v ↑s
hrr' : (interpolate s v) r = (interpolate s v) r'
x✝ : ι
hi : x✝ ∈ s
⊢ r' x✝ = r' x✝

Tactic:
]

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

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 : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ i ∈ s, eval (v i) f = r i
⊢ ((interpolate s v) fun i ↦ eval (v i) f) = (interpolate s v) r

Tactic:
]

Goal state after:
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
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ i ∈ s, eval (v i) f = r i
⊢ ((interpolate s v) fun i ↦ eval (v i) f) = (interpolate s v) r
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₂)
⊢ 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₂))

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₂
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.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false)).det =
    ∏ i,
      ∏ i_1 > i,
        (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
          MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false))
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false)).det =
    ∏ i,
      ∏ i_1 > i,
        (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
          MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false))
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
        (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))).det =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
        (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))).det =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
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
⊢ ((interpolate s v) r).degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) ((interpolate s v) r) = 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
⊢ ((interpolate s v) r).degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) ((interpolate s v) r) = r 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)
⊢ ((interpolate s v) fun x ↦ if x ∈ s then eval (v x) f else 0) = 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)
⊢ ((interpolate s v) fun x ↦ if x ∈ s then eval (v x) f else 0) = f
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})
⊢ (prodSymmEquiv eι b₁ b₂).symm y ∈ prodCartan eι.symm b₂ b₁

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})
⊢ (prodSymmEquiv eι b₁ b₂).symm y ∈ prodCartan eι.symm b₂ b₁
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 : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ v j ^ ↑k = v j ^ ↑k

Tactic:
]

Goal state after:
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})
⊢ (prodSymmEquiv eι b₁ b₂).symm y ∈ lieSpan R ↥(prod eι.symm b₂ b₁) {x | ∃ i, ⟨(b₂.h i, b₁.h (eι.symm 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})
⊢ (prodSymmEquiv eι b₁ b₂).symm y ∈ lieSpan R ↥(prod eι.symm b₂ b₁) {x | ∃ i, ⟨(b₂.h i, b₁.h (eι.symm i)), ⋯⟩ = x}
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i ↦ v i - a).det = (vandermonde fun i ↦ v i + -a).det

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i ↦ v i - a).det = (vandermonde fun i ↦ v i + -a).det
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ ∑ i_1, (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1 = ∑ j_1, of (fun i j ↦ v i ^ ↑j) i j_1 * (p j).coeff ↑j_1

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ ∑ i_1, (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1 = ∑ j_1, of (fun i j ↦ v i ^ ↑j) i j_1 * (p j).coeff ↑j_1
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e_f
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
k : Fin n
⊢ v i ^ ↑k * (p j).coeff ↑k = v i ^ ↑k * (p j).coeff ↑k

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: 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 ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
⊢ #t = #t

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ (vandermonde v).det = (vandermonde v).det

Tactic:
]

Goal state after:
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
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ ((interpolate (insert i (t \ s)) v) r).degree < ↑(1 + (#t - #s))

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
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ ((interpolate (insert i (t \ s)) v) r).degree < ↑(1 + (#t - #s))
Module: Mathlib.LinearAlgebra.Vandermonde

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

Tactic:
]

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