awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : finrank.{u, v} R ↥B = 0
H₁ : finrank.{u, v} R ↥A = 1
⊢ Nontrivial R

Tactic:
rw [h2, Nat.coprime_zero_right] at H

Premises used: Nat.coprime_zero_right
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : finrank.{u, v} R ↥B = 0
H₁ : finrank.{u, v} R ↥A = 1
a : Nontrivial R
⊢ ¬finrank.{u, v} R ↥A = 0

Tactic:
rw [h2, Nat.coprime_zero_right] at H

Premises used: Nat.coprime_zero_right
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : finrank.{u, v} R ↥B = 0
H₁ : finrank.{u, v} R ↥A = 1
a : Nontrivial R
h1₁ : ¬finrank.{u, v} R ↥A = 0
⊢ finrank.{u, v} R ↥B = 0

Tactic:
rw [h2, Nat.coprime_zero_right] at H

Premises used: Nat.coprime_zero_right
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : finrank.{u, v} R ↥A = 1
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : finrank.{u, v} R ↥B = 0
pos : Subalgebra.LinearDisjoint ⊥ B
⊢ A.LinearDisjoint B

Tactic:
rw [eq_bot_of_finrank_one H]

Premises used: Subalgebra.eq_bot_of_finrank_one
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : finrank.{u, v} R ↥A = 1
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : finrank.{u, v} R ↥B = 0
⊢ Subalgebra.LinearDisjoint ⊥ B

Tactic:
bot_left _

Premises used: Subalgebra.LinearDisjoint.bot_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : finrank.{u, v} R ↥A = 1
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : finrank.{u, v} R ↥B = 0
⊢ Subalgebra.LinearDisjoint ⊥ B

Tactic:
exact bot_left _

Premises used: Subalgebra.LinearDisjoint.bot_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
⊢ Module.Finite.{u, v} R ↥A

Tactic:
haveI := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h1)
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this : Module.Finite.{u, v} R ↥A
⊢ Module.Finite.{u, v} R ↥B

Tactic:
haveI := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h2)
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this_1 : Module.Finite.{u, v} R ↥A
this : Module.Finite.{u, v} R ↥B
⊢ Module.Finite.{u, v} R ↥(A ⊔ B)

Tactic:
haveI := finite_sup A B
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this_1 : Module.Finite.{u, v} R ↥A
this_2 : Module.Finite.{u, v} R ↥B
this : Module.Finite.{u, v} R ↥(A ⊔ B)
⊢ LE.le (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)
    ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)

Tactic:
simp
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this_1 : Module.Finite.{u, v} R ↥A
this_2 : Module.Finite.{u, v} R ↥B
this : Module.Finite.{u, v} R ↥(A ⊔ B)
⊢ finrank.{u, v} R ↥A ≤ finrank.{u, v} R ↥(A ⊔ B)

Tactic:
have : Module.finrank R A ≤ Module.finrank R ↥(A ⊔ B) :=
    LinearMap.finrank_le_finrank_of_injective <|
      Submodule.inclusion_injective (show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp)
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this_1 : Module.Finite.{u, v} R ↥A
this_2 : Module.Finite.{u, v} R ↥B
this_3 : Module.Finite.{u, v} R ↥(A ⊔ B)
this : finrank.{u, v} R ↥A ≤ finrank.{u, v} R ↥(A ⊔ B)
⊢ A.LinearDisjoint B

Tactic:
of_finrank_sup_of_free <| (finrank_sup_le_of_free A B).antisymm <|
    Nat.le_of_dvd (lt_of_lt_of_le (Nat.pos_of_ne_zero h1) this) <| H.mul_dvd_of_dvd_of_dvd
      (finrank_left_dvd_finrank_sup_of_free A B) (finrank_right_dvd_finrank_sup_of_free A B)

