-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem of_le_right' (H : A.LinearDisjoint L) (L' : Type*) [Field L']
    [Algebra F L'] [Algebra L' L] [IsScalarTower F L' L]
    [Algebra L' E] [IsScalarTower F L' E] [IsScalarTower L' L E] : A.LinearDisjoint L'

Proof state:
case h.e'_3.h.e'_9.H
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
x✝ : L'
⊢ (IsScalarTower.toAlgHom F L' E) x✝ = ((IsScalarTower.toAlgHom F L E).comp (IsScalarTower.toAlgHom F L' L)) x✝

Tactic:
exact IsScalarTower.algebraMap_apply L' L E _

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ (IsScalarTower.toAlgHom F L' E).range ≤ (IsScalarTower.toAlgHom F L E).range

Tactic:
convert AlgHom.range_comp_le_range (IsScalarTower.toAlgHom F L' L) (IsScalarTower.toAlgHom F L E)

Result:
case h.e'_3.h.e'_9
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ IsScalarTower.toAlgHom F L' E = (IsScalarTower.toAlgHom F L E).comp (IsScalarTower.toAlgHom F L' L)

Proof state:
case h.e'_3.h.e'_9
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ IsScalarTower.toAlgHom F L' E = (IsScalarTower.toAlgHom F L E).comp (IsScalarTower.toAlgHom F L' L)

Tactic:
ext

Result:
case h.e'_3.h.e'_9.H
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
x✝ : L'
⊢ (IsScalarTower.toAlgHom F L' E) x✝ = ((IsScalarTower.toAlgHom F L E).comp (IsScalarTower.toAlgHom F L' L)) x✝

Proof state:
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ A.LinearDisjoint L'

Tactic:
refine Subalgebra.LinearDisjoint.of_le_right_of_flat H ?_

Result:
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ (IsScalarTower.toAlgHom F L' E).range ≤ (IsScalarTower.toAlgHom F L E).range