awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
A : Subalgebra R S
hA : A.FG
ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
u : TensorProduct.{u_1, u_2, u_3} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
this :
  ∀
    (h :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N)),
    ∃ (B : Subalgebra R S),
      B.FG ∧
        ∃ (x : A ≤ B),
          Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
hu'_1 :
  Eq (α := S ⊗[R] N)
    ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      S ⊗[R] N)
    (0 : S ⊗[R] N)
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
      (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
have h : Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((LinearMap.baseChange (↥B) f : (a : ↥B ⊗[R] M) → ↥B ⊗[R] N)
        ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N) ∧
  (rTensor M B.val.toLinearMap : (a : ↥B ⊗[R] M) → S ⊗[R] M)
      ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) =
    t
Tactic: use B, hB, rTensor M (Subalgebra.inclusion hAB).toLinearMap u
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
A : Subalgebra R S
hA : A.FG
ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
u : TensorProduct.{u_1, u_2, u_3} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
this :
  ∀
    (h :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N)),
    ∃ (B : Subalgebra R S),
      B.FG ∧
        ∃ (x : A ≤ B),
          Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
hu'_1 :
  Eq (α := S ⊗[R] N)
    ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      S ⊗[R] N)
    (0 : S ⊗[R] N)
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
      ((LinearMap.baseChange (↥B) f : (a : ↥B ⊗[R] M) → ↥B ⊗[R] N)
          ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) :
        TensorProduct.{u_1, u_2, u_4} R (↥B) N)
      (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N) ∧
    (rTensor M B.val.toLinearMap : (a : ↥B ⊗[R] M) → S ⊗[R] M)
        ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) =
      t
have h : Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
  ((LinearMap.baseChange (↥B) f : (a : ↥B ⊗[R] M) → ↥B ⊗[R] N)
      ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) :
    TensorProduct.{u_1, u_2, u_4} R (↥B) N)
  (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
A : Subalgebra R S
hA : A.FG
ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
u : TensorProduct.{u_1, u_2, u_3} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
this :
  ∀
    (h :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N)),
    ∃ (B : Subalgebra R S),
      B.FG ∧
        ∃ (x : A ≤ B),
          Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
hu'_1 :
  Eq (α := S ⊗[R] N)
    ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      S ⊗[R] N)
    (0 : S ⊗[R] N)
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
h :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((LinearMap.baseChange (↥B) f : (a : ↥B ⊗[R] M) → ↥B ⊗[R] N)
        ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
      ((LinearMap.baseChange (↥B) f : (a : ↥B ⊗[R] M) → ↥B ⊗[R] N)
          ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) :
        TensorProduct.{u_1, u_2, u_4} R (↥B) N)
      (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N) ∧
    (rTensor M B.val.toLinearMap : (a : ↥B ⊗[R] M) → S ⊗[R] M)
        ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) =
      t
have h₁ : (rTensor M B.val.toLinearMap : (a : ↥B ⊗[R] M) → S ⊗[R] M)
    ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) =
  t
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
A : Subalgebra R S
hA : A.FG
ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
u : TensorProduct.{u_1, u_2, u_3} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
this :
  ∀
    (h :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N)),
    ∃ (B : Subalgebra R S),
      B.FG ∧
        ∃ (x : A ≤ B),
          Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
hu'_1 :
  Eq (α := S ⊗[R] N)
    ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      S ⊗[R] N)
    (0 : S ⊗[R] N)
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
h :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((LinearMap.baseChange (↥B) f : (a : ↥B ⊗[R] M) → ↥B ⊗[R] N)
        ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
have h₁ : Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N) 0 0
Tactic: rw [← rTensor_baseChange, hu']
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
A : Subalgebra R S
hA : A.FG
ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
u : TensorProduct.{u_1, u_2, u_3} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
this :
  ∀
    (h :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N)),
    ∃ (B : Subalgebra R S),
      B.FG ∧
        ∃ (x : A ≤ B),
          Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
hu'_1 :
  Eq (α := S ⊗[R] N)
    ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      S ⊗[R] N)
    (0 : S ⊗[R] N)
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ (rTensor M B.val.toLinearMap : (a : ↥B ⊗[R] M) → S ⊗[R] M)
      ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) =
    t
