awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
refine_2 :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (∑ i : ι, HMul.hMul (α := K) (↑(c i) : K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i))))
        (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′) /
      (↑(Fintype.card.{u_2} Gal(K/F)) : K)
⊢ (algebraMap F K : (a : F) → K) a =
    ∑ x : ι,
        HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x))) /
          (↑(Fintype.card.{u_2} Gal(K/F)) : K) +
      HDiv.hDiv (α := K) (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′) (↑(Fintype.card.{u_2} Gal(K/F)) : K)

Tactic:
rw [← sum_div, ← add_div]

Premises used: Finset.sum_div, add_div
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
refine_2 :
  HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    HAdd.hAdd (α := K)
      (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x))))
      (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)
⊢ (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (∑ i : ι, HMul.hMul (α := K) (↑(c i) : K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i))))
        (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′) /
      (↑(Fintype.card.{u_2} Gal(K/F)) : K)

Tactic:
field_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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
h₁ : ∀ (i : ι), logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i))
| HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    HAdd.hAdd (α := K)
      (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x))))
      (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)

Tactic:
enter [2, 1, 2, i, 2]
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
i : ι
pos :
  ∀ (h : u i = 0),
    Eq.{u_2 + 1} (α := K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i)))
      (∑ x : Gal(K/F), logDeriv ((x : (a : K) → K) (u i)))
neg :
  ∀ (h : ¬u i = 0),
    Eq.{u_2 + 1} (α := K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i)))
      (∑ x : Gal(K/F), logDeriv ((x : (a : K) → K) (u i)))
⊢ Eq.{u_2 + 1} (α := K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i)))
    (∑ x : Gal(K/F), logDeriv ((x : (a : K) → K) (u i)))

Tactic:
by_cases h : u i = 0
-- 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_1 : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (u x) : K) (v′ : K)
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
i : ι
h : u i = 0
⊢ Eq.{u_2 + 1} (α := K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i)))
    (∑ x : Gal(K/F), logDeriv ((x : (a : K) → K) (u i)))

Tactic:
simp [logDeriv_prod, h]

Premises used: Differential.logDeriv_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_1 : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (u x) : K) (v′ : K)
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
i : ι
h : ¬u i = 0
⊢ Eq.{u_2 + 1} (α := K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i)))
    (∑ x : Gal(K/F), logDeriv ((x : (a : K) → K) (u i)))

Tactic:
simp [logDeriv_prod, h]

Premises used: Differential.logDeriv_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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
enter :
  HAdd.hAdd (α := K) (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x))))
    (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)
enter₁ : ∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)))
enter₂ : fun (x : ι) ↦ HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)))
h₁ : ∀ (i : ι), HMul.hMul (α := K) (↑(c i) : K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i)))
h₂ : ∀ (i : ι), logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i))
| HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    HAdd.hAdd (α := K)
      (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x))))
      (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)

Tactic:
enter [2, 1, 2, i, 2]
        equals ∑ x : K ≃ₐ[F] K, logDeriv (x (u i)) =>
          by_cases h : u i = 0 <;>
          simp [logDeriv_prod, h]

Premises used: Differential.logDeriv_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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
refine_2 :
  HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    HAdd.hAdd (α := K) (∑ i : ι, HMul.hMul (α := K) (↑(c i) : K) (∑ x : Gal(K/F), logDeriv ((x : (a : K) → K) (u i))))
      (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    HAdd.hAdd (α := K)
      (∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x))))
      (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)

Tactic:
conv =>
        enter [2, 1, 2, i, 2]
        equals ∑ x : K ≃ₐ[F] K, logDeriv (x (u i)) =>
          by_cases h : u i = 0 <;>
          simp [logDeriv_prod, h]

Premises used: Differential.logDeriv_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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
refine_2 :
  HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    HAdd.hAdd (α := K)
      (∑ x : ι, ∑ i : Gal(K/F), HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((i : (a : K) → K) (u x)) : K))
      (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    HAdd.hAdd (α := K) (∑ i : ι, HMul.hMul (α := K) (↑(c i) : K) (∑ x : Gal(K/F), logDeriv ((x : (a : K) → K) (u i))))
      (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)

Tactic:
simp_rw [mul_sum]

Premises used: Finset.mul_sum
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
refine_2 :
  HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    ∑ x : Gal(K/F),
      HAdd.hAdd (α := K) (β := K)
        (∑ x_1 : ι, HMul.hMul (α := K) (β := K) ((↑(c x_1) : K) : K) (logDeriv ((x : (a : K) → K) (u x_1)) : K) : K)
        (((x : (a : K) → K) v : K)′ : K)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    HAdd.hAdd (α := K)
      (∑ x : ι, ∑ i : Gal(K/F), HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((i : (a : K) → K) (u x)) : K))
      (∑ x : Gal(K/F), ((x : (a : K) → K) v : K)′)

Tactic:
rw [sum_comm, ← sum_add_distrib]

Premises used: Finset.sum_add_distrib, Finset.sum_comm
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
trans :
  HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    ∑ x : Gal(K/F), (↑a : K)
