-- Mathlib/FieldTheory/Differential/Liouville.lean
lemma IsLiouville.trans {A : Type*} [Field A] [Algebra K A] [Algebra F A]
    [Differential A] [IsScalarTower F K A] [Differential.ContainConstants F K]
    (inst1 : IsLiouville F K) (inst2 : IsLiouville K A) : IsLiouville F A where
  isLiouville (a : F) (ι : Type) [Fintype ι] (c : ι → F) (hc : ∀ x, (c x)′ = 0)
      (u : ι → A) (v : A) (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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
⊢ ↑↑a = ∑ x : ι, ↑((Algebra.cast ∘ c) x) * logDeriv (((fun x => x) ∘ u) x) + v′

Tactic:
simpa only [Function.comp_apply, ← IsScalarTower.algebraMap_apply]

Result:
no goals

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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x : ι₀, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ∀ (x : ι₀), (c₀ x)′ = 0

Tactic:
intro

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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x : ι₀, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ (c₀ x✝)′ = 0

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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x : ι₀, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ (c₀✝ x✝)′ = 0

Tactic:
apply hc₀

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x : ι₀, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ∑ x : ι₀, c₀✝ x * logDeriv (u₀ x) + v₀′ = ∑ x : ι₀, ↑(c₀ x) * logDeriv (u₀ x) + v₀′

Tactic:
simp [hc]

Result:
no goals

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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x : ι, ↑(c x) * logDeriv (u x) + v′
x✝ : ι
⊢ ((Algebra.cast ∘ c) x✝)′ = 0

Tactic:
simp only [Function.comp_apply, ← coe_deriv, lift_map_eq_zero_iff, hc]

Result:
no goals