awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rhs : 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)

Tactic:
rhs
-- 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)
a₁ : ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)
a₂ : ((↑v : K)′ : K)
| HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)

Tactic:
congr
-- 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)
a₁ : fun (x : ι) ↦ (↑(c x) : K) * logDeriv (↑(u x) : K)
| ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)

Tactic:
rhs
-- 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)
x : ι
a₁ : logDeriv (↑(u x) : K)
| (↑(c x) : K) * logDeriv (↑(u x) : K)

Tactic:
rhs
-- 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)
a₁ : fun (x : ι) ↦ (↑(c x) : K) * logDeriv (↑(u x) : K)
a₂ : ∀ (x : ι), (↑(c x) : K) * logDeriv (↑(u x) : K)
a₃ : ∀ (x : ι), logDeriv (↑(u x) : K)
| ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)

Tactic:
rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
-- 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)
| ∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K)

Tactic:
· rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
-- 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)
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₂ a₃ : ((↑v : K)′ : K)
| (↑a : K) = 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)

Premises used: DifferentialAlgebra.deriv_algebraMap
-- 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)
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)
⊢ (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (↑(u x) : K) : K) ((↑v : K)′ : K)

Tactic:
conv =>
      rhs
      congr
      · rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
      · apply (deriv_algebraMap v)

Premises used: DifferentialAlgebra.deriv_algebraMap
-- 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)
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)
⊢ (↑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:
simp_rw [IsScalarTower.algebraMap_apply F B K]

Premises used: Membership.mem, Subtype, IsScalarTower.algebraMap_apply
-- 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)
norm_cast norm_cast₁ norm_cast₂ 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)
⊢ (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:
norm_cast
-- 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
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')
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)
⊢ ∃ (ι₀ : 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 (e.symm ∘ u) (e.symm v)

Premises used: AlgEquiv.symm, Function.comp, IsLiouville.isLiouville, 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
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')
⊢ 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

Premises used: AlgEquiv.symm
-- 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
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 :
  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)
⊢ (↑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:
simpa [AlgEquiv.commutes, map_add, map_sum, map_mul, logDeriv, algEquiv_deriv'] using h

Premises used: AlgEquiv.commutes, map_add, map_sum, map_mul, Differential.logDeriv, Differential.algEquiv_deriv'
-- 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
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)
⊢ CharZero K

Tactic:
haveI : CharZero K := charZero_of_injective_algebraMap
      (FaithfulSMul.algebraMap_injective F K)
-- 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
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
change : (e : (a : K) → K) (u₁ i) = u₁ i
⊢ Subtype.mk (p := fun (x : Gal(K/F)) ↦ Membership.mem (γ := Subgroup Gal(K/F)) ⊤ x) e property • u₁ i = u₁ i

Tactic:
change e (u₁ i) = u₁ i

Premises used: DFunLike.coe
-- 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
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
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))
⊢ (e : (a : K) → K) (u₁ i) = u₁ i

Tactic:
simp only [u₁, map_prod]

Premises used: map_prod
-- 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
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
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)
⊢ 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:
apply Fintype.prod_equiv (Equiv.mulLeft e)

Premises used: Fintype.prod_equiv, Equiv.mulLeft
-- 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
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
⊢ ∀ (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:
simp
-- 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
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 : ι), Membership.mem (γ := IntermediateField F K) (fixedField ⊤) (u₁ i)

Tactic:
have : ∀ i, u₁ i ∈ fixedField (⊤ : Subgroup (K ≃ₐ[F] K)) := by
      rintro i ⟨e, _⟩
      change e (u₁ i) = u₁ i
      simp only [u₁, map_prod]
      apply Fintype.prod_equiv (Equiv.mulLeft e)
      simp
-- 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
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_1 : 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)
this : ∀ (i : ι), Membership.mem (γ := IntermediateField F K) (fixedField ⊤) (u₁ i)
⊢ Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥

Tactic:
have ffb : fixedField ⊤ = ⊥ := (IsGalois.tfae.out 0 1).mp (inferInstance : IsGalois F K)
-- 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
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_1 : 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)
this : ∀ (i : ι), Membership.mem (γ := IntermediateField F K) (fixedField ⊤) (u₁ i)
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
⊢ ∀ (i : ι), ∃ (y : F), (algebraMap F K : (a : F) → K) y = u₁ i

Tactic:
simp_rw [ffb, IntermediateField.mem_bot, Set.mem_range] at this

Premises used: Set.mem_range, IntermediateField.mem_bot
-- 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
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_1 : 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)
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
this : ∀ (i : ι), ∃ (y : F), (algebraMap F K : (a : F) → K) y = u₁ i
choose :
  ∀ (u₀ : (i : ι) → F) (hu₀ : ∀ (i : ι), (algebraMap F K : (a : F) → K) (u₀ i) = u₁ i),
    ∃ (ι₀ : 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 u₀ hu₀ using this
-- 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
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)
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
u₀ : (i : ι) → F
hu₀ : ∀ (i : ι), (algebraMap F K : (a : F) → K) (u₀ i) = u₁ i
v₁ : K := HDiv.hDiv (α := K) (∑ x : Gal(K/F), (x : (a : K) → K) v) (↑(Fintype.card.{u_2} Gal(K/F)) : K)
e : Gal(K/F)
property : Membership.mem (γ := Subgroup Gal(K/F)) ⊤ e
change : (e : (a : K) → K) v₁ = v₁
⊢ Subtype.mk (p := fun (x : Gal(K/F)) ↦ Membership.mem (γ := Subgroup Gal(K/F)) ⊤ x) e property • v₁ = v₁

Tactic:
change e v₁ = v₁

Premises used: DFunLike.coe
-- 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
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)
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
u₀ : (i : ι) → F
hu₀ : ∀ (i : ι), (algebraMap F K : (a : F) → K) (u₀ i) = u₁ i
v₁ : K := HDiv.hDiv (α := K) (∑ x : Gal(K/F), (x : (a : K) → K) v) (↑(Fintype.card.{u_2} Gal(K/F)) : K)
e : Gal(K/F)
property : Membership.mem (γ := Subgroup Gal(K/F)) ⊤ e
simp :
  HDiv.hDiv (α := K) (∑ x : Gal(K/F), (e : (a : K) → K) ((x : (a : K) → K) v : K))
      (↑(Fintype.card.{u_2} Gal(K/F)) : K) =
    HDiv.hDiv (α := K) (∑ x : Gal(K/F), (x : (a : K) → K) v) (↑(Fintype.card.{u_2} Gal(K/F)) : K)
⊢ (e : (a : K) → K) v₁ = v₁

Tactic:
simp only [v₁, map_div₀, map_sum, map_natCast]

Premises used: map_sum, map_div₀, map_natCast