trans₁ :
  Eq.{u_2 + 1} (α := K) (∑ x : Gal(K/F), (↑a : K))
    (∑ x : Gal(K/F),
      HAdd.hAdd (α := K) (β := K)
        (∑ x_1 : ι, HMul.hMul (α := K) (β := K) ((↑(c x_1) : K) : K) (logDeriv ((x : (a : K) → K) (u x_1)) : K) : K)
        (((x : (a : K) → K) v : K)′ : K))
⊢ HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    ∑ x : Gal(K/F),
      HAdd.hAdd (α := K) (β := K)
        (∑ x_1 : ι, HMul.hMul (α := K) (β := K) ((↑(c x_1) : K) : K) (logDeriv ((x : (a : K) → K) (u x_1)) : K) : K)
        (((x : (a : K) → K) v : K)′ : K)

Tactic:
trans ∑ _ : (K ≃ₐ[F] K), a

Premises used: AlgEquiv
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
⊢ HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) a : K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K) =
    ∑ x : Gal(K/F), (↑a : K)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e_f :
  ∀ (e : Gal(K/F)),
    (↑a : K) =
      HAdd.hAdd (α := K) (β := K)
        (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K) : K)
        (((e : (a : K) → K) v : K)′ : K)
⊢ Eq.{u_2 + 1} (α := K) (∑ x : Gal(K/F), (↑a : K))
    (∑ x : Gal(K/F),
      HAdd.hAdd (α := K) (β := K)
        (∑ x_1 : ι, HMul.hMul (α := K) (β := K) ((↑(c x_1) : K) : K) (logDeriv ((x : (a : K) → K) (u x_1)) : K) : K)
        (((x : (a : K) → K) v : K)′ : K))

Tactic:
rcongr e
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
⊢ Eq (α := K) ((e : (a : K) → K) (↑a : K) : K)
    ((e : (a : K) → K) (HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (u x) : K) (v′ : K)) : K)

Tactic:
apply_fun e at 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
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
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  Eq (α := K) ((e : (a : K) → K) (↑a : K) : K)
    ((e : (a : K) → K) (HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (u x) : K) (v′ : K)) : K)
⊢ (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)

Tactic:
simp only [AlgEquiv.commutes, map_add, map_sum, map_mul] at h

Premises used: AlgEquiv.commutes, map_add, map_sum, map_mul
-- 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
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
⊢ (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)

Tactic:
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
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
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
h₁ :
  Eq.{u_2 + 1} (α := K)
    (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K))
    (∑ x : ι,
      HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K) ((e : (a : K) → K) (logDeriv (u x)) : K))
h₂ : Eq (α := K) (((e : (a : K) → K) v : K)′ : K) ((e : (a : K) → K) (v′ : K) : K)
⊢ (↑a : K) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K) : K)
      (((e : (a : K) → K) v : K)′ : K)

Tactic:
convert! h using 2
-- 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
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
h₁ : ∀ (x : ι), Eq (α := K) (logDeriv ((e : (a : K) → K) (u x)) : K) ((e : (a : K) → K) (logDeriv (u x)) : K)
⊢ Eq.{u_2 + 1} (α := K)
    (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K))
    (∑ x : ι,
      HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K) ((e : (a : K) → K) (logDeriv (u x)) : K))

Tactic:
rcongr 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
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
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
x : ι
⊢ Eq (α := K) (logDeriv ((e : (a : K) → K) (u x)) : K) ((e : (a : K) → K) (logDeriv (u x)) : K)

Tactic:
simp [logDeriv, algEquiv_deriv']

Premises used: 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
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
h₁ h₂ : Eq (α := K) (((e : (a : K) → K) v : K)′ : K) (((e : (a : K) → K) v : K)′ : K)
⊢ Eq (α := K) (((e : (a : K) → K) v : K)′ : K) ((e : (a : K) → K) (v′ : K) : K)

Tactic:
rw [algEquiv_deriv']

Premises used: 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
⊢ IsLiouville F K

Tactic:
let map := IsAlgClosed.lift (M := AlgebraicClosure F) (R := F) (S := K)
  let K' := map.fieldRange
  have : FiniteDimensional F K' :=
    LinearMap.finiteDimensional_range map.toLinearMap
  let K'' := normalClosure F K' (AlgebraicClosure F)
  let B : IntermediateField F K'' := IntermediateField.restrict
    (F := K') (IntermediateField.le_normalClosure ..)
  have kequiv : K ≃ₐ[F] ↥B := (show K ≃ₐ[F] K' from AlgEquiv.ofInjectiveField map).trans
    (IntermediateField.restrict_algEquiv _)
  IsLiouville.equiv kequiv.symm

Premises used: AlgHom.toLinearMap, AlgEquiv.ofInjectiveField, AlgEquiv.symm, IntermediateField.normalClosure, Membership.mem, Subtype, IsAlgClosed.lift, AlgHom.fieldRange, AlgEquiv.trans, IntermediateField.restrict, IsLiouville.equiv, AlgebraicClosure, IntermediateField.le_normalClosure, LinearMap.finiteDimensional_range, IntermediateField.restrict_algEquiv
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : Lifts F E K
⊢ ∀ (x : ↥L.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L.emb : (a : ↥L.carrier) → K) ((inclusion ⋯ : (a : ↥L.carrier) → ↥L.carrier) x : ↥L.carrier) : K)
      ((L.emb : (a : ↥L.carrier) → K) x : K)

Tactic:
simp