-- 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 * Module.finrank R ↥B
⊢ A.LinearDisjoint B

Tactic:
nontriviality R

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 * Module.finrank R ↥B
a✝ : Nontrivial R
⊢ 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
j : Fin (Module.finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
⊢ Module.finrank R (↥A ⊗[R] ↥B) = Module.finrank R (Fin (Module.finrank R (↥A ⊗[R] ↥B)) →₀ R)

Tactic:
simp

Result:
no goals

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 : LinearIndependent R j
⊢ A.LinearDisjoint B

Tactic:
rw [LinearIndependent] at hj

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)
⊢ 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'
⊢ A.LinearDisjoint B

Tactic:
have hf : Function.Surjective (mulMap' A B).toLinearMap := mulMap'_surjective 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
⊢ 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)
⊢ Function.Injective ⇑((toSubmodule A).mulMap (toSubmodule B))

Tactic:
exact Subtype.val_injective.comp (OrzechProperty.injective_of_surjective_of_injective j' _ hj hf)

Result:
no goals