mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case cons.ha
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ f a✝ ≠ 0

pp: case hb
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ (Multiset.map f s✝).prod ≠ 0

Tactic:
·

Goal state after:
case cons.ha
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ f a✝ ≠ 0
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case hb
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ (Multiset.map f s✝).prod ≠ 0

Tactic:
·

Goal state after:
case hb
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ (Multiset.map f s✝).prod ≠ 0
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ ∀ x ∈ s✝, f x ≠ 0

Tactic:
·

Goal state after:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ ∀ x ∈ s✝, f x ≠ 0
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case h.h0
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
this : 0 < p.natDegree
⊢ derivative p ≠ 0

pp: case hl
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
this : 0 < p.natDegree
⊢ (derivative p).natDegree < p.natDegree

Tactic:
·

Goal state after:
case h.h0
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
this : 0 < p.natDegree
⊢ derivative p ≠ 0
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Fintype (Extension k p n)
⊢ Nat.card k ^ n = Fintype.card (Extension k p n)

Tactic:
·

Goal state after:
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Fintype (Extension k p n)
⊢ Nat.card k ^ n = Fintype.card (Extension k p n)
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′ =
    (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′

pp: case inj
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Function.Injective fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′ =
    (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
h : f ∣ X ^ Nat.card k ^ 0 - X
⊢ f.natDegree ∣ 0

pp: case inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
⊢ f.natDegree ∣ n

Tactic:
·

Goal state after:
case inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
h : f ∣ X ^ Nat.card k ^ 0 - X
⊢ f.natDegree ∣ 0
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n

pp: case inr.inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
⊢ f.natDegree ∣ n

Tactic:
·

Goal state after:
case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case inj
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Function.Injective fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1

Tactic:
·

Goal state after:
case inj
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Function.Injective fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inr.inl.refine_1
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ (Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X)).Splits

pp: case inr.inl.refine_2
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X) ≠ 0

Tactic:
·

Goal state after:
case inr.inl.refine_1
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ (Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X)).Splits
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inr.inl.refine_2
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X) ≠ 0

Tactic:
·

Goal state after:
case inr.inl.refine_2
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X) ≠ 0
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case inj.h0
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ derivative (minpoly F x) ≠ 0

pp: case hl
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ (derivative (minpoly F x)).natDegree < (minpoly F x).natDegree

Tactic:
·

Goal state after:
case inj.h0
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ derivative (minpoly F x) ≠ 0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (a : ZMod p), (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)

pp: case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = (expand p) (p_1 + q)

pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)

Tactic:
·

Goal state after:
case C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (a : ZMod p), (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = (expand p) (p_1 + q)

pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)

Tactic:
·

Goal state after:
case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = (expand p) (p_1 + q)
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)

Tactic:
·

Goal state after:
case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ (X s).degrees ∪ 0 ≤ {s}

Tactic:
Multiset.union_zero

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ (X s).degrees ≤ {s}
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x, (Fintype.card K - 1) * Multiset.count n {x} = ?m.62

pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ?m.62 = Fintype.card K - 1

pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ℕ

Tactic:
·

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x, (Fintype.card K - 1) * Multiset.count n {x} = ?m.62
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∀ b ∈ Finset.univ, b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0

pp: case refine_2
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ n ∉ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∀ b ∈ Finset.univ, b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ↑a = ∑ x, ↑(c₀ x) * logDeriv (u₀ x) + v₀′

pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ∀ (x : ι₀), (c₀ x)′ = 0

Tactic:
·

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ↑a = ∑ x, ↑(c₀ x) * logDeriv (u₀ x) + v₀′
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case refine_2
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ n ∉ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ n ∉ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1

Tactic:
·

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ∀ (x : ι₀), (c₀ x)′ = 0

Tactic:
·

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ∀ (x : ι₀), (c₀ x)′ = 0
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ ↑(c₀ x✝)′ = ↑0

pp: case inj
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ Function.Injective Algebra.cast

Tactic:
·

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ ↑(c₀ x✝)′ = ↑0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro.refine_1
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∑ n, e n • indicator n ∈ restrictDegree σ K (Fintype.card K - 1)

pp: case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ (evalₗ K σ) (∑ n, e n • indicator n) = e

Tactic:
·

Goal state after:
case intro.refine_1
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∑ n, e n • indicator n ∈ restrictDegree σ K (Fintype.card K - 1)
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ (evalₗ K σ) (∑ n, e n • indicator n) = e

Tactic:
·

Goal state after:
case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ (evalₗ K σ) (∑ n, e n • indicator n) = e