awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ 0 < natDegree (minpoly F x)

Tactic:
have : 0 < (minpoly F x).natDegree := Irreducible.natDegree_pos
      (minpoly.irreducible (Algebra.IsIntegral.isIntegral _))
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < natDegree (minpoly F x)
a₁ : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) (0 : F[X])
a₂ : natDegree.{u_2} (R := F) ((derivative : (a : F[X]) → F[X]) (minpoly F x)) < natDegree (minpoly F x)
⊢ ¬Dvd.dvd (α := F[X]) (minpoly F x) ((derivative : (a : F[X]) → F[X]) (minpoly F x))

Tactic:
apply not_dvd_of_natDegree_lt

Premises used: Polynomial.not_dvd_of_natDegree_lt
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < natDegree (minpoly F x)
nh : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) (0 : F[X])
⊢ False

Tactic:
simp [natDegree_eq_zero_of_derivative_eq_zero nh] at this

Premises used: Polynomial.natDegree_eq_zero_of_derivative_eq_zero
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < natDegree (minpoly F x)
a₁ : natDegree (minpoly F x) ≠ 0
⊢ natDegree.{u_2} (R := F) ((derivative : (a : F[X]) → F[X]) (minpoly F x)) < natDegree (minpoly F x)

Tactic:
apply natDegree_derivative_lt

Premises used: Polynomial.natDegree_derivative_lt
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < natDegree (minpoly F x)
⊢ natDegree (minpoly F x) ≠ 0

Tactic:
Nat.ne_zero_of_lt this

Premises used: Nat.ne_zero_of_lt
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < natDegree (minpoly F x)
⊢ natDegree (minpoly F x) ≠ 0

Tactic:
exact Nat.ne_zero_of_lt this

Premises used: Nat.ne_zero_of_lt
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
B : IntermediateField F K
inst_7 : FiniteDimensional.{u_2, u_3} F ↥B
⊢ DifferentialAlgebra.{u_2, u_3} F ↥B

Tactic:
differentialAlgebraFiniteDimensional

Premises used: Set.Mem, setOf, Differential.differentialAlgebraFiniteDimensional
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : Differential K
inst_8 : DifferentialAlgebra F K
B : IntermediateField F K
inst_9 : FiniteDimensional.{u_2, u_3} F ↥B
a : ↥B
change : Eq (α := K) (((B.val : (a : ↥B) → K) a : K)′ : K) ((B.val : (a : ↥B) → K) (a′ : ↥B) : K)
⊢ Eq (α := K) (((algebraMap (↥B) K : (a : ↥B) → K) a : K)′ : K) ((algebraMap (↥B) K : (a : ↥B) → K) (a′ : ↥B) : K)

Tactic:
change (B.val a)′ = B.val a′

Premises used: Differential.deriv, IntermediateField.val, DFunLike.coe
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : Differential K
inst_8 : DifferentialAlgebra F K
B : IntermediateField F K
inst_9 : FiniteDimensional.{u_2, u_3} F ↥B
a : ↥B
hf : Function.Injective (α := ↥B) (β := K) (⇑B.val : (a : ↥B) → K)
⊢ Eq (α := K) (((B.val : (a : ↥B) → K) a : K)′ : K) ((B.val : (a : ↥B) → K) (a′ : ↥B) : K)

Tactic:
rw [algHom_deriv']

Premises used: Differential.algHom_deriv'
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : Differential K
inst_8 : DifferentialAlgebra F K
B : IntermediateField F K
inst_9 : FiniteDimensional.{u_2, u_3} F ↥B
a : ↥B
⊢ Function.Injective (α := ↥B) (β := K) (⇑B.val : (a : ↥B) → K)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : Differential K
inst_8 : DifferentialAlgebra F K
B : IntermediateField F K
inst_9 : FiniteDimensional.{u_2, u_3} F ↥B
a : ↥B
⊢ Function.Injective (α := ↥B) (β := K) (⇑B.val : (a : ↥B) → K)

Tactic:
exact Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
x : ι
⊢ Eq.{u_2 + 1} (α := K) (((Algebra.cast ∘ c) x)′ : K) (0 : K)

Tactic:
simp only [Function.comp_apply, ← coe_deriv, coe_eq_zero_iff, hc]

Premises used: algebraMap.coe_eq_zero_iff, algebraMap.coe_deriv, Function.comp_apply
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
⊢ (↑(↑a : K) : A) =
    HAdd.hAdd (α := A) (β := A)
      (∑ x : ι, HMul.hMul (α := A) (↑((Algebra.cast ∘ c) x) : A) (logDeriv (((fun (x : A) ↦ x) ∘ u) x)) : A) (v′ : A)

Tactic:
simpa only [Function.comp_apply, ← IsScalarTower.algebraMap_apply]

Premises used: Function.comp_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
obtain :
  ∀ (ι₀ : Type) (w : Fintype ι₀) (c₀ : ι₀ → K) (hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀ x)′ : K) (0 : K)) (u₀ : ι₀ → K)
    (v₀ : K) (h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : K) (v₀′ : K)),
    ∃ (ι₀ : Type) (x : Fintype ι₀) (c₀ : ι₀ → F) (_ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)) (u₀ : ι₀ → F) (v₀ :
      F), a = HAdd.hAdd (α := F) (β := F) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)
⊢ ∃ (ι₀ : Type) (x : Fintype ι₀) (c₀ : ι₀ → F) (_ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)) (u₀ : ι₀ → F) (v₀ :
    F), a = HAdd.hAdd (α := F) (β := F) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)

