-- Mathlib/RingTheory/LinearDisjoint.lean
theorem of_finrank_sup_of_free [Module.Free R A] [Module.Free R B]
    [Module.Finite R A] [Module.Finite R B]
    (H : Module.finrank R ↥(A ⊔ B) = Module.finrank R A * Module.finrank R B) :
    A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
⊢ A.LinearDisjoint B

Tactic:
obtain ⟨j, hj⟩ := exists_linearIndependent_of_le_finrank H.ge

Result:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : LinearIndependent R j
⊢ A.LinearDisjoint B

Proof state:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
⊢ A.LinearDisjoint B

Tactic:
replace hj : Function.Injective j' := by simpa [j']

Result:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
hj : Function.Injective ⇑j'
⊢ A.LinearDisjoint B

Proof state:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
hj : Function.Injective ⇑j'
hf : Function.Surjective ⇑(A.mulMap' B).toLinearMap
this : Module.Finite R ↥(A ⊔ B)
⊢ A.LinearDisjoint B

Tactic:
rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]

Result:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
hj : Function.Injective ⇑j'
hf : Function.Surjective ⇑(A.mulMap' B).toLinearMap
this : Module.Finite R ↥(A ⊔ B)
⊢ Function.Injective ⇑((toSubmodule A).mulMap (toSubmodule B))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
⊢ Function.Injective ⇑j'

Tactic:
simpa [j']

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥A * Module.finrank R ↥B
a✝ : Nontrivial R
⊢ A.LinearDisjoint B

Tactic:
rw [← Module.finrank_tensorProduct] at H

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
⊢ A.LinearDisjoint B

Proof state:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
⊢ A.LinearDisjoint B

Tactic:
let j' := Finsupp.linearCombination R j ∘ₗ
  (LinearEquiv.ofFinrankEq (A ⊗[R] B) _ (by simp)).toLinearMap

Result:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
⊢ A.LinearDisjoint B

Proof state:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
hj : Function.Injective ⇑j'
hf : Function.Surjective ⇑(A.mulMap' B).toLinearMap
⊢ A.LinearDisjoint B

Tactic:
haveI := Subalgebra.finite_sup A B

Result:
case intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : Module.finrank R ↥(A ⊔ B) = Module.finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
hj : Function.Injective ⇑j'
hf : Function.Surjective ⇑(A.mulMap' B).toLinearMap
this : Module.Finite R ↥(A ⊔ B)
⊢ A.LinearDisjoint B