internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.hasSum_of_monomials_self
Proof state before:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
⊢ HasSum (fun d => (monomial α d) ((coeff α d) f)) f
Tactic:
rw [← (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.hasSum_iff]
Proof state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
⊢ HasSum ((fun d => (monomial α d) ((coeff α d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) f
Theorem: PowerSeries.hasSum_of_monomials_self
Proof state before:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
⊢ HasSum ((fun d => (monomial α d) ((coeff α d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) f
Tactic:
convert MvPowerSeries.hasSum_of_monomials_self f
Proof state after:
case h.e'_5.h.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ ((fun d => (monomial α d) ((coeff α d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) x✝ =
    (MvPowerSeries.monomial α x✝) ((MvPowerSeries.coeff α x✝) f)
Theorem: PowerSeries.hasSum_of_monomials_self
Proof state before:
case h.e'_5.h.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ ((fun d => (monomial α d) ((coeff α d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) x✝ =
    (MvPowerSeries.monomial α x✝) ((MvPowerSeries.coeff α x✝) f)
Tactic:
simp only [LinearEquiv.coe_toEquiv, comp_apply, monomial, coeff,
  Finsupp.LinearEquiv.finsuppUnique_apply, PUnit.default_eq_unit]
Proof state after:
case h.e'_5.h.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ (MvPowerSeries.monomial α (Finsupp.single () (x✝ PUnit.unit)))
      ((MvPowerSeries.coeff α (Finsupp.single () (x✝ PUnit.unit))) f) =
    (MvPowerSeries.monomial α x✝) ((MvPowerSeries.coeff α x✝) f)
Theorem: PowerSeries.hasSum_of_monomials_self
Proof state before:
case h.e'_5.h.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ (MvPowerSeries.monomial α (Finsupp.single () (x✝ PUnit.unit)))
      ((MvPowerSeries.coeff α (Finsupp.single () (x✝ PUnit.unit))) f) =
    (MvPowerSeries.monomial α x✝) ((MvPowerSeries.coeff α x✝) f)
Tactic:
congr
Proof state after:
case h.e'_5.h.h.h.e_5.h.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝

case h.e'_5.h.h.h.e_6.h.e_a.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝
Theorem: PowerSeries.hasSum_of_monomials_self
Proof state before:
case h.e'_5.h.h.h.e_5.h.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝

case h.e'_5.h.h.h.e_6.h.e_a.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝
Tactic:
all_goals { ext ; simp }
Proof state after:
no goals
Theorem: PowerSeries.hasSum_of_monomials_self
Proof state before:
case h.e'_5.h.h.h.e_6.h.e_a.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝
Tactic:
ext
Proof state after:
case h.e'_5.h.h.h.e_6.h.e_a.e_n.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ (Finsupp.single () (x✝ PUnit.unit)) default = x✝ default
Theorem: PowerSeries.hasSum_of_monomials_self
Proof state before:
case h.e'_5.h.h.h.e_6.h.e_a.e_n.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ (Finsupp.single () (x✝ PUnit.unit)) default = x✝ default
Tactic:
simp
Proof state after:
no goals
Theorem: rTensor_fgEquiv_of
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
⊢ (rTensor_fgEquiv R M N)
      ((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)
        u) =
    (LinearMap.rTensor N (↑P).subtype) u
Tactic:
suffices (rTensor_fgEquiv R M N).toLinearMap.comp
    (Module.DirectLimit.of R (Submodules_fg R M) (fun P ↦ P.val ⊗[R] N)
      (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P)
    = LinearMap.rTensor N (Submodule.subtype P.val) by
  exact DFunLike.congr_fun this u
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
⊢ ↑(rTensor_fgEquiv R M N) ∘ₗ
      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 =
    LinearMap.rTensor N (↑P).subtype
Theorem: rTensor_fgEquiv_of
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
⊢ ↑(rTensor_fgEquiv R M N) ∘ₗ
      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 =
    LinearMap.rTensor N (↑P).subtype
Tactic:
ext p n
Proof state after:
case a.h.h
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (↑(rTensor_fgEquiv R M N) ∘ₗ
            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))
        p)
      n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (↑P).subtype)) p) n
Theorem: rTensor_fgEquiv_of
Proof state before:
case a.h.h
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (↑(rTensor_fgEquiv R M N) ∘ₗ
            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))
        p)
      n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (↑P).subtype)) p) n
