awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (hypothesis)
Goal:
F : Type u_2
inst : Field F
inst_1 : Differential F
inst_2 : CharZero F
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : FiniteDimensional F K
k : K := Exists.choose (p := fun (α : K) ↦ Eq (α := IntermediateField F K) F⟮α⟯ ⊤) ⋯
h : Eq (α := IntermediateField F K) F⟮k⟯ ⊤
⊢ DifferentialAlgebra F K
have this : Fact (Monic (minpoly F k))
Tactic: haveI : Fact (minpoly F k).Monic := ⟨minpoly.monic (IsAlgebraic.of_finite ..).isIntegral⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (hypothesis)
Goal:
F : Type u_2
inst : Field F
inst_1 : Differential F
inst_2 : CharZero F
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : FiniteDimensional F K
k : K := Exists.choose (p := fun (α : K) ↦ Eq (α := IntermediateField F K) F⟮α⟯ ⊤) ⋯
h : Eq (α := IntermediateField F K) F⟮k⟯ ⊤
this : Fact (Monic (minpoly F k))
⊢ DifferentialAlgebra F K
have this₁ : Fact (Irreducible (M := F[X]) (minpoly F k))
Tactic: haveI : Fact (Irreducible (minpoly F k)) :=
    ⟨minpoly.irreducible (IsAlgebraic.of_finite ..).isIntegral⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
⊢ Unique { _a : Differential K // DifferentialAlgebra F K }
have refine : ∀ (x : { _a : Differential K // DifferentialAlgebra F K }) (a : Differential K) (ha : DifferentialAlgebra F K),
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) a ha = Inhabited.default
Tactic: refine ⟨⟨default⟩, fun ⟨a, ha⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
⊢ Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) a ha = Inhabited.default
have a₁ : ∀ (x : K), Eq (α := K) (x′ : K) (x′ : K)
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Eq (α := K) (x′ : K) (x′ : K)
have a₁ : Eq.{u_3 + 1} (α := K)
  ((fun (x_2 : K) ↦
      HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
        (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          x_2))
    x′)
  ((fun (x_2 : K) ↦
      HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
        (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          x_2))
    x′)
Tactic: apply_fun (aeval x (mapCoeffs (minpoly F x)) + aeval x (derivative (minpoly F x)) * ·)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
a₁ :
  Eq.{u_3 + 1} (α := K)
    ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′)
    ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′)
⊢ Eq (α := K) (x′ : K) (x′ : K)
have a₂ : Function.Injective (β := K) fun (x_2 : K) ↦
  HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
    (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K) x_2)
Tactic: apply_fun (aeval x (mapCoeffs (minpoly F x)) + aeval x (derivative (minpoly F x)) * ·)
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Eq.{u_3 + 1} (α := K)
    ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′)
    ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′)
have a₁ : Eq.{u_3 + 1} (α := K) (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
  ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′ :
    K)
Tactic: conv_lhs => apply (deriv_aeval_eq ..).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Eq.{u_3 + 1} (α := K) (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
    ((fun (x_2 : K) ↦
          HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
              x_2))
        x′ :
      K)
have a₁ : Eq.{u_3 + 1} (α := K) (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
  (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
Tactic: conv_rhs => apply (@deriv_aeval_eq _ _ _ _ _ default.1 _ default.2 _ _).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Function.Injective (β := K) fun (x_2 : K) ↦
    HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
      (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K) x_2)
have a₁ : Function.Injective (α := K)
  (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K))
Tactic: apply (add_right_injective _).comp
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Function.Injective (α := K)
    (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K))