have h : Eq (α := S ⊗[R] M)
  ((rTensor M (B.val.toLinearMap ∘ₗ (Subalgebra.inclusion hAB).toLinearMap) : (a : ↥A ⊗[R] M) → S ⊗[R] M) u : S ⊗[R] M)
  ((rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u : S ⊗[R] M)
Tactic: rw [← comp_apply, ← rTensor_comp, ← hu]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
⊢ ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
      (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
have obtain : ∀ (A : Subalgebra R S) (hA : A.FG)
  (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
  ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
      (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
Tactic: classical
  obtain ⟨A, hA, ht_memA⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨u, hu⟩ := _root_.id ht_memA
  have := TensorProduct.Algebra.eq_of_fg_of_subtype_eq hA (t := f.baseChange _ u) (t' := 0)
  simp only [map_zero, exists_and_left] at this
  have hu' : (A.val.toLinearMap.rTensor N) (f.baseChange (↥A) u) = 0 := by
    rw [← ht, ← hu, rTensor_baseChange]
  obtain ⟨B, hB, hAB, hu'⟩ := this hu'
  use B, hB, rTensor M (Subalgebra.inclusion hAB).toLinearMap u
  constructor
  · rw [← rTensor_baseChange, hu']
  · rw [← comp_apply, ← rTensor_comp, ← hu]
    congr
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
obtain :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
⊢ ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
      (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
have obtain₁ : ∀ (A : Subalgebra R S) (hA : A.FG)
  (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
  (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t),
  ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
      (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
Tactic: classical
  obtain ⟨A, hA, ht_memA⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨u, hu⟩ := _root_.id ht_memA
  have := TensorProduct.Algebra.eq_of_fg_of_subtype_eq hA (t := f.baseChange _ u) (t' := 0)
  simp only [map_zero, exists_and_left] at this
  have hu' : (A.val.toLinearMap.rTensor N) (f.baseChange (↥A) u) = 0 := by
    rw [← ht, ← hu, rTensor_baseChange]
  obtain ⟨B, hB, hAB, hu'⟩ := this hu'
  use B, hB, rTensor M (Subalgebra.inclusion hAB).toLinearMap u
  constructor
  · rw [← rTensor_baseChange, hu']
  · rw [← comp_apply, ← rTensor_comp, ← hu]
    congr
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x₁ x₂ : N ⊗[R] M
ihx₁ :
  ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    x₁ = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
ihx₂ :
  ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    x₂ = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
⊢ ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    x₁ + x₂ = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
have add : ∀ (J₁ : Submodule R N) (fg₁ : J₁.FG) (y₁ : TensorProduct.{u_1, u_3, u_2} R (↥J₁) M),
  ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    HAdd.hAdd (α := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M) x₂ =
      (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
Tactic: obtain ⟨J₁, fg₁, y₁, rfl⟩ := ihx₁
Cleared hypotheses: x₁, ihx₁
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x₂ : N ⊗[R] M
ihx₂ :
  ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    x₂ = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : TensorProduct.{u_1, u_3, u_2} R (↥J₁) M
⊢ ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    HAdd.hAdd (α := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M) x₂ =
      (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
have add : ∀ (J₂ : Submodule R N) (fg₂ : J₂.FG) (y₂ : TensorProduct.{u_1, u_3, u_2} R (↥J₂) M),
  ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
        ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
      (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
Tactic: obtain ⟨J₂, fg₂, y₂, rfl⟩ := ihx₂
Cleared hypotheses: x₂, ihx₂
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : TensorProduct.{u_1, u_3, u_2} R (↥J₁) M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : TensorProduct.{u_1, u_3, u_2} R (↥J₂) M
⊢ ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
        ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
      (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
have add : HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
    ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
  (rTensor M (J₁ ⊔ J₂).subtype : (a : ↥(J₁ ⊔ J₂) ⊗[R] M) → N ⊗[R] M)
    (HAdd.hAdd (α := TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M) (β :=
      TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M)
      ((rTensor M (inclusion sorry) : (a : ↥J₁ ⊗[R] M) → ↥(J₁ ⊔ J₂) ⊗[R] M) y₁ :
        TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M)
      ((rTensor M (inclusion sorry) : (a : ↥J₂ ⊗[R] M) → ↥(J₁ ⊔ J₂) ⊗[R] M) y₂ :
        TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M))
Tactic: refine ⟨J₁ ⊔ J₂, fg₁.sup fg₂,
      rTensor M (J₁.inclusion le_sup_left) y₁ + rTensor M (J₂.inclusion le_sup_right) y₂, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : TensorProduct.{u_1, u_3, u_2} R (↥J₁) M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : TensorProduct.{u_1, u_3, u_2} R (↥J₂) M
⊢ HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
      ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
    (rTensor M (J₁ ⊔ J₂).subtype : (a : ↥(J₁ ⊔ J₂) ⊗[R] M) → N ⊗[R] M)
      (HAdd.hAdd (α := TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M) (β :=
        TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M)
        ((rTensor M (inclusion ⋯) : (a : ↥J₁ ⊗[R] M) → ↥(J₁ ⊔ J₂) ⊗[R] M) y₁ :
          TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M)
        ((rTensor M (inclusion ⋯) : (a : ↥J₂ ⊗[R] M) → ↥(J₁ ⊔ J₂) ⊗[R] M) y₂ :
          TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M))
have add : HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
    ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
  HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M)
    ((rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion sorry) : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
    ((rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion sorry) : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M)
Tactic: rw [map_add, ← rTensor_comp_apply, ← rTensor_comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : N ⊗[R] M
⊢ ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    x = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
have zero : ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
  Eq (α := N ⊗[R] M) (0 : N ⊗[R] M) ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
Tactic: induction x with
  | zero => exact ⟨⊥, fg_bot, 0, rfl⟩
  | tmul i m => exact ⟨R ∙ i, fg_span_singleton i, ⟨i, mem_span_singleton_self _⟩ ⊗ₜ[R] m, rfl⟩
  | add x₁ x₂ ihx₁ ihx₂ =>
    obtain ⟨J₁, fg₁, y₁, rfl⟩ := ihx₁
    obtain ⟨J₂, fg₂, y₂, rfl⟩ := ihx₂
    refine ⟨J₁ ⊔ J₂, fg₁.sup fg₂,
      rTensor M (J₁.inclusion le_sup_left) y₁ + rTensor M (J₂.inclusion le_sup_right) y₂, ?_⟩
    rw [map_add, ← rTensor_comp_apply, ← rTensor_comp_apply]
    rfl
Cleared hypotheses: x