awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ ∃ (ι₀ : 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₁ : ∀ (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
-- 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)
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)
⊢ ∃ (ι₀ : 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 ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
Tactic: have ffb : fixedField ⊤ = ⊥ := (IsGalois.tfae.out 0 1).mp (inferInstance : IsGalois F K)
-- 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)
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 ⊤) ⊥
⊢ ∃ (ι₀ : 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₁ : ∀ (i : ι), ∃ (y : F), (algebraMap F K : (a : F) → K) y = u₁ i
Tactic: simp_rw [ffb, IntermediateField.mem_bot, Set.mem_range] at this
Cleared hypotheses: this
-- 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_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
⊢ ∃ (ι₀ : 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 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)
Tactic: choose u₀ hu₀ using this
Cleared hypotheses: this
-- 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)
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
⊢ Subtype.mk (p := fun (x : Gal(K/F)) ↦ Membership.mem (γ := Subgroup Gal(K/F)) ⊤ x) e property • v₁ = v₁
have change : (e : (a : K) → K) v₁ = v₁
Tactic: change e v₁ = v₁
-- 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)
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 : K) → K) v₁ = v₁
have 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)
Tactic: simp only [v₁, map_div₀, map_sum, map_natCast]
-- 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)
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
⊢ 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)
have 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)
Tactic: congr 1
-- 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)
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
⊢ 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)
have 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)
Tactic: apply Fintype.sum_equiv (Equiv.mulLeft e)
-- 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)
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)
⊢ ∃ (ι₀ : 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₁ : 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
-- 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)
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₁
⊢ ∃ (ι₀ : 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₁ : 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
Cleared hypotheses: this
-- 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_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₁
⊢ ∃ (ι₀ : 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 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)
Tactic: obtain ⟨v₀, hv₀⟩ := this
Cleared hypotheses: this
-- 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)
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₁
⊢ ∃ (ι₀ : 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 refine_1 : ∀ (x : ι), Eq (α := F) ((c₀ x)′ : F) (0 : F)
Tactic: exists ι, inferInstance, c₀, ?_, u₀, v₀
-- 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)
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)
⊢ ∃ (ι₀ : 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 refine_2 : a = HAdd.hAdd (α := F) (β := F) (∑ x : ι, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)
Tactic: exists ι, inferInstance, c₀, ?_, u₀, v₀
-- 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)
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₁
⊢ a = HAdd.hAdd (α := F) (β := F) (∑ x : ι, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)
have 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)
Tactic: apply_fun (algebraMap 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)
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)
⊢ a = HAdd.hAdd (α := F) (β := F) (∑ x : ι, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)
have apply_fun : Function.Injective.{u_1 + 1, u_2 + 1} (α := F) (β := K) (⇑(algebraMap F K) : (a : F) → K)
Tactic: apply_fun (algebraMap 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)
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₁
⊢ 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)
have 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)
Tactic: simp only [map_add, map_sum, map_mul, ← logDeriv_algebraMap, hu₀, ← deriv_algebraMap, hv₀]
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
⊢ (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)
have 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)
Tactic: push_cast
-- 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
⊢ (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)
have 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)
Tactic: rw [Derivation.leibniz_div_const, smul_eq_mul, inv_mul_eq_div]