awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
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)
⊢ (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 rw : Eq.{u_2 + 1} (α := K) ((↑(Fintype.card.{u_2} Gal(K/F)) : K)′ : K) (0 : K)
Tactic: rw [Derivation.leibniz_div_const, smul_eq_mul, inv_mul_eq_div]
-- 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 =
    ∑ 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)
have 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)
Tactic: simp only [map_sum, div_mul_eq_mul_div]
-- 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 =
    ∑ 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)
have 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)
Tactic: rw [← sum_div, ← add_div]
-- 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) (∑ 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)
have 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)′)
Tactic: field_simp
-- 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 ⊤) ⊥
| 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)′)
have h₁ : ∀ (i : ι), logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i))
Tactic: enter [2, 1, 2, i, 2]
-- 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 ⊤) ⊥
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)))
have 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)))
Tactic: by_cases h : u i = 0
-- 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 ⊤) ⊥
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)))
⊢ 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)))
have 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)))
Tactic: by_cases h : u i = 0
-- 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 ⊤) ⊥
| 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)′)
have 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)′)
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]
-- 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 ⊤) ⊥
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)′)
| 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)′)
have enter₁ : ∑ x : ι, HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)))
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]
-- 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 ⊤) ⊥
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)))
| 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)′)
have enter₂ : fun (x : ι) ↦ HMul.hMul (α := K) (↑(c x) : K) (logDeriv (∏ x_1 : Gal(K/F), (x_1 : (a : K) → K) (u x)))
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]
-- 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 ⊤) ⊥
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)))
| 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)′)
have h₁ : ∀ (i : ι), HMul.hMul (α := K) (↑(c i) : K) (logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i)))
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]
-- 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 ⊤) ⊥
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)))
| 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)′)
have h₂ : ∀ (i : ι), logDeriv (∏ x : Gal(K/F), (x : (a : K) → K) (u i))
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]
-- 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 ⊤) ⊥
⊢ 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)′)
have 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)′)
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]
-- 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 ⊤) ⊥
⊢ 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)′)
have 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)′)
Tactic: simp_rw [mul_sum]
-- 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 ⊤) ⊥
⊢ 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)′)
have 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)
Tactic: rw [sum_comm, ← sum_add_distrib]
-- 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 ⊤) ⊥
⊢ 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)
have 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)
Tactic: trans ∑ _ : (K ≃ₐ[F] K), a
-- 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 ⊤) ⊥
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)
⊢ 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)
have 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))
Tactic: trans ∑ _ : (K ≃ₐ[F] K), a
-- 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 ⊤) ⊥
⊢ 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))
have 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)
Tactic: rcongr 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
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
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)
have 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)
Tactic: apply_fun e at h
Cleared hypotheses: h