awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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 (α := F) ((c₀ x)′ : F) (0 : F)
have apply_fun : Eq.{u_2 + 1} (α := K) (↑((c₀ x)′ : F) : K) (↑0 : K)
Tactic: apply_fun ((↑) : F → K)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
⊢ Eq (α := F) ((c₀ x)′ : F) (0 : F)
have inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F) (β := K) Algebra.cast
Tactic: apply_fun ((↑) : F → K)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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.{u_2 + 1} (α := K) (↑((c₀ x)′ : F) : K) (↑0 : K)
have simp : Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
Tactic: simp only [coe_deriv, hc, algebraMap.coe_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
⊢ ∃ (ι₀ : 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)
have 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)
Tactic: apply inst.isLiouville a ι c hc (B.val ∘ u) (B.val v)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
⊢ (↑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)
have dsimp : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
Tactic: dsimp only [coe_val, Function.comp_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
| (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
have rhs : HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
Tactic: rhs
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
| HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
have a₁ : ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
a₁ : ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
| HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
have a₂ : ((↑v : K)′ : K)
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
| ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
have a₁ : fun (x : ι) ↦ (↑(c x) : K) * logDeriv (↑(u x) : K)
Tactic: rhs
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
x : ι
| (↑(c x) : K) * logDeriv (↑(u x) : K)
have a₁ : logDeriv (↑(u x) : K)
Tactic: rhs
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
| ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
have a₁ : fun (x : ι) ↦ (↑(c x) : K) * logDeriv (↑(u x) : K)
Tactic: rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
a₁ : fun (x : ι) ↦ (↑(c x) : K) * logDeriv (↑(u x) : K)
| ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
have a₂ : ∀ (x : ι), (↑(c x) : K) * logDeriv (↑(u x) : K)
Tactic: rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
a₁ : fun (x : ι) ↦ (↑(c x) : K) * logDeriv (↑(u x) : K)
a₂ : ∀ (x : ι), (↑(c x) : K) * logDeriv (↑(u x) : K)
| ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
have a₃ : ∀ (x : ι), logDeriv (↑(u x) : K)
Tactic: rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
| (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
have intro : HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
Tactic: rhs
      congr
      · rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
      · apply (deriv_algebraMap v)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
intro : HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
| (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
have a₁ : ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
Tactic: rhs
      congr
      · rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
      · apply (deriv_algebraMap v)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
intro : HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
a₁ : ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
| (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
have a₂ : ((↑v : K)′ : K)
Tactic: rhs
      congr
      · rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
      · apply (deriv_algebraMap v)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
⊢ (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)
have conv : (↑a : K) =
  HAdd.hAdd (α := K) (β := K)
    (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) ((algebraMap (↥B) K : (a : ↥B) → K) (logDeriv (u x)) : K) :
      K)
    ((algebraMap (↥B) K : (a : ↥B) → K) (v′ : ↥B) : K)
Tactic: conv =>
      rhs
      congr
      · rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
      · apply (deriv_algebraMap v)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
⊢ (↑a : K) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) ((algebraMap (↥B) K : (a : ↥B) → K) (logDeriv (u x)) : K) :
        K)
      ((algebraMap (↥B) K : (a : ↥B) → K) (v′ : ↥B) : K)
have simp_rw : (algebraMap (↥B) K : (a : ↥B) → K) ((algebraMap F ↥B : (a : F) → ↥B) a : ↥B) =
  HAdd.hAdd (α := K) (β := K)
    (∑ x : ι,
        HMul.hMul (α := K) (β := K)
          ((algebraMap (↥B) K : (a : ↥B) → K) ((algebraMap F ↥B : (a : F) → ↥B) (c x) : ↥B) : K)
          ((algebraMap (↥B) K : (a : ↥B) → K) (logDeriv (u x)) : K) :
      K)
    ((algebraMap (↥B) K : (a : ↥B) → K) (v′ : ↥B) : K)
Tactic: simp_rw [IsScalarTower.algebraMap_apply F B K]
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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)
⊢ (algebraMap (↥B) K : (a : ↥B) → K) ((algebraMap F ↥B : (a : F) → ↥B) a : ↥B) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K)
            ((algebraMap (↥B) K : (a : ↥B) → K) ((algebraMap F ↥B : (a : F) → ↥B) (c x) : ↥B) : K)
            ((algebraMap (↥B) K : (a : ↥B) → K) (logDeriv (u x)) : K) :
        K)
      ((algebraMap (↥B) K : (a : ↥B) → K) (v′ : ↥B) : K)
have norm_cast : (algebraMap F ↥B : (a : F) → ↥B) a =
  HAdd.hAdd (α := ↥B) (β := ↥B)
    (∑ i : ι, HMul.hMul (α := ↥B) ((algebraMap F ↥B : (a : F) → ↥B) (c i) : ↥B) (logDeriv (u i)) : ↥B) (v′ : ↥B)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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
