-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.LinearDisjoint (goal)
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra.IsIntegral R₂ B
inst_45 : Free A R₂
inst_46 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
this_1 : Algebra.IsSeparable.{u_1, u_6} (FractionRing A) (FractionRing R₂)
this :
  LE.le (α := Submodule B L)
    (span B (↑(Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (traceDual R₁ (↥F₁) 1)) : Set L))
    (span B (↑(span R₁ ((⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) '' (↑(traceDual A K 1) : Set ↥F₂))) : Set L))
rwa :
  ∀
    (this :
      LE.le (α := Submodule B L) (span B (↑(span R₁ (↑(traceDual R₁ (↥F₁) 1) : Set L)) : Set L))
        (span B (↑(span R₁ ((⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) '' (↑(traceDual A K 1) : Set ↥F₂))) : Set L))),
    LE.le (α := Submodule B L) (traceDual R₁ (↥F₁) 1)
      (span B ((⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) '' (↑(traceDual A K 1) : Set ↥F₂)))
rwa₁ :
  ∀
    (this :
      LE.le (α := Submodule B L) (span B (↑(traceDual R₁ (↥F₁) 1) : Set L))
        (span B (↑(span R₁ ((⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) '' (↑(traceDual A K 1) : Set ↥F₂))) : Set L))),
    LE.le (α := Submodule B L) (traceDual R₁ (↥F₁) 1)
      (span B ((⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) '' (↑(traceDual A K 1) : Set ↥F₂)))
⊢ LE.le (α := Submodule B L) (traceDual R₁ (↥F₁) 1)
    (span B ((⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) '' (↑(traceDual A K 1) : Set ↥F₂)))
have rwa₂ : ∀
  (this :
    LE.le (α := Submodule B L) (span B (↑(traceDual R₁ (↥F₁) 1) : Set L))
      (span B ((⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) '' (↑(traceDual A K 1) : Set ↥F₂)))),
  LE.le (α := Submodule B L) (traceDual R₁ (↥F₁) 1)
    (span B ((⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) '' (↑(traceDual A K 1) : Set ↥F₂)))
Tactic: rwa [← span_coe_eq_restrictScalars, span_span_of_tower, span_span_of_tower, span_eq] at this
Cleared hypotheses: this