awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis.{u_1, u, v} ι R ↥M
H :
  Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S)
    (⇑(mulLeftMap (M := M) N (⇑m : (a : ι) → ↥M)) : (a : ι →₀ ↥N) → S)
⊢ Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)

Tactic:
simp_rw [mulLeftMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_rTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.injective_comp] at H

Premises used: EquivLike.injective_comp, LinearEquiv.comp_coe, LinearMap.coe_comp, Submodule.mulLeftMap_eq_mulMap_comp, Module.Basis.coe_repr_symm, LinearEquiv.coe_coe, LinearEquiv.coe_rTensor
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis.{u_1, u, v} ι R ↥M
H :
  Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S)
    (⇑(mulLeftMap (M := M) N (⇑m : (a : ι) → ↥M)) : (a : ι →₀ ↥N) → S)
⊢ Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)

Tactic:
classical simp_rw [mulLeftMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_rTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.injective_comp] at H

Premises used: EquivLike.injective_comp, LinearEquiv.comp_coe, LinearMap.coe_comp, Submodule.mulLeftMap_eq_mulMap_comp, Module.Basis.coe_repr_symm, LinearEquiv.coe_coe, LinearEquiv.coe_rTensor
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis.{u_1, u, v} ι R ↥M
H : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
⊢ M.LinearDisjoint N

Tactic:
⟨H⟩

Premises used: Submodule.LinearDisjoint.mk
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis.{u_1, u, v} ι R ↥M
H : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
⊢ M.LinearDisjoint N

Tactic:
exact ⟨H⟩
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis.{u_1, u, v} ι R ↥N
H :
  Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S)
    (⇑(M.mulRightMap (N := N) (⇑n : (a : ι) → ↥N)) : (a : ι →₀ ↥M) → S)
⊢ Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)

Tactic:
simp_rw [mulRightMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_lTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.injective_comp] at H

Premises used: LinearEquiv.coe_lTensor, EquivLike.injective_comp, Submodule.mulRightMap_eq_mulMap_comp, LinearEquiv.comp_coe, LinearMap.coe_comp, Module.Basis.coe_repr_symm, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis.{u_1, u, v} ι R ↥N
H :
  Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S)
    (⇑(M.mulRightMap (N := N) (⇑n : (a : ι) → ↥N)) : (a : ι →₀ ↥M) → S)
⊢ Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)

Tactic:
classical simp_rw [mulRightMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_lTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.injective_comp] at H

Premises used: LinearEquiv.coe_lTensor, EquivLike.injective_comp, Submodule.mulRightMap_eq_mulMap_comp, LinearEquiv.comp_coe, LinearMap.coe_comp, Module.Basis.coe_repr_symm, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis.{u_1, u, v} ι R ↥N
H : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
⊢ M.LinearDisjoint N

Tactic:
⟨H⟩

Premises used: Submodule.LinearDisjoint.mk
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis.{u_1, u, v} ι R ↥N
H : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
⊢ M.LinearDisjoint N

Tactic:
exact ⟨H⟩
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
H :
  Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦
          HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) :
      (a : κ × ι →₀ R) → S)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ (↑(i0 ≪≫ₗ i1.symm) : (κ × ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N)
h :
  ∀ (x : κ × ι),
    Eq.{v + 1} (α := S) ((i ∘ₗ Finsupp.lsingle x : (a : R) → S) 1 : S)
      (((Finsupp.linearCombination R fun (i : κ × ι) ↦
                HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) ∘ₗ
              Finsupp.lsingle x :
            (a : R) → S)
          1 :
        S)
⊢ i =
    Finsupp.linearCombination R fun (i : κ × ι) ↦
      HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
H :
  Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦
          HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) :
      (a : κ × ι →₀ R) → S)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ (↑(i0 ≪≫ₗ i1.symm) : (κ × ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N)
x : κ × ι
⊢ Eq.{v + 1} (α := S) ((i ∘ₗ Finsupp.lsingle x : (a : R) → S) 1 : S)
    (((Finsupp.linearCombination R fun (i : κ × ι) ↦
              HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) ∘ₗ
            Finsupp.lsingle x :
          (a : R) → S)
        1 :
      S)

Tactic:
simp [i, i0, i1, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Premises used: finsuppTensorFinsupp'_symm_single_eq_single_one_tmul
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
H :
  Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦
          HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) :
      (a : κ × ι →₀ R) → S)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ (↑(i0 ≪≫ₗ i1.symm) : (κ × ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N)
⊢ i =
    Finsupp.linearCombination R fun (i : κ × ι) ↦
      HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)

Tactic:
have : i = Finsupp.linearCombination R fun i : κ × ι ↦ (m i.1 * n i.2 : S) := by
    ext x
    simp [i, i0, i1, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
H :
  Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦
          HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) :
      (a : κ × ι →₀ R) → S)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ (↑(i0 ≪≫ₗ i1.symm) : (κ × ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N)
this :
  i =
    Finsupp.linearCombination R fun (i : κ × ι) ↦
      HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)
⊢ Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)

Tactic:
simp_rw [← this, i, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp] at H

Premises used: EquivLike.injective_comp, LinearMap.coe_comp, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ (↑(i0 ≪≫ₗ i1.symm) : (κ × ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N)
this :
  i =
    Finsupp.linearCombination R fun (i : κ × ι) ↦
      HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)
H : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
⊢ M.LinearDisjoint N

Tactic:
⟨H⟩

Premises used: Submodule.LinearDisjoint.mk
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ (↑(i0 ≪≫ₗ i1.symm) : (κ × ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N)
this :
  i =
    Finsupp.linearCombination R fun (i : κ × ι) ↦
      HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)
H : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
⊢ M.LinearDisjoint N

