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
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
e_a :
  Eq.{u_2 + 1} (α := K) (∑ x : Gal(K/F), (e : (a : K) → K) ((x : (a : K) → K) v : K))
    (∑ x : Gal(K/F), (x : (a : K) → K) v)
⊢ 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)

Tactic:
congr 1
-- 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
e_a :
  ∀ (x : Gal(K/F)),
    Eq (α := K) ((e : (a : K) → K) ((x : (a : K) → K) v : K) : K)
      ((((Equiv.mulLeft e : (a : Gal(K/F)) → Gal(K/F)) x : Gal(K/F)) : (a : K) → K) v : K)
⊢ Eq.{u_2 + 1} (α := K) (∑ x : Gal(K/F), (e : (a : K) → K) ((x : (a : K) → K) v : K))
    (∑ x : Gal(K/F), (x : (a : K) → K) v)

Tactic:
apply Fintype.sum_equiv (Equiv.mulLeft e)

Premises used: Equiv.mulLeft, Fintype.sum_equiv
-- 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
⊢ ∀ (x : Gal(K/F)),
    Eq (α := K) ((e : (a : K) → K) ((x : (a : K) → K) v : K) : K)
      ((((Equiv.mulLeft e : (a : Gal(K/F)) → Gal(K/F)) x : Gal(K/F)) : (a : K) → K) v : 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)
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)
⊢ Membership.mem (γ := IntermediateField F K) (fixedField ⊤) v₁

Tactic:
have : v₁ ∈ fixedField (⊤ : Subgroup (K ≃ₐ[F] K)) := by
      rintro ⟨e, _⟩
      change e v₁ = v₁
      simp only [v₁, map_div₀, map_sum, map_natCast]
      congr 1
      apply Fintype.sum_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)
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)
this : Membership.mem (γ := IntermediateField F K) (fixedField ⊤) v₁
⊢ Membership.mem (γ := Set K) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F K) : (a : F) → K)) v₁

Tactic:
rw [ffb, IntermediateField.mem_bot] at this

Premises used: 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 ⊤) ⊥
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)
this : Membership.mem (γ := Set K) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F K) : (a : F) → K)) v₁
obtain :
  ∀ (v₀ : F) (hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁),
    ∃ (ι₀ : 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 ⟨v₀, hv₀⟩ := 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)
v₀ : F
hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁
refine_1 : ∀ (x : ι), Eq (α := F) ((c₀ x)′ : F) (0 : F)
refine_2 : 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:
exists ι, inferInstance, c₀, ?_, u₀, v₀
-- 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)
v₀ : F
hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁
x : ι
⊢ Eq (α := F) ((c₀ x)′ : F) (0 : F)

Tactic:
simp [c₀, Derivation.leibniz_div, hc]

Premises used: Derivation.leibniz_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
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)
v₀ : F
hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁
refine_2 :
  Eq.{u_2 + 1} (α := K) ((algebraMap F K : (a : F) → K) a : K)
    ((algebraMap F K : (a : F) → K) (HAdd.hAdd (α := F) (β := F) (∑ x : ι, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)) : K)
apply_fun : Function.Injective.{u_1 + 1, u_2 + 1} (α := F) (β := K) (⇑(algebraMap F K) : (a : F) → K)
⊢ a = HAdd.hAdd (α := F) (β := F) (∑ x : ι, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)

Tactic:
apply_fun (algebraMap F K)

Premises used: Algebra.algebraMap
-- 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)
v₀ : F
hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F) (β := K) (⇑(algebraMap F K) : (a : F) → K)

Tactic:
FaithfulSMul.algebraMap_injective F K

Premises used: FaithfulSMul.algebraMap_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
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)
v₀ : F
hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F) (β := K) (⇑(algebraMap F K) : (a : F) → K)

Tactic:
exact FaithfulSMul.algebraMap_injective F K

Premises used: FaithfulSMul.algebraMap_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
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)
v₀ : F
hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F) (β := K) (⇑(algebraMap F K) : (a : F) → K)

