Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴⁶ : CommRing A
inst✝⁴⁵ : Field K
inst✝⁴⁴ : Algebra A K
inst✝⁴³ : IsFractionRing A K
inst✝⁴² : CommRing B
inst✝⁴¹ : Field L
inst✝⁴⁰ : Algebra B L
inst✝³⁹ : Algebra A L
inst✝³⁸ : Algebra K L
inst✝³⁷ : FiniteDimensional K L
inst✝³⁶ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝³⁵ : CommRing R₁
inst✝³⁴ : CommRing R₂
inst✝³³ : IsDomain R₁
inst✝³² : Algebra A R₁
inst✝³¹ : Algebra A R₂
inst✝³⁰ : Algebra R₁ B
inst✝²⁹ : Algebra R₂ B
inst✝²⁸ : Algebra R₁ L
inst✝²⁷ : Algebra R₂ L
inst✝²⁶ : IsScalarTower A R₁ L
inst✝²⁵ : IsScalarTower R₁ B L
inst✝²⁴ : IsScalarTower R₂ B L
inst✝²³ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝²² : Algebra R₁ ↥F₁
inst✝²¹ : Algebra R₂ ↥F₂
inst✝²⁰ : IsTorsionFree R₁ ↥F₁
inst✝¹⁹ : IsScalarTower A (↥F₂) L
inst✝¹⁸ : IsScalarTower A R₂ ↥F₂
inst✝¹⁷ : IsScalarTower R₁ (↥F₁) L
inst✝¹⁶ : IsScalarTower R₂ (↥F₂) L
inst✝¹⁵ : Algebra.IsSeparable K ↥F₂
inst✝¹⁴ : Algebra.IsSeparable (↥F₁) L
inst✝¹³ : IsDomain A
inst✝¹² : IsDedekindDomain B
inst✝¹¹ : IsDedekindDomain R₁
inst✝¹⁰ : IsDedekindDomain R₂
inst✝⁹ : IsFractionRing B L
inst✝⁸ : IsFractionRing R₁ ↥F₁
inst✝⁷ : IsFractionRing R₂ ↥F₂
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsIntegralClosure B R₁ L
inst✝⁴ : IsTorsionFree R₁ B
inst✝³ : IsTorsionFree R₂ B
inst✝² : Algebra.IsIntegral R₂ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
this : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
⊢ traceDual R₁ (↥F₁) 1 ≤ span B (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))

pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴⁶ : CommRing A
inst✝⁴⁵ : Field K
inst✝⁴⁴ : Algebra A K
inst✝⁴³ : IsFractionRing A K
inst✝⁴² : CommRing B
inst✝⁴¹ : Field L
inst✝⁴⁰ : Algebra B L
inst✝³⁹ : Algebra A L
inst✝³⁸ : Algebra K L
inst✝³⁷ : FiniteDimensional K L
inst✝³⁶ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝³⁵ : CommRing R₁
inst✝³⁴ : CommRing R₂
inst✝³³ : IsDomain R₁
inst✝³² : Algebra A R₁
inst✝³¹ : Algebra A R₂
inst✝³⁰ : Algebra R₁ B
inst✝²⁹ : Algebra R₂ B
inst✝²⁸ : Algebra R₁ L
inst✝²⁷ : Algebra R₂ L
inst✝²⁶ : IsScalarTower A R₁ L
inst✝²⁵ : IsScalarTower R₁ B L
inst✝²⁴ : IsScalarTower R₂ B L
inst✝²³ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝²² : Algebra R₁ ↥F₁
inst✝²¹ : Algebra R₂ ↥F₂
inst✝²⁰ : IsTorsionFree R₁ ↥F₁
inst✝¹⁹ : IsScalarTower A (↥F₂) L
inst✝¹⁸ : IsScalarTower A R₂ ↥F₂
inst✝¹⁷ : IsScalarTower R₁ (↥F₁) L
inst✝¹⁶ : IsScalarTower R₂ (↥F₂) L
inst✝¹⁵ : Algebra.IsSeparable K ↥F₂
inst✝¹⁴ : Algebra.IsSeparable (↥F₁) L
inst✝¹³ : IsDomain A
inst✝¹² : IsDedekindDomain B
inst✝¹¹ : IsDedekindDomain R₁
inst✝¹⁰ : IsDedekindDomain R₂
inst✝⁹ : IsFractionRing B L
inst✝⁸ : IsFractionRing R₁ ↥F₁
inst✝⁷ : IsFractionRing R₂ ↥F₂
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsIntegralClosure B R₁ L
inst✝⁴ : IsTorsionFree R₁ B
inst✝³ : IsTorsionFree R₂ B
inst✝² : Algebra.IsIntegral R₂ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
this : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
⊢ (extendedHom L B) ↑(differentIdeal A R₂) ≠ 0

Tactic:
· have := Submodule.span_mono (R := B) <| traceDual_le_span_map_traceDual A B R₁ R₂ h₁ h₂
    rwa [← span_coe_eq_restrictScalars, span_span_of_tower, span_span_of_tower, span_eq] at this

Goal state after:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴⁶ : CommRing A
inst✝⁴⁵ : Field K
inst✝⁴⁴ : Algebra A K
inst✝⁴³ : IsFractionRing A K
inst✝⁴² : CommRing B
inst✝⁴¹ : Field L
inst✝⁴⁰ : Algebra B L
inst✝³⁹ : Algebra A L
inst✝³⁸ : Algebra K L
inst✝³⁷ : FiniteDimensional K L
inst✝³⁶ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝³⁵ : CommRing R₁
inst✝³⁴ : CommRing R₂
inst✝³³ : IsDomain R₁
inst✝³² : Algebra A R₁
inst✝³¹ : Algebra A R₂
inst✝³⁰ : Algebra R₁ B
inst✝²⁹ : Algebra R₂ B
inst✝²⁸ : Algebra R₁ L
inst✝²⁷ : Algebra R₂ L
inst✝²⁶ : IsScalarTower A R₁ L
inst✝²⁵ : IsScalarTower R₁ B L
inst✝²⁴ : IsScalarTower R₂ B L
inst✝²³ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝²² : Algebra R₁ ↥F₁
inst✝²¹ : Algebra R₂ ↥F₂
inst✝²⁰ : IsTorsionFree R₁ ↥F₁
inst✝¹⁹ : IsScalarTower A (↥F₂) L
inst✝¹⁸ : IsScalarTower A R₂ ↥F₂
inst✝¹⁷ : IsScalarTower R₁ (↥F₁) L
inst✝¹⁶ : IsScalarTower R₂ (↥F₂) L
inst✝¹⁵ : Algebra.IsSeparable K ↥F₂
inst✝¹⁴ : Algebra.IsSeparable (↥F₁) L
inst✝¹³ : IsDomain A
inst✝¹² : IsDedekindDomain B
inst✝¹¹ : IsDedekindDomain R₁
inst✝¹⁰ : IsDedekindDomain R₂
inst✝⁹ : IsFractionRing B L
inst✝⁸ : IsFractionRing R₁ ↥F₁
inst✝⁷ : IsFractionRing R₂ ↥F₂
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsIntegralClosure B R₁ L
inst✝⁴ : IsTorsionFree R₁ B
inst✝³ : IsTorsionFree R₂ B
inst✝² : Algebra.IsIntegral R₂ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
this : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
⊢ (extendedHom L B) ↑(differentIdeal A R₂) ≠ 0