awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∃ (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 tmul : ∀ (i : N) (m : M),
  ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    Eq (α := N ⊗[R] M) (i ⊗ₜ[R] m) ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y)
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
-- 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
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)
tmul :
  ∀ (i : N) (m : M),
    ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
      Eq (α := N ⊗[R] M) (i ⊗ₜ[R] m) ((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 = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
have add : ∀ (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
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
-- 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
s : Set (N ⊗[R] M)
hs : s.Finite
⊢ ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))
have choose : ∀ (J : (x : N ⊗[R] M) → Submodule R N) (fg : ∀ (x : N ⊗[R] M), (J x).FG)
  (y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M)
  (eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)),
  ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))
Tactic: choose J fg y eq using exists_fg_le_eq_rTensor_subtype (R := R) (M := M) (N := N)
-- 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
s : Set (N ⊗[R] M)
hs : s.Finite
J : (x : N ⊗[R] M) → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)
⊢ ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))
have rw : ∀ (hs : Finite (↑s : Type (max u_2 u_3))) (J : (x : N ⊗[R] M) → Submodule R N) (fg : ∀ (x : N ⊗[R] M), (J x).FG)
  (y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M)
  (eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)),
  ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))
Tactic: rw [← Set.finite_coe_iff] at hs
Cleared hypotheses: hs, J, fg, y, eq
-- 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
s : Set (N ⊗[R] M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : N ⊗[R] M) → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)
⊢ ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))
have refine : ∀ (x : N ⊗[R] M) (hx : x ∈ s),
  Eq (α := N ⊗[R] M)
    ((rTensor M (Submodule.subtype (⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M))) :
          (a : ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ⊗[R] M) → N ⊗[R] M)
        (((rTensor M (inclusion sorry) :
              TensorProduct.{u_1, u_3, u_2} R (↥(J (↑(Subtype.mk (p := fun (x : N ⊗[R] M) ↦ x ∈ s) x hx) : N ⊗[R] M)))
                  M →ₗ[R]
                TensorProduct.{u_1, u_3, u_2} R (↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M))) M) :
            (a : ↥(J (↑⟨x, hx⟩ : N ⊗[R] M)) ⊗[R] M) → ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ⊗[R] M)
          (y x)) :
      N ⊗[R] M)
    ((rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x) : N ⊗[R] M)
Tactic: refine ⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, fun x hx ↦
    ⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩
-- 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
s : Set (N ⊗[R] M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : N ⊗[R] M) → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ Eq (α := N ⊗[R] M)
    ((rTensor M (Submodule.subtype (⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M))) :
          (a : ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ⊗[R] M) → N ⊗[R] M)
        (((rTensor M (inclusion ⋯) :
              TensorProduct.{u_1, u_3, u_2} R (↥(J (↑(Subtype.mk (p := fun (x : N ⊗[R] M) ↦ x ∈ s) x hx) : N ⊗[R] M)))
                  M →ₗ[R]
                TensorProduct.{u_1, u_3, u_2} R (↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M))) M) :
            (a : ↥(J (↑⟨x, hx⟩ : N ⊗[R] M)) ⊗[R] M) → ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ⊗[R] M)
          (y x)) :
      N ⊗[R] M)
    ((rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x) : N ⊗[R] M)
have rw : Eq (α := N ⊗[R] M)
  (((rTensor M (Submodule.subtype (⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ∘ₗ inclusion sorry) :
          TensorProduct.{u_1, u_3, u_2} R (↥(J (↑(Subtype.mk (p := fun (x : N ⊗[R] M) ↦ x ∈ s) x hx) : N ⊗[R] M)))
              M →ₗ[R]
            N ⊗[R] M) :
        (a : ↥(J (↑⟨x, hx⟩ : N ⊗[R] M)) ⊗[R] M) → N ⊗[R] M)
      (y x) :
    N ⊗[R] M)
  ((rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x) : N ⊗[R] M)
Tactic: rw [← comp_apply, ← rTensor_comp]
-- 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
I : Submodule R N
x : TensorProduct.{u_1, u_3, u_2} R (↥I) M
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    x = (rTensor M (inclusion hle) : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y
have obtain : ∀ (J : Submodule R ↥I) (fg : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
  ∃ (J_1 : Submodule R N) (_ : J_1.FG) (hle : J_1 ≤ I) (y_1 : TensorProduct.{u_1, u_3, u_2} R (↥J_1) M),
    Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M (inclusion hle) : (a : ↥J_1 ⊗[R] M) → ↥I ⊗[R] M) y_1 : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
Tactic: obtain ⟨J, fg, y, rfl⟩ := exists_fg_le_eq_rTensor_subtype x
Cleared hypotheses: x
-- 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
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : TensorProduct.{u_1, u_3, u_2} R (↥J) M
⊢ ∃ (J_1 : Submodule R N) (_ : J_1.FG) (hle : J_1 ≤ I) (y_1 : TensorProduct.{u_1, u_3, u_2} R (↥J_1) M),
    Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M (inclusion hle) : (a : ↥J_1 ⊗[R] M) → ↥I ⊗[R] M) y_1 : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
have refine : Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
  ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
  ((rTensor M (inclusion sorry) : (a : ↥(map I.subtype J) ⊗[R] M) → ↥I ⊗[R] M)
      ((rTensor M (I.subtype.submoduleMap J) : (a : ↥J ⊗[R] M) → ↥(map I.subtype J) ⊗[R] M) y) :
    TensorProduct.{u_1, u_3, u_2} R (↥I) M)
Tactic: refine ⟨J.map I.subtype, fg.map _, I.map_subtype_le J, rTensor M (I.subtype.submoduleMap J) 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
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : TensorProduct.{u_1, u_3, u_2} R (↥J) M
⊢ Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion ⋯) : (a : ↥(map I.subtype J) ⊗[R] M) → ↥I ⊗[R] M)
        ((rTensor M (I.subtype.submoduleMap J) : (a : ↥J ⊗[R] M) → ↥(map I.subtype J) ⊗[R] M) y) :
      TensorProduct.{u_1, u_3, u_2} R (↥I) M)
