-- Mathlib/RingTheory/LinearDisjoint.lean
theorem adjoin_rank_eq_rank_left [Module.Free R A] [Module.Flat R B]
    [Nontrivial R] [Nontrivial S] :
    Module.rank B (Algebra.adjoin B (A : Set S)) = Module.rank R A

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Module.Free R ↥A
inst✝² : Module.Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ Module.rank ↥B ↥(Submodule.span (↥B) (Set.range fun i => ↑((Module.Free.chooseBasis R ↥A) i))) =
    Cardinal.mk (Module.Free.ChooseBasisIndex R ↥A)

Tactic:
change Module.rank B (Submodule.span B (Set.range (A.val ∘ Module.Free.chooseBasis R A))) = _

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Module.Free R ↥A
inst✝² : Module.Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ Module.rank ↥B ↥(Submodule.span (↥B) (Set.range (⇑A.val ∘ ⇑(Module.Free.chooseBasis R ↥A)))) =
    Cardinal.mk (Module.Free.ChooseBasisIndex R ↥A)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Module.Free R ↥A
inst✝² : Module.Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ Module.rank ↥B ↥(Submodule.span (↥B) (Set.range (⇑A.val ∘ ⇑(Module.Free.chooseBasis R ↥A)))) =
    Cardinal.mk (Module.Free.ChooseBasisIndex R ↥A)

Tactic:
have := H.linearIndependent_left_of_flat (Module.Free.chooseBasis R A).linearIndependent

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Module.Free R ↥A
inst✝² : Module.Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : LinearIndependent (↥B) (⇑A.val ∘ ⇑(Module.Free.chooseBasis R ↥A))
⊢ Module.rank ↥B ↥(Submodule.span (↥B) (Set.range (⇑A.val ∘ ⇑(Module.Free.chooseBasis R ↥A)))) =
    Cardinal.mk (Module.Free.ChooseBasisIndex R ↥A)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Module.Free R ↥A
inst✝² : Module.Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A) = Module.rank R ↥A

Tactic:
rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex R A,
  A.adjoin_eq_span_basis B (Module.Free.chooseBasis R A)]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Module.Free R ↥A
inst✝² : Module.Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ Module.rank ↥B ↥(Submodule.span (↥B) (Set.range fun i => ↑((Module.Free.chooseBasis R ↥A) i))) =
    Cardinal.mk (Module.Free.ChooseBasisIndex R ↥A)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Module.Free R ↥A
inst✝² : Module.Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : LinearIndependent (↥B) (⇑A.val ∘ ⇑(Module.Free.chooseBasis R ↥A))
⊢ Module.rank ↥B ↥(Submodule.span (↥B) (Set.range (⇑A.val ∘ ⇑(Module.Free.chooseBasis R ↥A)))) =
    Cardinal.mk (Module.Free.ChooseBasisIndex R ↥A)

Tactic:
rw [rank_span this, Cardinal.mk_range_eq _ this.injective]

Result:
no goals