Tactic:
case inj =>
        exact FaithfulSMul.algebraMap_injective F K

Premises used: FaithfulSMul.algebraMap_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
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)
v₀ : F
hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁
refine_2 :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (c₀ x) : K) (logDeriv (u₁ x)) : K) (v₁′ : K)
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap F K : (a : F) → K) a : K)
    ((algebraMap F K : (a : F) → K) (HAdd.hAdd (α := F) (β := F) (∑ x : ι, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)) : K)

Tactic:
simp only [map_add, map_sum, map_mul, ← logDeriv_algebraMap, hu₀, ← deriv_algebraMap, hv₀]

Premises used: DifferentialAlgebra.deriv_algebraMap, map_add, map_sum, map_mul, Differential.logDeriv_algebraMap
-- 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)
v₀ : F
hv₀ : (algebraMap F K : (a : F) → K) v₀ = v₁
refine_2 :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x / (↑(Fintype.card.{u_2} Gal(K/F)) : F)) : K)
            (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)) : K) :
        K)
      ((HDiv.hDiv (α := K) (∑ x : Gal(K/F), (x : (a : K) → K) v) (↑(Fintype.card.{u_2} Gal(K/F)) : K))′ : K)
⊢ (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (c₀ x) : K) (logDeriv (u₁ x)) : K) (v₁′ : K)

Tactic:
unfold u₁ v₁ c₀
-- 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) (β := K)
      (∑ x : ι,
          HDiv.hDiv (α := K) (↑(c x) : K) (↑(Fintype.card.{u_2} Gal(K/F)) : K) *
            logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)) :
        K)
      ((HDiv.hDiv (α := K) (∑ x : Gal(K/F), (x : (a : K) → K) v) (↑(Fintype.card.{u_2} Gal(K/F)) : 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 / (↑(Fintype.card.{u_2} Gal(K/F)) : F)) : K)
            (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)) : K) :
        K)
      ((HDiv.hDiv (α := K) (∑ x : Gal(K/F), (x : (a : K) → K) v) (↑(Fintype.card.{u_2} Gal(K/F)) : K))′ : K)

Tactic:
push_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
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 =
    ∑ x : ι,
        HDiv.hDiv (α := K) (↑(c x) : K) (↑(Fintype.card.{u_2} Gal(K/F)) : K) *
          logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)) +
      HDiv.hDiv (α := K) (β := K) ((∑ x : Gal(K/F), (x : (a : K) → K) v)′ : K)
        ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K)
rw : Eq.{u_2 + 1} (α := K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K)′ : K) (0 : K)
⊢ (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HDiv.hDiv (α := K) (↑(c x) : K) (↑(Fintype.card.{u_2} Gal(K/F)) : K) *
            logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)) :
        K)
      ((HDiv.hDiv (α := K) (∑ x : Gal(K/F), (x : (a : K) → K) v) (↑(Fintype.card.{u_2} Gal(K/F)) : K))′ : K)

Tactic:
rw [Derivation.leibniz_div_const, smul_eq_mul, inv_mul_eq_div]

Premises used: inv_mul_eq_div, smul_eq_mul, Derivation.leibniz_div_const
-- 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 ⊤) ⊥
⊢ Eq.{u_2 + 1} (α := K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K)′ : K) (0 : 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
⊢ Eq.{u_2 + 1} (α := K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K)′ : K) (0 : K)

Tactic:
case h => 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 ⊤) ⊥
refine_2 :
  (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)
⊢ (algebraMap F K : (a : F) → K) a =
    ∑ x : ι,
        HDiv.hDiv (α := K) (↑(c x) : K) (↑(Fintype.card.{u_2} Gal(K/F)) : K) *
          logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)) +
      HDiv.hDiv (α := K) (β := K) ((∑ x : Gal(K/F), (x : (a : K) → K) v)′ : K)
        ((↑(Fintype.card.{u_2} Gal(K/F)) : K) : K)

Tactic:
simp only [map_sum, div_mul_eq_mul_div]

Premises used: div_mul_eq_mul_div, map_sum