awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
M : Type u_1
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : M ⊗[R] N
⊢ ∃ (P : Submodule R M), P.FG ∧ Membership.mem (γ := Submodule R (M ⊗[R] N)) (range (rTensor N P.subtype)) u
have let : ∀ (P : { P : Submodule R M // P.FG }) (t : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
  (ht :
    Eq (α :=
      Module.DirectLimit (R := R)
        (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
        fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
      (((Module.DirectLimit.of R { P : Submodule R M // P.FG }
                (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
                (fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) P :
              TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N →ₗ[R]
                Module.DirectLimit (R := R)
                  (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
                  fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) :
            (a : ↥(↑P : Submodule R M) ⊗[R] N) →
              Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
                fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
          t :
        Module.DirectLimit (R := R)
          (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
          fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
      ((LinearEquiv.symm (FG.rTensor.directLimit R M N) :
            (a : M ⊗[R] N) →
              Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
                fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
          u :
        Module.DirectLimit (R := R)
          (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
          fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))),
  ∃ (P : Submodule R M), P.FG ∧ Membership.mem (γ := Submodule R (M ⊗[R] N)) (range (rTensor N P.subtype)) u
Tactic: let ⟨P, t, ht⟩ := Module.DirectLimit.exists_of ((Submodule.FG.rTensor.directLimit R M N).symm u)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
M : Type u_1
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : M ⊗[R] N
P : { P : Submodule R M // P.FG }
t : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N
ht :
  Eq (α :=
    Module.DirectLimit (R := R)
      (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
      fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
    (((Module.DirectLimit.of R { P : Submodule R M // P.FG }
              (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
              (fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) P :
            TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N →ₗ[R]
              Module.DirectLimit (R := R)
                (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
                fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) :
          (a : ↥(↑P : Submodule R M) ⊗[R] N) →
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
              fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
        t :
      Module.DirectLimit (R := R)
        (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
        fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
    ((LinearEquiv.symm (FG.rTensor.directLimit R M N) :
          (a : M ⊗[R] N) →
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
              fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
        u :
      Module.DirectLimit (R := R)
        (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
        fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
⊢ ∃ (P : Submodule R M), P.FG ∧ Membership.mem (γ := Submodule R (M ⊗[R] N)) (range (rTensor N P.subtype)) u
have h : (rTensor N (↑P : Submodule R M).subtype : (a : ↥(↑P : Submodule R M) ⊗[R] N) → M ⊗[R] N) t = u
Tactic: use P.val, P.property, t
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
M : Type u_1
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : M ⊗[R] N
⊢ ∃ (P : Submodule R M), P.FG ∧ Membership.mem (γ := Submodule R (M ⊗[R] N)) (range (rTensor N P.subtype)) u
have let : ∀ (P : { P : Submodule R M // P.FG }) (t : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
  (ht :
    Eq (α :=
      Module.DirectLimit (R := R)
        (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
        fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
      (((Module.DirectLimit.of R { P : Submodule R M // P.FG }
                (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
                (fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) P :
              TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N →ₗ[R]
                Module.DirectLimit (R := R)
                  (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
                  fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) :
            (a : ↥(↑P : Submodule R M) ⊗[R] N) →
              Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
                fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
          t :
        Module.DirectLimit (R := R)
          (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
          fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
      ((LinearEquiv.symm (FG.rTensor.directLimit R M N) :
            (a : M ⊗[R] N) →
              Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
                fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
          u :
        Module.DirectLimit (R := R)
          (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
          fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))),
  ∃ (P : Submodule R M), P.FG ∧ Membership.mem (γ := Submodule R (M ⊗[R] N)) (range (rTensor N P.subtype)) u
Tactic: classical
  let ⟨P, t, ht⟩ := Module.DirectLimit.exists_of ((Submodule.FG.rTensor.directLimit R M N).symm u)
  use P.val, P.property, t
  rw [← Submodule.FG.rTensor.directLimit_apply, ht, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (hypothesis)
Goal:
R : Type u
M : Type u_1
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
h : Eq (α := M ⊗[R] N) ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N) (0 : M ⊗[R] N)
⊢ ∃ (Q : Submodule R M) (hPQ : P ≤ Q),
    Q.FG ∧
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
        (0 : TensorProduct.{u, u_1, u_2} R (↥Q) N)
have h₁ : Eq (α := M ⊗[R] N) ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
  ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) 0 : M ⊗[R] N)
Tactic: rw [← (rTensor N P.subtype).map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (hypothesis)
Goal:
R : Type u
M : Type u_1
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
P' : Submodule R M
hP' : P'.FG
t' : TensorProduct.{u, u_1, u_2} R (↥P') N
h :
  Eq (α := M ⊗[R] N) ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
    ((rTensor N P'.subtype : (a : ↥P' ⊗[R] N) → M ⊗[R] N) t' : M ⊗[R] N)
⊢ ∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
    Q.FG ∧
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hP'Q) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)
have h₁ : Eq (α := M ⊗[R] N)
  ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
      ((rTensor N (inclusion sorry) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
    M ⊗[R] N)
  ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
      ((rTensor N (inclusion sorry) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
    M ⊗[R] N)
Tactic: simp only [← subtype_comp_inclusion _ _ (le_sup_left : _ ≤ P ⊔ P'),
    ← subtype_comp_inclusion _ _ (le_sup_right : _ ≤ P ⊔ P'),
    rTensor_comp, coe_comp, Function.comp_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
M : Type u_1
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
P' : Submodule R M
hP' : P'.FG
t' : TensorProduct.{u, u_1, u_2} R (↥P') N
h :
  Eq (α := M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      M ⊗[R] N)
⊢ ∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
    Q.FG ∧
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hP'Q) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)
have let : ∀ (Q : Submodule R M) (hQ_le : P ⊔ P' ≤ Q) (hQ : Q.FG)
  (h :
    Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
      ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
          ((rTensor N (inclusion sorry) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
        TensorProduct.{u, u_1, u_2} R (↥Q) N)
      ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
          ((rTensor N (inclusion sorry) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
        TensorProduct.{u, u_1, u_2} R (↥Q) N)),
  ∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
    Q.FG ∧
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hP'Q) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)
Tactic: let ⟨Q, hQ_le, hQ, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq (hP.sup hP') h
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
M : Type u_1
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
P' : Submodule R M
hP' : P'.FG
t' : TensorProduct.{u, u_1, u_2} R (↥P') N
h_1 :
  Eq (α := M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      M ⊗[R] N)
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      TensorProduct.{u, u_1, u_2} R (↥Q) N)
⊢ ∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
    Q.FG ∧
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hP'Q) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)
have right : Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
  ((rTensor N (inclusion sorry) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
  ((rTensor N (inclusion sorry) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)
Tactic: use Q, le_trans le_sup_left hQ_le, le_trans le_sup_right hQ_le, hQ
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : S ⊗[R] N
⊢ ∃ (A : Subalgebra R S), A.FG ∧ Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N A.val.toLinearMap)) u
have obtain : ∀ (P : Submodule R S) (hu : Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N P.subtype)) u) (s : Finset S)
  (hs : span R (↑s : Set S) = P),
  ∃ (A : Subalgebra R S), A.FG ∧ Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N A.val.toLinearMap)) u
Tactic: obtain ⟨P, ⟨s, hs⟩, hu⟩ := TensorProduct.exists_of_fg u
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N P.subtype)) u
s : Finset S
hs : span R (↑s : Set S) = P
⊢ ∃ (A : Subalgebra R S), A.FG ∧ Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N A.val.toLinearMap)) u
have right : Membership.mem (γ := Submodule R (S ⊗[R] N))
  (range (M := TensorProduct.{u_1, u_2, u_4} R (↥(Algebra.adjoin R (↑s : Set S))) N)
    (rTensor N (AlgHom.toLinearMap (Subalgebra.val (Algebra.adjoin R (↑s : Set S))))))
  u
Tactic: use Algebra.adjoin R s, Subalgebra.fg_adjoin_finset _
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N P.subtype)) u
s : Finset S
hs : span R (↑s : Set S) = P
⊢ P ≤ (Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S))
have simp : (↑s : Set S) ⊆ (↑(Algebra.adjoin R (↑s : Set S)) : Set S)
Tactic: simp only [← hs, span_le, Subalgebra.coe_toSubmodule]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (hypothesis)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N P.subtype)) u
s : Finset S
hs : span R (↑s : Set S) = P
⊢ Membership.mem (γ := Submodule R (S ⊗[R] N))
    (range (M := TensorProduct.{u_1, u_2, u_4} R (↥(Algebra.adjoin R (↑s : Set S))) N)
      (rTensor N (AlgHom.toLinearMap (Subalgebra.val (Algebra.adjoin R (↑s : Set S))))))
    u
have this : P ≤ (Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S))
Tactic: have : P ≤ (Algebra.adjoin R (s : Set S)).toSubmodule := by
    simp only [← hs, span_le, Subalgebra.coe_toSubmodule]
    exact Algebra.subset_adjoin
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (hypothesis)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N P.subtype)) u
s : Finset S
hs : span R (↑s : Set S) = P
this : P ≤ (Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S))
⊢ Membership.mem (γ := Submodule R (S ⊗[R] N))
    (range (M := TensorProduct.{u_1, u_2, u_4} R (↥(Algebra.adjoin R (↑s : Set S))) N)
      (rTensor N (AlgHom.toLinearMap (Subalgebra.val (Algebra.adjoin R (↑s : Set S))))))
    u
have hu₁ : Membership.mem (γ := Submodule R (S ⊗[R] N))
  (range
    (rTensor N
        (Submodule.subtype
          ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S)))) ∘ₗ
      rTensor N (inclusion this)))
  u
Tactic: rw [← subtype_comp_inclusion P _ this, rTensor_comp] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
⊢ (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
have H : ∀ (x : ↥A),
  Eq (α := S) (((A ⊔ A').val.comp (Subalgebra.inclusion sorry) : (a : ↥A) → S) x : S) ((A.val : (a : ↥A) → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (hypothesis)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
⊢ ∃ (B : Subalgebra R S) (hAB : A ≤ B) (hA'B : A' ≤ B),
    B.FG ∧
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) t :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥A' ⊗[R] N) → ↥B ⊗[R] N) t' :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
have hj : (A ⊔ A').val.comp (Subalgebra.inclusion sorry) = A.val
Tactic: have hj : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_left) = A.val := by ext; rfl
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
⊢ (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
have H : ∀ (x : ↥A'),
  Eq (α := S) (((A ⊔ A').val.comp (Subalgebra.inclusion sorry) : (a : ↥A') → S) x : S) ((A'.val : (a : ↥A') → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (hypothesis)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
⊢ ∃ (B : Subalgebra R S) (hAB : A ≤ B) (hA'B : A' ≤ B),
    B.FG ∧
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) t :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥A' ⊗[R] N) → ↥B ⊗[R] N) t' :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
have hj' : (A ⊔ A').val.comp (Subalgebra.inclusion sorry) = A'.val
Tactic: have hj' : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_right) = A'.val := by ext; rfl
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (hypothesis)
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
⊢ ∃ (B : Subalgebra R S) (hAB : A ≤ B) (hA'B : A' ≤ B),
    B.FG ∧
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) t :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥A' ⊗[R] N) → ↥B ⊗[R] N) t' :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
have h₁ : Eq (α := S ⊗[R] N)
  ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
      ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion sorry)) : (a : ↥A ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t) :
    S ⊗[R] N)
  ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
      ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion sorry)) : (a : ↥A' ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t') :
    S ⊗[R] N)
Tactic: simp only [← hj, ← hj', AlgHom.comp_toLinearMap, rTensor_comp, comp_apply] at h
Cleared hypotheses: h