awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
rw :
  Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    (((rTensor M (inclusion ⋯ ∘ₗ 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 (↥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 ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x) : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
⊢ 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)

Tactic:
rw [← comp_apply, ← rTensor_comp]

Premises used: LinearMap.comp_apply, LinearMap.rTensor_comp
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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 ⋯ ∘ₗ 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 (↥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 ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x) : TensorProduct.{u_1, u_3, u_2} R (↥I) M)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
obtain :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
    Module.Finite A (TensorProduct R A M)
⊢ Module.Finite A (TensorProduct R A M)

Tactic:
obtain ⟨s, hs⟩ := h.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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)

Tactic:
⟨⟨s.image (TensorProduct.mk R A M 1), eq_top_iff.mpr ?_⟩⟩

Premises used: Iff.mpr, eq_top_iff, Module.Finite.of_fg_top, Exists.intro, OfNat.ofNat, DFunLike.coe, Finset.image, TensorProduct.mk
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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)) ⊤
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)))
⊢ Module.Finite A (TensorProduct R A M)

Tactic:
refine ⟨⟨s.image (TensorProduct.mk R A M 1), eq_top_iff.mpr ?_⟩⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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)) ⊤
⊢ 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:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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)) ⊤
⊢ 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:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
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))
⊢ 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:
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']

Premises used: Submodule.span_span_of_tower, Submodule.map_top, Finset.coe_image, LinearMap.coe_range, TensorProduct.smul_tmul', smul_eq_mul, mul_one, Submodule.span_image
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
      (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:
Submodule.smul_mem _ x (Submodule.subset_span <| Set.mem_range_self y)

Premises used: Set.mem_range_self, Set.Mem, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
      (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:
exact Submodule.smul_mem _ x (Submodule.subset_span <| Set.mem_range_self y)

Premises used: Set.mem_range_self, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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 y : TensorProduct R A M
hx :
  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
hy :
  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)))
    y
⊢ 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 + y)

Tactic:
Submodule.add_mem _ hx hy

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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 y : TensorProduct R A M
hx :
  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
hy :
  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)))
    y
⊢ 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 + y)

Tactic:
exact Submodule.add_mem _ hx hy

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
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)
add :
  ∀ (x y : TensorProduct R A M)
    (hx :
      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)
    (hy :
      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)))
        y),
    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 + y)
⊢ 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

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

Premises used: Submodule.span_span_of_tower, Submodule.map_top, Finset.coe_image, LinearMap.coe_range, TensorProduct.smul_tmul', ZeroMemClass.zero_mem, smul_eq_mul, Submodule.span_image
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
obtain :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
    Module.Finite A (TensorProduct R A M)
obtain₁ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
    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)))
obtain₂ :
  ∀ (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
⊢ Module.Finite A (TensorProduct R A M)

Tactic:
classical
    obtain ⟨s, hs⟩ := h.fg_top
    refine ⟨⟨s.image (TensorProduct.mk R A M 1), eq_top_iff.mpr ?_⟩⟩
    rintro x -
    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

Premises used: Submodule.span_span_of_tower, Module.Finite.fg_top, Submodule.map_top, Finset.coe_image, LinearMap.coe_range, TensorProduct.smul_tmul', ZeroMemClass.zero_mem, smul_eq_mul, Submodule.span_image
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
obtain :
  ∀ (n : ℕ) (f : Fin n → M) (hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤),
    ∃ (N : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤
⊢ ∃ (N : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤

Tactic:
obtain ⟨n, f, hf⟩ := @Module.Finite.exists_fin R M _ _ _ _

Premises used: Module.Finite.exists_fin
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
⊢ ∀ x ∈ s, x < n

Tactic:
fun x hx ↦ lt_iff_not_ge.mpr fun e ↦ ?_

Premises used: Iff.mpr, lt_iff_not_ge
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
refine : ∀ (x : ℕ) (hx : x ∈ s) (e : n ≤ x), False
⊢ ∀ x ∈ s, x < n

Tactic:
refine fun x hx ↦ lt_iff_not_ge.mpr fun e ↦ ?_

Premises used: Iff.mpr, lt_iff_not_ge
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
h :
  ∀ (y : Fin n),
    Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' Set.Iio x) y ↔ Membership.mem (γ := Set (Fin n)) Set.univ y
⊢ Eq (α := Set (Fin n)) (Fin.val ⁻¹' Set.Iio x) Set.univ

Tactic:
ext y
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
y : Fin n
⊢ Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' Set.Iio x) y ↔ Membership.mem (γ := Set (Fin n)) Set.univ y

Tactic:
simpa using y.2.trans_le e

Premises used: Fin.isLt, LT.lt.trans_le
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
⊢ Eq (α := Set (Fin n)) (Fin.val ⁻¹' Set.Iio x) Set.univ

Tactic:
have : (Fin.val ⁻¹' Set.Iio x : Set (Fin n)) = Set.univ := by ext y; simpa using y.2.trans_le e
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
this : Eq (α := Set (Fin n)) (Fin.val ⁻¹' Set.Iio x) Set.univ
⊢ False

Tactic:
simp [s, this, hf] at hx
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
⊢ ∀ x ∈ s, x < n

Tactic:
have hns : ∀ x ∈ s, x < n := by
    refine fun x hx ↦ lt_iff_not_ge.mpr fun e ↦ ?_
    have : (Fin.val ⁻¹' Set.Iio x : Set (Fin n)) = Set.univ := by ext y; simpa using y.2.trans_le e
    simp [s, this, hf] at hx
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
⊢ 0 ∈ s

Tactic:
simp [s]
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
⊢ s.Nonempty

Tactic:
have hs₁ : s.Nonempty := ⟨0, by simp [s]⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
⊢ BddAbove s

Tactic:
have hs₂ : BddAbove s := ⟨n, fun x hx ↦ (hns x hx).le⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
⊢ sSup s ∈ s

Tactic:
have hs := Nat.sSup_mem hs₁ hs₂
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
⊢ ∃ (N : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤

Tactic:
⟨_, hs, ⟨⟨Submodule.mkQ _ (f ⟨_, hns _ hs⟩), ?_⟩⟩⟩

Premises used: Fin.mk, Submodule.IsPrincipal.mk, And.intro, Exists.intro, Submodule.mkQ, DFunLike.coe