have a₁ : Ne.{u_3 + 1} (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K) (0 : K)
Tactic: apply mul_right_injective₀
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Ne.{u_3 + 1} (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K) (0 : K)
have a₁ : ¬Dvd.dvd (α := F[X]) (minpoly F x) ((derivative : (a : F[X]) → F[X]) (minpoly F x))
Tactic: rw [ne_eq, ← minpoly.dvd_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (hypothesis)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ ¬Dvd.dvd (α := F[X]) (minpoly F x) ((derivative : (a : F[X]) → F[X]) (minpoly F x))
have this : 0 < natDegree (minpoly F x)
Tactic: have : 0 < (minpoly F x).natDegree := Irreducible.natDegree_pos
      (minpoly.irreducible (Algebra.IsIntegral.isIntegral _))
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < natDegree (minpoly F x)
⊢ ¬Dvd.dvd (α := F[X]) (minpoly F x) ((derivative : (a : F[X]) → F[X]) (minpoly F x))
have a₁ : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) (0 : F[X])
Tactic: apply not_dvd_of_natDegree_lt
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < natDegree (minpoly F x)
a₁ : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) (0 : F[X])
⊢ ¬Dvd.dvd (α := F[X]) (minpoly F x) ((derivative : (a : F[X]) → F[X]) (minpoly F x))
have a₂ : natDegree.{u_2} (R := F) ((derivative : (a : F[X]) → F[X]) (minpoly F x)) < natDegree (minpoly F x)
Tactic: apply not_dvd_of_natDegree_lt
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < natDegree (minpoly F x)
⊢ natDegree.{u_2} (R := F) ((derivative : (a : F[X]) → F[X]) (minpoly F x)) < natDegree (minpoly F x)
have a₁ : natDegree (minpoly F x) ≠ 0
Tactic: apply natDegree_derivative_lt
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : Differential K
inst_8 : DifferentialAlgebra F K
B : IntermediateField F K
inst_9 : FiniteDimensional.{u_2, u_3} F ↥B
a : ↥B
⊢ Eq (α := K) (((algebraMap (↥B) K : (a : ↥B) → K) a : K)′ : K) ((algebraMap (↥B) K : (a : ↥B) → K) (a′ : ↥B) : K)
have change : Eq (α := K) (((B.val : (a : ↥B) → K) a : K)′ : K) ((B.val : (a : ↥B) → K) (a′ : ↥B) : K)
Tactic: change (B.val a)′ = B.val a′
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Basic (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : Differential K
inst_8 : DifferentialAlgebra F K
B : IntermediateField F K
inst_9 : FiniteDimensional.{u_2, u_3} F ↥B
a : ↥B
⊢ Eq (α := K) (((B.val : (a : ↥B) → K) a : K)′ : K) ((B.val : (a : ↥B) → K) (a′ : ↥B) : K)
have hf : Function.Injective (α := ↥B) (β := K) (⇑B.val : (a : ↥B) → K)
Tactic: rw [algHom_deriv']
-- 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
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
⊢ ∃ (ι₀ : 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 : ∀ (ι₀ : Type) (w : Fintype ι₀) (c₀ : ι₀ → K) (hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀ x)′ : K) (0 : K)) (u₀ : ι₀ → K)
  (v₀ : K) (h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : K) (v₀′ : K)),
  ∃ (ι₀ : Type) (x : Fintype ι₀) (c₀ : ι₀ → F) (_ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)) (u₀ : ι₀ → F) (v₀ :
    F), a = HAdd.hAdd (α := F) (β := F) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : F) (v₀′ : F)
Tactic: obtain ⟨ι₀, _, c₀, hc₀, u₀, v₀, h₀⟩ := inst2.isLiouville (a : K) ι
        ((↑) ∘ c)
        (fun _ ↦ by simp only [Function.comp_apply, ← coe_deriv, coe_eq_zero_iff, hc])
        ((↑) ∘ u) v (by simpa only [Function.comp_apply, ← IsScalarTower.algebraMap_apply])
-- 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
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀ : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀ x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : K) (v₀′ : 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 hc₁ : ∀ (x : ι₀), Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F K)) (c₀ x)
Tactic: have hc (x : ι₀) := mem_range_of_deriv_eq_zero F (hc₀ x)
-- 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
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀ : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀ x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀ x * logDeriv (u₀ x) : K) (v₀′ : K)
hc : ∀ (x : ι₀), Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F K)) (c₀ x)
⊢ ∃ (ι₀ : 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 : ∀ (c₀_1 : (x : ι₀) → F) (hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀_1 x) = c₀ x),
  ∃ (ι₀ : 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 c₀ hc using hc
Cleared hypotheses: hc
-- 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
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
⊢ ∃ (ι₀ : 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 apply : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, (↑(c₀ x) : K) * logDeriv (u₀ x) : K) (v₀′ : K)
Tactic: apply inst1.isLiouville a ι₀ 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
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
apply : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, (↑(c₀ x) : K) * logDeriv (u₀ x) : K) (v₀′ : 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 apply₁ : ∀ (x : ι₀), Eq (α := F) ((c₀ x)′ : F) (0 : F)
Tactic: apply inst1.isLiouville a ι₀ 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
A : Type u_3
inst_6 : Field A
inst_7 : Algebra K A
inst_8 : Algebra F A
inst_9 : Differential A
inst_10 : IsScalarTower F K A
inst_11 : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst_12 : Fintype ι
c : ι → F
hc_1 : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → A
v : A
h : (↑a : A) = HAdd.hAdd (α := A) (β := A) (∑ x : ι, (↑(c x) : A) * logDeriv (u x) : A) (v′ : A)
ι₀ : Type
w : Fintype ι₀
c₀_1 : ι₀ → K
hc₀ : ∀ (x : ι₀), Eq (α := K) ((c₀_1 x)′ : K) (0 : K)
u₀ : ι₀ → K
v₀ : K
h₀ : (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K)
c₀ : (x : ι₀) → F
hc : ∀ (x : ι₀), ((algebraMap F K : F →+* K) : (a : F) → K) (c₀ x) = c₀_1 x
⊢ (↑a : K) = HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, (↑(c₀ x) : K) * logDeriv (u₀ x) : K) (v₀′ : K)
have rw : HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, c₀_1 x * logDeriv (u₀ x) : K) (v₀′ : K) =
  HAdd.hAdd (α := K) (β := K) (∑ x : ι₀, (↑(c₀ x) : K) * logDeriv (u₀ x) : K) (v₀′ : K)
Tactic: rw [h₀]