Premises used: LE.le.antisymm, Subalgebra.finrank_right_dvd_finrank_sup_of_free, Subalgebra.finrank_left_dvd_finrank_sup_of_free, Subalgebra.finrank_sup_le_of_free, Subalgebra.LinearDisjoint.of_finrank_sup_of_free, Nat.pos_of_ne_zero, Nat.le_of_dvd, Nat.Coprime.mul_dvd_of_dvd_of_dvd, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this_1 : Module.Finite.{u, v} R ↥A
this_2 : Module.Finite.{u, v} R ↥B
this_3 : Module.Finite.{u, v} R ↥(A ⊔ B)
this : finrank.{u, v} R ↥A ≤ finrank.{u, v} R ↥(A ⊔ B)
⊢ A.LinearDisjoint B

Tactic:
exact of_finrank_sup_of_free <| (finrank_sup_le_of_free A B).antisymm <|
    Nat.le_of_dvd (lt_of_lt_of_le (Nat.pos_of_ne_zero h1) this) <| H.mul_dvd_of_dvd_of_dvd
      (finrank_left_dvd_finrank_sup_of_free A B) (finrank_right_dvd_finrank_sup_of_free A B)

Premises used: LE.le.antisymm, Subalgebra.finrank_right_dvd_finrank_sup_of_free, Subalgebra.finrank_left_dvd_finrank_sup_of_free, Subalgebra.finrank_sup_le_of_free, Subalgebra.LinearDisjoint.of_finrank_sup_of_free, Nat.pos_of_ne_zero, Nat.le_of_dvd, Nat.Coprime.mul_dvd_of_dvd_of_dvd, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
rw :
  Function.Injective.{v + 1, v + 1} (α :=
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
      ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
    (β := S)
    (⇑(Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
          ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) :
      (a :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
        S)
⊢ A.LinearDisjoint B

Tactic:
rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]

Premises used: Submodule.linearDisjoint_iff, Subalgebra.linearDisjoint_iff
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
obtain :
  ∀ (M' : Submodule R S) (hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
    (hf : Module.Finite.{u, v} R ↥M')
    (h :
      {x, y} ⊆
        (↑(LinearMap.range
              (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
                (Submodule.inclusion hM))) :
          Set
            (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))),
    x = y
⊢ x = y

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

Premises used: Insert.insert, Set.toFinite, TensorProduct.exists_finite_submodule_left_of_setFinite', Singleton.singleton
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
⊢ M'.FG

Tactic:
.of_finite

Premises used: Submodule.FG.of_finite
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
obtain : ∀ (s : Finset S) (hs : Submodule.span R (↑s : Set S) = M'), x = y
⊢ x = y

Tactic:
obtain ⟨s, hs⟩ : M'.FG := .of_finite

Premises used: Submodule.FG
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
s : Finset S
hs : Submodule.span R (↑s : Set S) = M'
rwa :
  ∀
    (hM :
      LE.le (α := Submodule R S) (Submodule.span R (↑s : Set S))
        ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A))
    (hs : Submodule.span R (↑s : Set S) = M'), (↑s : Set S) ⊆ (↑A : Set S)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hM : (↑s : Set S) ⊆ (↑((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) : Set S))
    (hs : Submodule.span R (↑s : Set S) = M'), (↑s : Set S) ⊆ (↑A : Set S)
⊢ (↑s : Set S) ⊆ (↑A : Set S)

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

Premises used: Submodule.span_le
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
s : Finset S
hs : Submodule.span R (↑s : Set S) = M'
⊢ (↑s : Set S) ⊆ (↑A : Set S)

Tactic:
have hs' : (s : Set S) ⊆ A := by rwa [← hs, Submodule.span_le] at hM
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
s : Finset S
hs : Submodule.span R (↑s : Set S) = M'
hs' : (↑s : Set S) ⊆ (↑A : Set S)
A' : Subalgebra R S := Algebra.adjoin R (↑s : Set S)
⊢ Submodule.FG.{u, v} (R := R) (M := S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A')

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⟩)
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
s : Finset S
hs : Submodule.span R (↑s : Set S) = M'
hs' : (↑s : Set S) ⊆ (↑A : Set S)
A' : Subalgebra R S := Algebra.adjoin R (↑s : Set S)
hf' : Submodule.FG.{u, v} (R := R) (M := S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A')
⊢ Module.Finite.{u, v} R ↥A'

Tactic:
replace hf' : Module.Finite R A' := .of_fg hf'