-- Mathlib/RingTheory/LinearDisjoint.lean
theorem of_linearDisjoint_finite_left [Algebra.IsIntegral R A]
    (H : ∀ A' : Subalgebra R S, A' ≤ A → [Module.Finite R A'] → A'.LinearDisjoint B) :
    A.LinearDisjoint B

Proof state:
case intro.intro.intro.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [inst : Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)))
s : Finset S
hs : Submodule.span R ↑s = M'
⊢ x = y

Tactic:
have hs' : (s : Set S) ⊆ A := by rwa [← hs, Submodule.span_le] at hM

Result:
case intro.intro.intro.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [inst : Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)))
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
⊢ x = y

Proof state:
case intro.intro.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [inst : Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)))
⊢ x = y

Tactic:
obtain ⟨s, hs⟩ := Module.Finite.iff_fg.1 hf

Result:
case intro.intro.intro.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [inst : Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)))
s : Finset S
hs : Submodule.span R ↑s = M'
⊢ x = y

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [inst : Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h :
  {x, y} ⊆
    ↑(LinearMap.range
        (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA) ∘ₗ
          LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion ⋯)))
x✝ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hx : x✝ ∈ {x, y}
this : Submodule.inclusion hM = Submodule.inclusion hA ∘ₗ Submodule.inclusion ⋯
⊢ x✝ ∈ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)))

Tactic:
exact LinearMap.range_comp_le_range _ _ (h hx)

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✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [inst : Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)))
x' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hx' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = x
y' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hy' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) y' = y
⊢ ((toSubmodule A').mulMap (toSubmodule B)) x' = ((toSubmodule A').mulMap (toSubmodule B)) y'

Tactic:
simp [← Submodule.mulMap_comp_rTensor _ hA, hx', hy', hxy]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [inst : Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)))
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
⊢ x = y

Tactic:
have hA : toSubmodule A' ≤ toSubmodule A := Algebra.adjoin_le_iff.2 hs'

Result:
case intro.intro.intro.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [inst : Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)))
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
⊢ x = y