-- 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:
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✝ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hx : x✝ ∈ {x, y}
⊢ x✝ ∈ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)))

Tactic:
have : Submodule.inclusion hM = Submodule.inclusion hA ∘ₗ Submodule.inclusion
  (show M' ≤ toSubmodule A' by
    rw [← hs, Submodule.span_le]; exact Algebra.adjoin_le_iff.1 (le_refl _)) := rfl

Result:
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✝ : ↥(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)))

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'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)))
s : Finset S
hs : Submodule.span R ↑s = M'
⊢ ↑s ⊆ ↑A

Tactic:
rwa [← hs, Submodule.span_le] at hM

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
⊢ x = y

Tactic:
obtain ⟨M', hM, hf, h⟩ :=
  TensorProduct.exists_finite_submodule_left_of_finite' {x, y} (Set.toFinite _)

Result:
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

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
⊢ x = y

Tactic:
have hf' : Submodule.FG (toSubmodule A') := fg_adjoin_of_finite s.finite_toSet fun x hx ↦
  (isIntegral_algHom_iff A.val Subtype.val_injective).2
    (Algebra.IsIntegral.isIntegral (R := R) (A := A) ⟨x, hs' hx⟩)

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' : (toSubmodule A').FG
⊢ 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)))
⊢ x ∈ {x, y}

Tactic:
simp

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'
hA : toSubmodule A' ≤ toSubmodule A
⊢ x = y

Tactic:
replace h : {x, y} ⊆ (LinearMap.range (LinearMap.rTensor (toSubmodule B)
    (Submodule.inclusion hA)) : Set _) := fun _ hx ↦ by
  have : Submodule.inclusion hM = Submodule.inclusion hA ∘ₗ Submodule.inclusion
    (show M' ≤ toSubmodule A' by
      rw [← hs, Submodule.span_le]; exact Algebra.adjoin_le_iff.1 (le_refl _)) := rfl
  rw [this, LinearMap.rTensor_comp] at h
  exact LinearMap.range_comp_le_range _ _ (h hx)

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'
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 = y