Tactic:
obtain ⟨ι₀, _, c₀, hc₀, u₀, v₀, h₀⟩ := inst2.isLiouville (a : K) ι
        ((↑) ∘ c)
        (fun _ ↦ by simp only [Function.comp_apply, ← coe_deriv, coe_eq_zero_iff, hc])
        ((↑) ∘ u) v (by simpa only [Function.comp_apply, ← IsScalarTower.algebraMap_apply])

Premises used: Algebra.cast, Function.comp, IsLiouville.isLiouville
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀ : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀ x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : K) (v₀′ : K)
⊢ ∀ (x : ι₀), Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F K)) (c₀ x)

Tactic:
have hc (x : ι₀) := mem_range_of_deriv_eq_zero F (hc₀ x)
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀ : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀ x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : K) (v₀′ : K)
hc : ∀ (x : ι₀), Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F K)) (c₀ x)
choose :
  ∀ (c₀_1 : (x : ι₀) → F) (hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀_1 x) = c₀ x),
    ∃ (ι₀ : Type) (x : Fintype ι₀) (c₀ : ι₀ → F) (_ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)) (u₀ : ι₀ → F) (v₀ :
      F), a = HAdd.hAdd (α := F) (β := F) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)
⊢ ∃ (ι₀ : Type) (x : Fintype ι₀) (c₀ : ι₀ → F) (_ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)) (u₀ : ι₀ → F) (v₀ :
    F), a = HAdd.hAdd (α := F) (β := F) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)

Tactic:
choose c₀ hc using hc
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
apply : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, (↑(c₀ x) : K) * logDeriv (u₀ x) : K) (v₀′ : K)
apply₁ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)
⊢ ∃ (ι₀ : Type) (x : Fintype ι₀) (c₀ : ι₀ → F) (_ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)) (u₀ : ι₀ → F) (v₀ :
    F), a = HAdd.hAdd (α := F) (β := F) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)

Tactic:
apply inst1.isLiouville a ι₀ c₀ _ u₀ v₀

Premises used: IsLiouville.isLiouville
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
rw :
  HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K) =
    HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, (↑(c₀ x) : K) * logDeriv (u₀ x) : K) (v₀′ : K)
⊢ (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, (↑(c₀ x) : K) * logDeriv (u₀ x) : K) (v₀′ : K)

Tactic:
rw [h₀]
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
⊢ HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K) =
    HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, (↑(c₀ x) : K) * logDeriv (u₀ x) : K) (v₀′ : K)

Tactic:
simp [hc]
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
x : ι₀
apply_fun : Eq.{u_2 + 1} (α := K) (↑((c₀ x)′ : F) : K) (↑0 : K)
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F) (β := K) Algebra.cast
⊢ Eq (α := F) ((c₀ x)′ : F) (0 : F)

Tactic:
apply_fun ((↑) : F → K)

Premises used: Algebra.cast
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
x : ι₀
simp : Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) (↑((c₀ x)′ : F) : K) (↑0 : K)

Tactic:
simp only [coe_deriv, hc, algebraMap.coe_zero]

Premises used: algebraMap.coe_deriv, algebraMap.coe_zero
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
x : ι₀
⊢ Eq (α := K) ((c₀_1 x)′ : K) (0 : K)

Tactic:
apply hc₀
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
x : ι₀
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F) (β := K) Algebra.cast

Tactic:
apply FaithfulSMul.algebraMap_injective

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst_1 : Field F
inst_2 : Field K
inst_3 : Differential F
inst_4 : Differential K
inst_5 : Algebra F K
inst_6 : DifferentialAlgebra F K
inst_7 : CharZero F
B : IntermediateField F K
inst_8 : FiniteDimensional.{u_1, u_2} F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → ↥B
v : ↥B
h : (↑a : ↥B) = HAdd.hAdd (α := ↥B) (β := ↥B) (∑ x : ι, (↑(c x) : ↥B) * logDeriv (u x) : ↥B) (v′ : ↥B)
apply :
  (↑a : K) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (((⇑B.val : (a : ↥B) → K) ∘ u) x)) : K)
      (((B.val : (a : ↥B) → K) v : K)′ : K)
⊢ ∃ (ι₀ : Type) (x : Fintype ι₀) (c₀ : ι₀ → F) (_ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)) (u₀ : ι₀ → F) (v₀ :
    F), a = HAdd.hAdd (α := F) (β := F) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)

Tactic:
apply inst.isLiouville a ι c hc (B.val ∘ u) (B.val v)

Premises used: Function.comp, IsLiouville.isLiouville, IntermediateField.val, DFunLike.coe
-- Module: Mathlib.FieldTheory.Differential.Liouville
Goal:
F : Type u_1
K : Type u_2
inst_1 : Field F
inst_2 : Field K
inst_3 : Differential F
inst_4 : Differential K
inst_5 : Algebra F K
inst_6 : DifferentialAlgebra F K
inst_7 : CharZero F
B : IntermediateField F K
inst_8 : FiniteDimensional.{u_1, u_2} F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → ↥B
v : ↥B
h : (↑a : ↥B) = HAdd.hAdd (α := ↥B) (β := ↥B) (∑ x : ι, (↑(c x) : ↥B) * logDeriv (u x) : ↥B) (v′ : ↥B)
dsimp : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
⊢ (↑a : K) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (((⇑B.val : (a : ↥B) → K) ∘ u) x)) : K)
      (((B.val : (a : ↥B) → K) v : K)′ : K)

Tactic:
dsimp only [coe_val, Function.comp_apply]

Premises used: IntermediateField.coe_val, Function.comp_apply