-- Mathlib/FieldTheory/Differential/Liouville.lean
/--
Transfer an `IsLiouville` instance using an equivalence `K ≃ₐ[F] K'`.
Requires an algebraic `K'` to show that the equivalence commutes with the derivative.
-/
lemma IsLiouville.equiv {K' : Type*} [Field K'] [Differential K'] [Algebra F K']
    [DifferentialAlgebra F K'] [Algebra.IsAlgebraic F K']
    [inst : IsLiouville F K] (e : K ≃ₐ[F] K') : IsLiouville F K' where
  isLiouville (a : F) (ι : Type) [Fintype ι] (c : ι → F) (hc : ∀ x, (c x)′ = 0)
      (u : ι → K') (v : K') (h : a = ∑ x, c x * logDeriv (u x) + v′)

Proof state:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x : ι₀, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
apply inst.isLiouville a ι c hc (e.symm ∘ u) (e.symm v)

Result:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
⊢ ↑a = ∑ x : ι, ↑(c x) * logDeriv ((⇑e.symm ∘ u) x) + (e.symm v)′

Proof state:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
⊢ ↑a = ∑ x : ι, ↑(c x) * logDeriv ((⇑e.symm ∘ u) x) + (e.symm v)′

Tactic:
apply_fun e.symm at h

Result:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : e.symm ↑a = e.symm (∑ x : ι, ↑(c x) * logDeriv (u x) + v′)
⊢ ↑a = ∑ x : ι, ↑(c x) * logDeriv ((⇑e.symm ∘ u) x) + (e.symm v)′

Proof state:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : e.symm ↑a = e.symm (∑ x : ι, ↑(c x) * logDeriv (u x) + v′)
⊢ ↑a = ∑ x : ι, ↑(c x) * logDeriv ((⇑e.symm ∘ u) x) + (e.symm v)′

Tactic:
simpa [AlgEquiv.commutes, map_add, map_sum, map_mul, logDeriv, algEquiv_deriv'] using h

Result:
no goals