awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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 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)
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
⊢ 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: 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
-- 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
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)
have 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)))
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
-- 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
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)))
⊢ Module.Finite A (TensorProduct R A M)
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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 : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤
have 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) ⊤
Tactic: obtain ⟨n, f, hf⟩ := @Module.Finite.exists_fin R M _ _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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
have refine : ∀ (x : ℕ) (hx : x ∈ s) (e : n ≤ x), False
Tactic: refine fun x hx ↦ lt_iff_not_ge.mpr fun e ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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
have h : ∀ (y : Fin n),
  Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' Set.Iio x) y ↔ Membership.mem (γ := Set (Fin n)) Set.univ y
Tactic: ext y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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
⊢ False
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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)) ⊤}
⊢ ∃ (N : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤
have hns : ∀ 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
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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
⊢ ∃ (N : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤
have hs₁ : s.Nonempty
Tactic: have hs₁ : s.Nonempty := ⟨0, by simp [s]⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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
⊢ ∃ (N : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤
have hs₂ : BddAbove s
Tactic: have hs₂ : BddAbove s := ⟨n, fun x hx ↦ (hns x hx).le⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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
⊢ ∃ (N : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤
have hs : sSup s ∈ s
Tactic: have hs := Nat.sSup_mem hs₁ hs₂
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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) ⊤
have refine : Eq (α :=
  Submodule R (HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))) ⊤
  (Submodule.span R
    (singleton (α := HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))
      ((Submodule.mkQ (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))) :
            (a : M) → M ⧸ Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s)))
          (f ⟨sSup s, sorry⟩) :
        HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))))
Tactic: refine ⟨_, hs, ⟨⟨Submodule.mkQ _ (f ⟨_, hns _ hs⟩), ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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
⊢ Eq (α :=
    Submodule R (HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))) ⊤
    (Submodule.span R
      (singleton (α :=
        HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))
        ((Submodule.mkQ (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))) :
              (a : M) → M ⧸ Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s)))
            (f ⟨sSup s, ⋯⟩) :
          HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))))
have this : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤
Tactic: have := not_not.mp (notMem_of_csSup_lt (Order.lt_succ _) hs₂)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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
this : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤
⊢ Eq (α :=
    Submodule R (HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))) ⊤
    (Submodule.span R
      (singleton (α :=
        HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))
        ((Submodule.mkQ (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))) :
              (a : M) → M ⧸ Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s)))
            (f ⟨sSup s, ⋯⟩) :
          HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))))
have rw : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' {sSup s} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)))
  (Submodule.span R (f '' {(⟨sSup s, sorry⟩ : Fin n)} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)))
Tactic: rw [← Set.image_singleton, ← Submodule.map_span,
    ← (Submodule.comap_injective_of_surjective (Submodule.mkQ_surjective _)).eq_iff,
    Submodule.comap_map_eq, Submodule.ker_mkQ, Submodule.comap_top, ← this, ← Submodule.span_union,
    Order.Iio_succ_eq_insert (sSup s), ← Set.union_singleton, Set.preimage_union, Set.image_union,
    ← @Set.image_singleton _ _ f, Set.union_comm]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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
this : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤
⊢ Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' {sSup s} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)))
    (Submodule.span R (f '' {(⟨sSup s, ⋯⟩ : Fin n)} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)))
have h : Eq (α := Set (Fin n)) (Fin.val ⁻¹' {sSup s}) {(⟨sSup s, sorry⟩ : Fin n)}
Tactic: congr!
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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
this : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤
⊢ Eq (α := Set (Fin n)) (Fin.val ⁻¹' {sSup s}) {(⟨sSup s, ⋯⟩ : Fin n)}
have h : ∀ (x : Fin n),
  Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' {sSup s}) x ↔
    Membership.mem (γ := Set (Fin n)) {(⟨sSup s, sorry⟩ : Fin n)} x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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
⊢ ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I),
    I ≠ ⊤ ∧ Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑f : (a : M) → R ⧸ I)
have obtain : ∀ (N : Submodule R M) (hN : N ≠ ⊤) (x : M ⧸ N) (hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)),
  ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I),
    I ≠ ⊤ ∧ Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑f : (a : M) → R ⧸ I)
Tactic: obtain ⟨N, hN, ⟨x, hx⟩⟩ := Module.exists_isPrincipal_quotient_of_finite R M
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := M ⧸ N) (⇑(LinearMap.toSpanSingleton R (M ⧸ N) x) : (a : R) → M ⧸ N)
have rw : Eq (α := Submodule R (M ⧸ N)) (LinearMap.range (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
Tactic: rw [← LinearMap.range_eq_top, ← LinearMap.span_singleton_eq_range, hx]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
rw : Eq (α := Submodule R (M ⧸ N)) (LinearMap.range (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := M ⧸ N) (⇑(LinearMap.toSpanSingleton R (M ⧸ N) x) : (a : R) → M ⧸ N)
have rw₁ : Eq (α := Submodule R (M ⧸ N)) (R ∙ x) ⊤
Tactic: rw [← LinearMap.range_eq_top, ← LinearMap.span_singleton_eq_range, hx]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
rw : Eq (α := Submodule R (M ⧸ N)) (LinearMap.range (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
rw₁ : Eq (α := Submodule R (M ⧸ N)) (R ∙ x) ⊤
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := M ⧸ N) (⇑(LinearMap.toSpanSingleton R (M ⧸ N) x) : (a : R) → M ⧸ N)
have rw₂ : Eq (α := Submodule R (M ⧸ N)) (R ∙ x) (R ∙ x)
Tactic: rw [← LinearMap.range_eq_top, ← LinearMap.span_singleton_eq_range, hx]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x))) (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) x) ⋯
⊢ ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I),
    I ≠ ⊤ ∧ Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑f : (a : M) → R ⧸ I)
have refine : ∀ (e : Eq (α := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤), False
Tactic: refine ⟨_, f.symm.toLinearMap.comp N.mkQ, fun e ↦ ?_, f.symm.surjective.comp N.mkQ_surjective⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x))) (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) x) ⋯
e : Eq (α := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
⊢ False
have hx₁ : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ 0)
Tactic: obtain rfl : x = 0 := by simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1
Cleared hypotheses: x, hx, f, e
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x))) (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) x) ⋯
e : Eq (α := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
hx₁ : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ 0)
⊢ False
have e₁ : Eq (α := Ideal R) (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ⊤
Tactic: obtain rfl : x = 0 := by simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1
Cleared hypotheses: x, hx, f, e
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
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 : Submodule R M
hN : N ≠ ⊤
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ 0)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R)
    (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)))
  (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) 0) ⋯
e : Eq (α := Ideal R) (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ⊤
⊢ False
have this : Nontrivial.{u_2} (M ⧸ N)
Tactic: have : Nontrivial (M ⧸ N) := by rwa [Submodule.Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
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
⊢ Nontrivial.{u_2} (M ⊗[R] M)
have obtain : ∀ (I : Ideal R) (ϕ : M →ₗ[R] R ⧸ I) (hI : I ≠ ⊤)
  (hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)), Nontrivial.{u_2} (M ⊗[R] M)
Tactic: obtain ⟨I, ϕ, hI, hϕ⟩ := Module.exists_surjective_quotient_of_finite R M