Tactic:
simp only [rTensor_fgEquiv, AlgebraTensorModule.curry_apply, curry_apply,
  LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  LinearEquiv.trans_apply, directLimitLeft_symm_of_tmul, LinearEquiv.rTensor_tmul,
  LinearMap.rTensor_tmul, Submodule.coeSubtype]
Proof state after:
case a.h.h
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_equiv R M)
        ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i)
            (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ) P)
          p) ⊗ₜ[R]
      n =
    ↑p ⊗ₜ[R] n
Theorem: rTensor_fgEquiv_of
Proof state before:
case a.h.h
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_equiv R M)
        ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i)
            (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ) P)
          p) ⊗ₜ[R]
      n =
    ↑p ⊗ₜ[R] n
Tactic:
congr
Proof state after:
case a.h.h.e_m
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_equiv R M)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Theorem: rTensor_fgEquiv_of
Proof state before:
case a.h.h.e_m
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_equiv R M)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Tactic:
simp only [Submodules_fg_equiv, LinearEquiv.ofBijective_apply]
Proof state after:
case a.h.h.e_m
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_map R M)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Theorem: rTensor_fgEquiv_of
Proof state before:
case a.h.h.e_m
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_map R M)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Tactic:
simp only [Submodules_fg_map]
Proof state after:
case a.h.h.e_m
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Module.DirectLimit.lift R (Submodules_fg R M) (fun P => ↥↑P) (Submodules_fg_inclusion R M) (fun P => (↑P).subtype) ⋯)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Theorem: rTensor_fgEquiv_of
Proof state before:
case a.h.h.e_m
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Module.DirectLimit.lift R (Submodules_fg R M) (fun P => ↥↑P) (Submodules_fg_inclusion R M) (fun P => (↑P).subtype) ⋯)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Tactic:
simp only [Module.DirectLimit.lift_of]
Proof state after:
case a.h.h.e_m
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (↑P).subtype p = ↑p
Theorem: rTensor_fgEquiv_of
Proof state before:
case a.h.h.e_m
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (↑P).subtype p = ↑p
Tactic:
simp only [Submodule.coeSubtype]
Proof state after:
no goals
Theorem: rTensor_fgEquiv_of
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 : Submodules_fg R M
u : ↥↑P ⊗[R] N
this :
  ↑(rTensor_fgEquiv R M N) ∘ₗ
      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 =
    LinearMap.rTensor N (↑P).subtype
⊢ (rTensor_fgEquiv R M N)
      ((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)
        u) =
    (LinearMap.rTensor N (↑P).subtype) u
Tactic:
exact DFunLike.congr_fun this u
Proof state after:
no goals
Theorem: rTensor_fg_directedSystem
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 : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP)) p = p
Tactic:
rw [← LinearMap.id_apply (R := R) 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 : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP)) (LinearMap.id p) = LinearMap.id p
Theorem: rTensor_fg_directedSystem
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 : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP)) (LinearMap.id p) = LinearMap.id p
Tactic:
apply DFunLike.congr_fun
Proof state after:
case h₁
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 : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP) = LinearMap.id
Theorem: rTensor_fg_directedSystem
Proof state before:
case h₁
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 : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP) = LinearMap.id
Tactic:
ext p n
Proof state after:
case h₁.a.h.h
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 : Submodules_fg R M
p✝ : ↥↑P ⊗[R] N
hP : P ≤ P
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP))) p) n =
    ((AlgebraTensorModule.curry LinearMap.id) p) n