have rw : Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
  ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
  ((rTensor M (inclusion sorry ∘ₗ I.subtype.submoduleMap J) : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y :
    TensorProduct.{u_1, u_3, u_2} R (↥I) M)
Tactic: rw [← LinearMap.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
I : Submodule R N
s : Set (TensorProduct.{u_1, u_3, u_2} R (↥I) M)
hs : s.Finite
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))
have choose : ∀ (J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N)
  (fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG)
  (hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I)
  (y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M)
  (eq :
    ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M),
      x = (rTensor M (inclusion sorry) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)),
  ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))
Tactic: choose J fg hle y eq using exists_fg_le_eq_rTensor_inclusion (M := M) (I := I)
-- 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
I : Submodule R N
s : Set (TensorProduct.{u_1, u_3, u_2} R (↥I) M)
hs : s.Finite
J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N
fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG
hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I
y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), x = (rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))
have rw : ∀ (hs : Finite (↑s : Type (max u_2 u_3))) (J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N)
  (fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG)
  (hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I)
  (y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M)
  (eq :
    ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M),
      x = (rTensor M (inclusion sorry) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)),
  ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))
Tactic: rw [← Set.finite_coe_iff] at hs
Cleared hypotheses: hs, J, fg, hle, y, eq
-- 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
I : Submodule R N
s : Set (TensorProduct.{u_1, u_3, u_2} R (↥I) M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N
fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG
hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I
y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), x = (rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))
have refine : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) (hx : x ∈ s),
  Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion sorry) : (a : ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M)) ⊗[R] M) → ↥I ⊗[R] M)
        (((rTensor M (inclusion sorry) :
              TensorProduct.{u_1, u_3, u_2} R
                  (↥(J
                      (↑(Subtype.mk (p := fun (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) ↦ x ∈ s) x hx) : ↥I ⊗[R] M)))
                  M →ₗ[R]
                TensorProduct.{u_1, u_3, u_2} R (↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M))) M) :
            (a : ↥(J (↑⟨x, hx⟩ : ↥I ⊗[R] M)) ⊗[R] M) → ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M)) ⊗[R] M)
          (y x)) :
      TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion sorry) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x) : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
Tactic: refine ⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, iSup_le fun _ ↦ hle _, fun x hx ↦
    ⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩
-- 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
I : Submodule R N
s : Set (TensorProduct.{u_1, u_3, u_2} R (↥I) M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N
fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG
hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I
y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), x = (rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)
x : TensorProduct.{u_1, u_3, u_2} R (↥I) M
hx : x ∈ s
⊢ Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion ⋯) : (a : ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M)) ⊗[R] M) → ↥I ⊗[R] M)
        (((rTensor M (inclusion ⋯) :
              TensorProduct.{u_1, u_3, u_2} R
                  (↥(J
                      (↑(Subtype.mk (p := fun (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) ↦ x ∈ s) x hx) : ↥I ⊗[R] M)))
                  M →ₗ[R]
                TensorProduct.{u_1, u_3, u_2} R (↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M))) M) :
            (a : ↥(J (↑⟨x, hx⟩ : ↥I ⊗[R] M)) ⊗[R] M) → ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M)) ⊗[R] M)
          (y x)) :
      TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x) : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