Tactic:
exact ⟨H⟩
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
N : Submodule R S
⊢ Submodule.LinearDisjoint ⊥ N

Tactic:
⟨Function.injective_of_subsingleton _⟩

Premises used: Submodule.LinearDisjoint.mk, Function.injective_of_subsingleton
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
⊢ M.LinearDisjoint ⊥

Tactic:
⟨Function.injective_of_subsingleton _⟩

Premises used: Submodule.LinearDisjoint.mk, Function.injective_of_subsingleton
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
N : Submodule R S
rw :
  Function.Injective (α := ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ⊗[R] ↥N)
    (β := S)
    (⇑(N.subtype ∘ₗ (↑N.lTensorOne : ↥⊥ ⊗[R] ↥N →ₗ[R] ↥N)) :
      (a : ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) ⊗[R] ↥N) → S)
⊢ Submodule.LinearDisjoint 1 N

Tactic:
rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_left_eq]

Premises used: Submodule.linearDisjoint_iff, Algebra.toSubmodule_bot, Submodule.mulMap_one_left_eq
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
N : Submodule R S
⊢ Function.Injective (α := ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ⊗[R] ↥N)
    (β := S)
    (⇑(N.subtype ∘ₗ (↑N.lTensorOne : ↥⊥ ⊗[R] ↥N →ₗ[R] ↥N)) :
      (a : ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) ⊗[R] ↥N) → S)

Tactic:
N.injective_subtype.comp N.lTensorOne.injective

Premises used: Submodule.lTensorOne, Submodule.injective_subtype, Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
N : Submodule R S
⊢ Function.Injective (α := ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ⊗[R] ↥N)
    (β := S)
    (⇑(N.subtype ∘ₗ (↑N.lTensorOne : ↥⊥ ⊗[R] ↥N →ₗ[R] ↥N)) :
      (a : ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) ⊗[R] ↥N) → S)

Tactic:
exact N.injective_subtype.comp N.lTensorOne.injective

Premises used: Submodule.lTensorOne, Submodule.injective_subtype, Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
rw :
  Function.Injective (α := ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S))
    (β := S)
    (⇑(M.subtype ∘ₗ (↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M)) :
      (a : ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥)) → S)
⊢ M.LinearDisjoint 1

Tactic:
rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_right_eq]

Premises used: Submodule.mulMap_one_right_eq, Submodule.linearDisjoint_iff, Algebra.toSubmodule_bot
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
⊢ Function.Injective (α := ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S))
    (β := S)
    (⇑(M.subtype ∘ₗ (↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M)) :
      (a : ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥)) → S)

Tactic:
M.injective_subtype.comp M.rTensorOne.injective

Premises used: Submodule.injective_subtype, Function.Injective.comp, Submodule.rTensorOne, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
⊢ Function.Injective (α := ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S))
    (β := S)
    (⇑(M.subtype ∘ₗ (↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M)) :
      (a : ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥)) → S)

Tactic:
exact M.injective_subtype.comp M.rTensorOne.injective

Premises used: Submodule.injective_subtype, Function.Injective.comp, Submodule.rTensorOne, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
obtain :
  ∀ (M' : Submodule R S) (hM : M' ≤ M) (hFG : Module.Finite.{u, v} R ↥M')
    (h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))), x = y
⊢ x = y

Tactic:
obtain ⟨M', hM, hFG, 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.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : Module.Finite.{u, v} R ↥M'
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
⊢ M'.FG

Tactic:
rw [Module.Finite.iff_fg] at hFG

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : Module.Finite.{u, v} R ↥M'
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
hFG₁ : M'.FG
⊢ {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))

Tactic:
rw [Module.Finite.iff_fg] at hFG

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
⊢ Membership.mem (γ := Set (↥M ⊗[R] ↥N)) {x, y} x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
obtain :
  ∀ (x' : ↥M' ⊗[R] ↥N) (hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x), x = y
⊢ x = y

Tactic:
obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
⊢ Membership.mem (γ := Set (↥M ⊗[R] ↥N)) {x, y} y

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
obtain :
  ∀ (y' : ↥M' ⊗[R] ↥N) (hy' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' = y), x = y
⊢ x = y

Tactic:
obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' = y
rw :
  Eq (α := ↥M ⊗[R] ↥N) ((LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' : ↥M ⊗[R] ↥N)
    ((LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' : ↥M ⊗[R] ↥N)
⊢ x = y

Tactic:
rw [← hx', ← hy']
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' = y
h₁ : x' = y'
⊢ Eq (α := ↥M ⊗[R] ↥N) ((LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' : ↥M ⊗[R] ↥N)
    ((LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' : ↥M ⊗[R] ↥N)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' = y
⊢ Eq (α := S) ((M'.mulMap N : (a : ↥M' ⊗[R] ↥N) → S) x' : S) ((M'.mulMap N : (a : ↥M' ⊗[R] ↥N) → S) y' : S)

Tactic:
simp [← mulMap_comp_rTensor _ hM, hx', hy', hxy]

Premises used: Submodule.mulMap_comp_rTensor
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' = y
⊢ x' = y'

Tactic:
exact (H M' hM hFG).injective (by simp [← mulMap_comp_rTensor _ hM, hx', hy', hxy])

Premises used: Submodule.LinearDisjoint.injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
obtain :
  ∀ (N' : Submodule R S) (hN : N' ≤ N) (hFG : Module.Finite.{u, v} R ↥N')
    (h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))), x = y
⊢ x = y

Tactic:
obtain ⟨N', hN, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_right_of_setFinite' {x, y} (Set.toFinite _)

Premises used: Insert.insert, TensorProduct.exists_finite_submodule_right_of_setFinite', Set.toFinite, Singleton.singleton