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

Goal state before:
pp: case succ.inr.inl.inr
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
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
hne : n ≠ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : ↑n ≤ a
b : S
hb : ↑n ≤ b
hab : a ≤ b
⊢ (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b

Tactic:
]

Goal state after:
case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : ↑n ≤ a
b : S
hb : ↑n ≤ b
hab : a ≤ b
⊢ (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b
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₂
⊢ ↑(lieSpan R (L₁ × L₂) (⇑(prod eι b₁ b₂).incl '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})) =
    ↑(lieSpan R (L₁ × L₂) {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₂
⊢ ↑(lieSpan R (L₁ × L₂) (⇑(prod eι b₁ b₂).incl '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.descFactorial b) = ↑(a.descFactorial b)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.descFactorial b) = ↑(a.descFactorial b)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ x ∈ s, eval x f = 0
⊢ f = 0

Tactic:
← mem_degreeLT

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, eval x f = 0
⊢ f = 0
Module: Mathlib.LinearAlgebra.Lagrange

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, eval x f = 0
⊢ f = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.inr.inr
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
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ ∏ i, ∏ j > i, ((v ∘ ⇑(swap 0 i₀)) j * (w ∘ ⇑(swap 0 i₀)) i - (v ∘ ⇑(swap 0 i₀)) i * (w ∘ ⇑(swap 0 i₀)) j) =
    ∏ i, ∏ j > i, (v ((swap 0 i₀) j) * w ((swap 0 i₀) i) - v ((swap 0 i₀) i) * w ((swap 0 i₀) j))

Tactic:
]

Goal state after:
case succ.inr.inr
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
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ ∏ i, ∏ j > i, ((v ∘ ⇑(swap 0 i₀)) j * (w ∘ ⇑(swap 0 i₀)) i - (v ∘ ⇑(swap 0 i₀)) i * (w ∘ ⇑(swap 0 i₀)) j) =
    ∏ i, ∏ j > i, (v ((swap 0 i₀) j) * w ((swap 0 i₀) i) - v ((swap 0 i₀) i) * w ((swap 0 i₀) j))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, ∑ i, (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ i * x ^ ↑i = 0
⊢ (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, ∑ i, (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ i * x ^ ↑i = 0
⊢ (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ = 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₂
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}
⊢ span R (⇑(LinearMap.fst R L₁ L₂) '' {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}) = span R (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}
⊢ span R (⇑(LinearMap.fst R L₁ L₂) '' {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}) = span R (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_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g = 0
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.degree < ↑(#s)
degree_g_lt : g.degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Tactic:
← mem_degreeLT

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

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
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.degree < ↑(#s)
degree_g_lt : g.degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Tactic:
rw [← mem_degreeLT] at degree_f_lt degree_g_lt

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
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).degree < ↑(#s)

Tactic:
← mem_degreeLT

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.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.LinearAlgebra.Lagrange

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : 0 = g
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
⊢ 0 = g

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : 0 = g
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
⊢ 0 = g
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 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₂
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}
h₃ : Submodule.map (LinearMap.fst R L₁ L₂) (span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}) = span R (Set.range b₁.h)
⊢ H₁ = H₁

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
degree_g_lt : g.degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ (f - g).degree < ↑(#s)

Tactic:
← mem_degreeLT

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g ∈ degreeLT R #s
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g ∈ degreeLT R #s

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g ∈ degreeLT R #s
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : 0 = g
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g
⊢ 0 = g

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : 0 = g
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g
⊢ 0 = g
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 * (W.submatrix succ (succAbove 0)).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

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
⊢ ∀ b ∈ univ, b ≠ 0 → (-1) ^ ↑b * W 0 b * (W.submatrix succ b.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
⊢ (-1) ^ ↑0 * W 0 0 * (W.submatrix succ (succAbove 0)).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

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
⊢ ∀ b ∈ univ, b ≠ 0 → (-1) ^ ↑b * W 0 b * (W.submatrix succ b.succAbove).det = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
⊢ ¬x = y ↔ x ≠ y

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
⊢ 1 = 1

pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0

Tactic:
]

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x : F
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x : F
⊢ 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 ι
v : ι → F
i : ι
⊢ 1 = 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 ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Lagrange.basis {j, i} v j = basisDivisor (v j) (v i)

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Lagrange.basis {j, i} v j = basisDivisor (v j) (v i)
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 : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬i = j

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬i = 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 : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j)) = 1

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j)) = 1
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 : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ 1 = 1

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

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ v i ≠ v j
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 *
      ((∏ i, (v i.succ - r * w i.succ)) * ∏ i, ∏ j > i, ((v ∘ succ) j * (w ∘ succ) i - (v ∘ succ) i * (w ∘ succ) j)) =
    ∏ i, ∏ j > i, (v j * w i - v i * w j)

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
⊢ (-1) ^ ↑0 * W 0 0 *
      ((∏ i, (v i.succ - r * w i.succ)) * ∏ i, ∏ j > i, ((v ∘ succ) j * (w ∘ succ) i - (v ∘ succ) i * (w ∘ succ) j)) =
    ∏ 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 : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ (Lagrange.basis s v i).natDegree = ∑ x ∈ s.erase i, 1

Tactic:
]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ (Lagrange.basis s v i).natDegree = ∑ x ∈ s.erase i, 1
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case e'_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
j : ι
hj : j ∈ s.erase i
⊢ ¬basisDivisor (v i) (v j) = 0

Tactic:
]

Goal state after:
case e'_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
j : ι
hj : j ∈ s.erase i
⊢ ¬basisDivisor (v i) (v j) = 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₂
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₂))
hr :
  range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
    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})
⊢ lieSpan R (↥(prod eι b₁ b₂))
      (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₂))
hr :
  range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
    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})
⊢ lieSpan R (↥(prod eι b₁ b₂))
      (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.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ↑(#s - 1) = ↑(#s - 1)

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 : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∀ b ∈ s, (Lagrange.basis s v b).degree < ↑(#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
⊢ ∀ b ∈ s, (Lagrange.basis s v b).degree < ↑(#s)