K' : Type u_3
inst_8 : Field K'
inst_9 : Differential K'
inst_10 : Algebra F K'
inst_11 : DifferentialAlgebra F K'
inst_12 : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst_13 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K'
v : K'
h : (↑a : K') = HAdd.hAdd (α := K') (β := K') (∑ x : ι, (↑(c x) : K') * 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)
have apply : (↑a : K) =
  HAdd.hAdd (α := K) (β := K)
    (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (((⇑e.symm : (a : K') → K) ∘ u) x)) : K)
    (((e.symm : (a : K') → K) v : K)′ : K)
Tactic: apply inst.isLiouville a ι c hc (e.symm ∘ u) (e.symm v)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (hypothesis)
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
K' : Type u_3
inst_8 : Field K'
inst_9 : Differential K'
inst_10 : Algebra F K'
inst_11 : DifferentialAlgebra F K'
inst_12 : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst_13 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K'
v : K'
h : (↑a : K') = HAdd.hAdd (α := K') (β := K') (∑ x : ι, (↑(c x) : K') * logDeriv (u x) : K') (v′ : K')
⊢ (↑a : K) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (((⇑e.symm : (a : K') → K) ∘ u) x)) : K)
      (((e.symm : (a : K') → K) v : K)′ : K)
have h₁ : Eq.{u_2 + 1} (α := K) ((e.symm : (a : K') → K) (↑a : K') : K)
  ((e.symm : (a : K') → K) (HAdd.hAdd (α := K') (β := K') (∑ x : ι, (↑(c x) : K') * logDeriv (u x) : K') (v′ : K')) : K)
Tactic: apply_fun e.symm at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (hypothesis)
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
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
h : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * 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)
have this : CharZero K
Tactic: haveI : CharZero K := charZero_of_injective_algebraMap
      (FaithfulSMul.algebraMap_injective F K)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
h : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (u x) : K) (v′ : K)
this : CharZero K
c₀ : (i : ι) → F := fun (i : ι) ↦ c i / (↑(Fintype.card.{u_2} Gal(K/F)) : F)
u₁ : (i : ι) → K := fun (i : ι) ↦ ∏ x : Gal(K/F), (x : (a : K) → K) (u i)
i : ι
e : Gal(K/F)
property : Membership.mem (γ := Subgroup Gal(K/F)) ⊤ e
⊢ Subtype.mk (p := fun (x : Gal(K/F)) ↦ Membership.mem (γ := Subgroup Gal(K/F)) ⊤ x) e property • u₁ i = u₁ i
have change : (e : (a : K) → K) (u₁ i) = u₁ i
Tactic: change e (u₁ i) = u₁ i
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
h : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (u x) : K) (v′ : K)
this : CharZero K
c₀ : (i : ι) → F := fun (i : ι) ↦ c i / (↑(Fintype.card.{u_2} Gal(K/F)) : F)
u₁ : (i : ι) → K := fun (i : ι) ↦ ∏ x : Gal(K/F), (x : (a : K) → K) (u i)
i : ι
e : Gal(K/F)
property : Membership.mem (γ := Subgroup Gal(K/F)) ⊤ e
⊢ (e : (a : K) → K) (u₁ i) = u₁ i
have simp : Eq.{u_2 + 1} (α := K) (∏ x : Gal(K/F), (e : (a : K) → K) ((x : (a : K) → K) (u i) : K))
  (∏ x : Gal(K/F), (x : (a : K) → K) (u i))
Tactic: simp only [u₁, map_prod]
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
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
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
h : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (u x) : K) (v′ : K)
this : CharZero K
c₀ : (i : ι) → F := fun (i : ι) ↦ c i / (↑(Fintype.card.{u_2} Gal(K/F)) : F)
u₁ : (i : ι) → K := fun (i : ι) ↦ ∏ x : Gal(K/F), (x : (a : K) → K) (u i)
i : ι
e : Gal(K/F)
property : Membership.mem (γ := Subgroup Gal(K/F)) ⊤ e
⊢ Eq.{u_2 + 1} (α := K) (∏ x : Gal(K/F), (e : (a : K) → K) ((x : (a : K) → K) (u i) : K))
    (∏ x : Gal(K/F), (x : (a : K) → K) (u i))
have h₁ : ∀ (x : Gal(K/F)),
  Eq (α := K) ((e : (a : K) → K) ((x : (a : K) → K) (u i) : K) : K)
    ((((Equiv.mulLeft e : (a : Gal(K/F)) → Gal(K/F)) x : Gal(K/F)) : (a : K) → K) (u i) : K)
Tactic: apply Fintype.prod_equiv (Equiv.mulLeft e)