I think the transcendental case is not too complicated if you use item 1 of my comment here (probably requires extra import though). You've already proven the result for purely transcendental extensions here. Even though we don't have a definition of transcendental degree yet, you can take a F-transcendental basis in A and one in B, and A ⊔ B will be algebraic over the intermediate field generated by the union of the two bases, because of IsTranscendenceBasis.isAlgebraic and algebraicClosure is an intermediate field. (The union of the two bases needs not be a basis, but we should prove a general IntermediateField.card(inal)_adjoin_le.)

By "complicated" I mean the proof is lengthy, cumbersome and need a lot of imports. In fact I have a proof but there are sill some sorrys mainly for struggling the relation of 9 intermediate fields...

Maybe later I'll reconsider your comments and looking for a simpler proof. My opinion is that if we want to keep the import of this file minimal, then we can only prove this version. The general version should go to another file with heavier imports. What's your opinion?

Even though we don't have a definition of transcendental degree yet

No I don't need that in this proof.

a general IntermediateField.card(inal)_adjoin_le

I think I have this result in my WIP file.

[EDIT] I think at least I need to import AlgebraicIndependent (#18648 is needed, and probably relrank in my PR #14987 for ease of computation), which will bump the import count from 1338 to ~1370.

Is there a reason to keep imports minimal? This is a new file after all. By the way, how do you count import increases without opening a PR?

Is there a reason to keep imports minimal? This is a new file after all.

No particular reason. But I feel that these two results are basic. I'm afraid that they will be used in other places. The direct use of them is in linearly disjointness, which does not import AlgebraicIndependent if I remembered correctly.

But anyway they imported Algebraic. The AlgebraicIndependent only adds 4 files compare to Algebraic. So maybe... it's reasonable.

By the way, how do you count import increases without opening a PR?

I'm guessing from #18770 which imports AlgebraicIndependent.

🎉

import Mathlib.RingTheory.Adjoin.Basic
import Mathlib.LinearAlgebra.Dimension.Constructions
import Mathlib.Algebra.Group.Pointwise.Set.Card

theorem Subalgebra.rank_sup_le_of_free!!! {R S : Type*} [CommRing R] [StrongRankCondition R]
    [CommRing S] [Algebra R S]
    (A : Subalgebra R S) (B : Subalgebra R S)
    [Module.Free R A] [Module.Free R B] :
    Module.rank R ↥(A ⊔ B) ≤ Module.rank R A * Module.rank R B := by
  obtain ⟨ιA, bA⟩ := Module.Free.exists_basis (R := R) (M := A)
  obtain ⟨ιB, bB⟩ := Module.Free.exists_basis (R := R) (M := B)
  have h := Algebra.adjoin_union_coe_submodule R (A : Set S) (B : Set S)
  rw [A.adjoin_eq_span_basis R bA, B.adjoin_eq_span_basis R bB, ← Algebra.sup_def,
    Submodule.span_mul_span] at h
  change Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ _
  rw [h, ← bA.mk_eq_rank'', ← bB.mk_eq_rank'']
  refine (rank_span_le _).trans Cardinal.mk_mul_le |>.trans ?_
  gcongr <;> exact Cardinal.mk_range_le

#find_home on my computer just runs out of memory. @alreadydone Could you help me to find a suitable place to put this result?

Great! I usually use the web editor. In this case it finds Mathlib itself. Note that I replaced StrongRankCondition with Nontrivial but it doesn't affect the result. I'm not sure which current files can host this result without adding too many imports.

I replaced StrongRankCondition with Nontrivial but it doesn't affect the result

Because in this case it uses an instance that a non-trivial commutative ring satisfies strong rank condition. I think that file is not imported by so many files.

it finds Mathlib itself

Oops. What about Mathlib.RingTheory.Adjoin.Dimension?

But then we got too many such small files...

[EDIT] Mathlib.FieldTheory.Adjoin seems reasonable, except for missing import Mathlib.Algebra.Group.Pointwise.Set.Card. At least I can put IntermediateField.rank_sup_le_of_isAlgebraic in that file.

I think for the Subalgebra result, Mathlib.LinearAlgebra.Dimension.Constructions is pretty reasonable. It has 2204 transitive imports and importing Mathlib.RingTheory.Adjoin.Basic adds 3 and importing Mathlib.Algebra.Group.Pointwise.Set.Card adds 1. (web editor link) The script is from Damiano here.

LGTM! Let's merge this now; when you're able to remove the algebraic condition, it would be reasonable to import AlgebraicIndependent, which adds 3 imports, plus 1 for RelRank.

it would be reasonable to import AlgebraicIndependent, which adds 3 imports, plus 1 for RelRank

Unfortunately, that's not possible, since AlgebraicIndependent (aevalEquivField in my working PR) and RelRank imports Mathlib.FieldTheory.Adjoin 😂