internlm/Lean-Github huggingface dataset:
Theorem: TensorProduct.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
have := Module.DirectLimit.of.zero_exact h
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
let ⟨Q, hPQ, h⟩ := this
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
Q : Submodules_fg R M
hPQ : ⟨P, hP⟩ ≤ Q
h : (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ Q hPQ)) (t - t') = 0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
Q : Submodules_fg R M
hPQ : ⟨P, hP⟩ ≤ Q
h : (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ Q hPQ)) (t - t') = 0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
use Q.val, Subtype.coe_le_coe.mpr hPQ, Q.property
Proof state after:
case right
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
Q : Submodules_fg R M
hPQ : ⟨P, hP⟩ ≤ Q
h : (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ Q hPQ)) (t - t') = 0
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq
Proof state before:
case right
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
Q : Submodules_fg R M
hPQ : ⟨P, hP⟩ ≤ Q
h : (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ Q hPQ)) (t - t') = 0
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Tactic:
simpa only [sub_eq_zero, map_sub] using h
Proof state after:
no goals
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
let P'' := P ⊔ P'
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
let _hP_le := (le_sup_left : P ≤ P'')
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
let _hP'_le := (le_sup_right : P' ≤ P'')
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
rw [← Submodule.subtype_comp_inclusion _ _ _hP_le] at h
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
h : (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP_le)) t = (LinearMap.rTensor N P'.subtype) t'
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
h : (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP_le)) t = (LinearMap.rTensor N P'.subtype) t'
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
rw [← Submodule.subtype_comp_inclusion _ _ _hP'_le] at h
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h :
  (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP_le)) t =
    (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP'_le)) t'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h :
  (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP_le)) t =
    (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP'_le)) t'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
simp only [LinearMap.rTensor_comp, LinearMap.coe_comp, Function.comp_apply] at h
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
let ⟨Q, hQ_le, hQ, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq
  (Submodule.FG.sup hP hP') _ _ h
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
use Q, le_trans _hP_le hQ_le, le_trans _hP'_le hQ_le, hQ
Proof state after:
case right
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
case right
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Tactic:
simp only [← LinearMap.comp_apply, ← LinearMap.rTensor_comp, Submodule.subtype_comp_inclusion] at h
Proof state after:
case right
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le ∘ₗ Submodule.inclusion _hP_le)) t =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le ∘ₗ Submodule.inclusion _hP'_le)) t'
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Theorem: TensorProduct.eq_of_fg_of_subtype_eq'
Proof state before:
case right
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le ∘ₗ Submodule.inclusion _hP_le)) t =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le ∘ₗ Submodule.inclusion _hP'_le)) t'
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Tactic:
exact h
Proof state after:
no goals
Theorem: TensorProduct.Algebra.exists_of_fg
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)
Tactic:
let ⟨P, hP, ht⟩ := TensorProduct.exists_of_fg t
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
hP : P.FG
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)
Theorem: TensorProduct.Algebra.exists_of_fg
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
hP : P.FG
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)
Tactic:
obtain ⟨s, hs⟩ := hP
Proof state after:
case intro
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)
Theorem: TensorProduct.Algebra.exists_of_fg
Proof state before:
case intro
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)
Tactic:
use Algebra.adjoin R s, Subalgebra.fg_adjoin_finset _
Proof state after:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)
Theorem: TensorProduct.Algebra.exists_of_fg
Proof state before:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)
Tactic:
have : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R (s : Set S)) := by
  simp only [← hs, Submodule.span_le, Subalgebra.coe_toSubmodule]
  exact Algebra.subset_adjoin
Proof state after:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)