Theorem: rTensor_fg_directedSystem
Proof state before:
case h₁.a.h.h
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 : Submodules_fg R M
p✝ : ↥↑P ⊗[R] N
hP : P ≤ P
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP))) p) n =
    ((AlgebraTensorModule.curry LinearMap.id) p) n
Tactic:
rfl
Proof state after:
no goals
Theorem: rTensor_fg_directedSystem
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ))
      ((LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P Q hPQ)) p) =
    (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)) p
Tactic:
rw [← LinearMap.comp_apply, ← LinearMap.rTensor_comp]
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ)) p =
    (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)) p
Theorem: rTensor_fg_directedSystem
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ)) p =
    (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)) p
Tactic:
apply DFunLike.congr_fun
Proof state after:
case h₁
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ) =
    LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)
Theorem: rTensor_fg_directedSystem
Proof state before:
case h₁
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ) =
    LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)
Tactic:
ext p n
Proof state after:
case h₁.a.h.h
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p✝ : ↥↑P ⊗[R✝] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ)))
        p)
      n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯))) p) n
Theorem: rTensor_fg_directedSystem
Proof state before:
case h₁.a.h.h
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p✝ : ↥↑P ⊗[R✝] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ)))
        p)
      n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯))) p) n
Tactic:
simp
Proof state after:
case h₁.a.h.h
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p✝ : ↥↑P ⊗[R✝] N
p : ↥↑P
n : N
⊢ (Submodules_fg_inclusion R✝ M Q R hRQ) ((Submodules_fg_inclusion R✝ M P Q hPQ) p) ⊗ₜ[R✝] n =
    (Submodules_fg_inclusion R✝ M P R ⋯) p ⊗ₜ[R✝] n
Theorem: rTensor_fg_directedSystem
Proof state before:
case h₁.a.h.h
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 Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p✝ : ↥↑P ⊗[R✝] N
p : ↥↑P
n : N
⊢ (Submodules_fg_inclusion R✝ M Q R hRQ) ((Submodules_fg_inclusion R✝ M P Q hPQ) p) ⊗ₜ[R✝] n =
    (Submodules_fg_inclusion R✝ M P R ⋯) p ⊗ₜ[R✝] n
Tactic:
rfl
Proof state after:
no goals
Theorem: TensorProduct.exists_of_fg
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
t : M ⊗[R] N
⊢ ∃ P, P.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
Tactic:
let ⟨P, u, hu⟩ := Module.DirectLimit.exists_of ((rTensor_fgEquiv R M N).symm t)
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
t : M ⊗[R] N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
hu :
  (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)
      u =
    (rTensor_fgEquiv R M N).symm t
⊢ ∃ P, P.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
Theorem: TensorProduct.exists_of_fg
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
t : M ⊗[R] N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
hu :
  (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)
      u =
    (rTensor_fgEquiv R M N).symm t
⊢ ∃ P, P.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
Tactic:
use P.val, P.property, u
Proof state after:
case h
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
t : M ⊗[R] N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
hu :
  (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)
      u =
    (rTensor_fgEquiv R M N).symm t
⊢ (LinearMap.rTensor N (↑P).subtype) u = t
Theorem: TensorProduct.exists_of_fg
Proof state before:
case h
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
t : M ⊗[R] N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
hu :
  (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)
      u =
    (rTensor_fgEquiv R M N).symm t
⊢ (LinearMap.rTensor N (↑P).subtype) u = t
Tactic:
rw [← rTensor_fgEquiv_of, hu, LinearEquiv.apply_symm_apply]
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 t' : ↥P ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P.subtype) t'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
rw [← sub_eq_zero, ← map_sub, ← rTensor_fgEquiv_of R M N ⟨P,hP⟩,
  LinearEquiv.map_eq_zero_iff] 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 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
⊢ ∃ 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
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
have := rTensor_fg_directedSystem R M N
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))
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'