have rw : Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
  (((rTensor M (inclusion sorry ∘ₗ inclusion sorry) :
          TensorProduct.{u_1, u_3, u_2} R
              (↥(J (↑(Subtype.mk (p := fun (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) ↦ x ∈ s) x hx) : ↥I ⊗[R] M)))
              M →ₗ[R]
            TensorProduct.{u_1, u_3, u_2} R (↥I) M) :
        (a : ↥(J (↑⟨x, hx⟩ : ↥I ⊗[R] M)) ⊗[R] M) → ↥I ⊗[R] M)
      (y x) :
    TensorProduct.{u_1, u_3, u_2} R (↥I) M)
  ((rTensor M (inclusion sorry) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x) : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
Tactic: rw [← comp_apply, ← rTensor_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
h : Module.Finite R M
⊢ Module.Finite A (TensorProduct R A M)
have obtain : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤), Module.Finite A (TensorProduct R A M)
Tactic: obtain ⟨s, hs⟩ := h.fg_top
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
h : Module.Finite R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
⊢ Module.Finite A (TensorProduct R A M)
have refine : LE.le (α := Submodule A (TensorProduct R A M)) ⊤
  (Submodule.span A
    (↑(Finset.image
          (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] TensorProduct R A M) 1) : (a : M) → TensorProduct R A M) s) :
      Set (TensorProduct R A M)))
Tactic: refine ⟨⟨s.image (TensorProduct.mk R A M 1), eq_top_iff.mpr ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
h : Module.Finite R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
x : A
y : M
⊢ Membership.mem (γ := Submodule A (TensorProduct R A M))
    (Submodule.span A
      (↑(Finset.image
            (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] TensorProduct R A M) 1) : (a : M) → TensorProduct R A M) s) :
        Set (TensorProduct R A M)))
    (x ⊗ₜ[R] y)
have tmul : Membership.mem (γ := Submodule A (TensorProduct R A M))
  (Submodule.span A
    (Set.range (ι := M)
      (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] TensorProduct R A M) 1) : (a : M) → TensorProduct R A M)))
  (HSMul.hSMul (β := TensorProduct R A M) x (1 ⊗ₜ[R] y))
Tactic: rw [Finset.coe_image, ← Submodule.span_span_of_tower R, Submodule.span_image, hs,
        Submodule.map_top, LinearMap.coe_range, ← mul_one x, ← smul_eq_mul,
        ← TensorProduct.smul_tmul']
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
h : Module.Finite R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
x : TensorProduct R A M
⊢ Membership.mem (γ := Submodule A (TensorProduct R A M))
    (Submodule.span A
      (↑(Finset.image
            (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] TensorProduct R A M) 1) : (a : M) → TensorProduct R A M) s) :
        Set (TensorProduct R A M)))
    x
have zero : Membership.mem (γ := Submodule A (TensorProduct R A M))
  (Submodule.span A
    (↑(Finset.image
          (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] TensorProduct R A M) 1) : (a : M) → TensorProduct R A M) s) :
      Set (TensorProduct R A M)))
  0
Tactic: induction x with
    | zero => exact zero_mem _
    | tmul x y =>
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, Submodule.span_image, hs,
        Submodule.map_top, LinearMap.coe_range, ← mul_one x, ← smul_eq_mul,
        ← TensorProduct.smul_tmul']
      exact Submodule.smul_mem _ x (Submodule.subset_span <| Set.mem_range_self y)
    | add x y hx hy => exact Submodule.add_mem _ hx hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
h : Module.Finite R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
x : TensorProduct R A M
zero :
  Membership.mem (γ := Submodule A (TensorProduct R A M))
    (Submodule.span A
      (↑(Finset.image
            (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] TensorProduct R A M) 1) : (a : M) → TensorProduct R A M) s) :
        Set (TensorProduct R A M)))
    0
⊢ Membership.mem (γ := Submodule A (TensorProduct R A M))
    (Submodule.span A
      (↑(Finset.image
            (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] TensorProduct R A M) 1) : (a : M) → TensorProduct R A M) s) :
        Set (TensorProduct R A M)))
    x
have tmul : ∀ (x : A) (y : M),
  Membership.mem (γ := Submodule A (TensorProduct R A M))
    (Submodule.span A
      (↑(Finset.image
            (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] TensorProduct R A M) 1) : (a : M) → TensorProduct R A M) s) :
        Set (TensorProduct R A M)))
    (x ⊗ₜ[R] y)
Tactic: induction x with
    | zero => exact zero_mem _
    | tmul x y =>
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, Submodule.span_image, hs,
        Submodule.map_top, LinearMap.coe_range, ← mul_one x, ← smul_eq_mul,
        ← TensorProduct.smul_tmul']
      exact Submodule.smul_mem _ x (Submodule.subset_span <| Set.mem_range_self y)
    | add x y hx hy => exact Submodule.add_mem _ hx hy
Cleared hypotheses: x