-- Mathlib/RingTheory/Adjoin/Dimension.lean
theorem rank_sup_le_of_free : Module.rank R ↥(A ⊔ B) ≤ Module.rank R A * Module.rank R B

Proof state:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))
⊢ Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
rw [h, ← bA.mk_eq_rank'', ← bB.mk_eq_rank'']

Result:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))
⊢ Module.rank R ↥(Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))) ≤
    Cardinal.mk ιA * Cardinal.mk ιB

Proof state:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
change Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ _

Result:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))
⊢ Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ Module.rank R ↥A * Module.rank R ↥B

Proof state:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
have h := Algebra.adjoin_union_coe_submodule R (A : Set S) (B : Set S)

Result:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (Algebra.adjoin R (↑A ∪ ↑B)) = toSubmodule (Algebra.adjoin R ↑A) * toSubmodule (Algebra.adjoin R ↑B)
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Proof state:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))
⊢ Cardinal.mk ↑(Set.range fun i => ↑(bA i)) * Cardinal.mk ↑(Set.range fun i => ↑(bB i)) ≤
    Cardinal.mk ιA * Cardinal.mk ιB

Tactic:
gcongr <;> exact Cardinal.mk_range_le

Result:
no goals

Proof state:
case intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
obtain ⟨ιB, bB⟩ := Free.exists_basis (R := R) (M := B)

Result:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Proof state:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
obtain ⟨ιA, bA⟩ := Free.exists_basis (R := R) (M := A)

Result:
case intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Proof state:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (Algebra.adjoin R (↑A ∪ ↑B)) = toSubmodule (Algebra.adjoin R ↑A) * toSubmodule (Algebra.adjoin R ↑B)
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
rw [A.adjoin_eq_span_basis R bA, B.adjoin_eq_span_basis R bB, ← Algebra.sup_def,
  Submodule.span_mul_span] at h

Result:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Proof state:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))
⊢ Module.rank R ↥(Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))) ≤
    Cardinal.mk ιA * Cardinal.mk ιB

Tactic:
refine (rank_span_le _).trans Cardinal.mk_mul_le |>.trans ?_

Result:
case intro.mk.intro.mk
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i => ↑(bA i)) * Set.range fun i => ↑(bB i))
⊢ Cardinal.mk ↑(Set.range fun i => ↑(bA i)) * Cardinal.mk ↑(Set.range fun i => ↑(bB i)) ≤
    Cardinal.mk ιA * Cardinal.mk ιB