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 A B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : IsTorsionFree A B
inst✝⁸ : IsTorsionFree A R₁
inst✝⁷ : IsTorsionFree A R₂
inst✝⁶ : Module.Finite A R₁
inst✝⁵ : Module.Finite R₂ B
inst✝⁴ : IsScalarTower A R₂ B
inst✝³ : Module.Finite R₁ B
inst✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝¹ : IsScalarTower A R₁ B
inst✝ : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
ι : Type u_7
b : Basis ι K ↥F₂
hb : span A (Set.range ⇑b) = (↑(IsScalarTower.toAlgHom A R₂ ↥F₂)).range
⊢ span R₁ (Set.range ⇑(h₁.basisOfBasisRight h₂ b)) = Submodule.restrictScalars R₁ 1

Tactic:
classical
  have h₂' : F₁ ⊔ F₂ = ⊤ := by
    rwa [← sup_toSubalgebra_of_isAlgebraic_right, ← top_toSubalgebra, toSubalgebra_inj] at h₂
  have : Finite ι := Module.Finite.finite_basis b
  have h_main := congr_arg (Submodule.restrictScalars R₁) <|
    congr_arg coeToSubmodule <| (1 : FractionalIdeal B⁰ L).dual_dual R₁ F₁
  rw [← coe_one, ← h_main, coe_dual _ _ (by simp), coe_dual_one, restrictScalars_traceDual,
    ← traceDual_eq_span_map_traceDual_of_linearDisjoint A B R₁ R₂ h₁ h₂' h₃,
    ← coe_restrictScalars A, traceDual_span_of_basis A (1 : Submodule R₂ F₂) b,
    ← IsScalarTower.coe_toAlgHom' A F₂ L, ← AlgHom.coe_toLinearMap, ← map_coe, map_span,
    span_span_of_tower, AlgHom.coe_toLinearMap, IsScalarTower.coe_toAlgHom', ← Set.range_comp]
  · have : (h₁.basisOfBasisRight h₂ b).traceDual = algebraMap F₂ L ∘ b.traceDual := by
      refine Basis.traceDual_eq_iff.mpr fun i j ↦ ?_
      rw [Function.comp_apply, h₁.basisOfBasisRight_apply, traceForm_apply, ← map_mul,
        h₁.trace_algebraMap h₂', b.trace_traceDual_mul i j, MonoidWithZeroHom.map_ite_one_zero]
    rw [← this, (traceForm F₁ L).dualSubmodule_span_of_basis (traceForm_nondegenerate F₁ L),
      ← Basis.traceDual_def, Basis.traceDual_traceDual]
  · rw [hb]
    ext; simp

Goal state after: