awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
refine_1 :
  LE.le (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))
refine_2 :
  LE.le (α := Submodule R M) (span R (range v)) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i))))
⊢ Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
refine_1 :
  ∀ (y : ι),
    Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) y)
⊢ LE.le (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))

Tactic:
simp only [span_le, Set.range_subset_iff, SetLike.mem_coe]

Premises used: SetLike.mem_coe, Set.range_subset_iff, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
refine_2 :
  ∀ (y : ι),
    Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v y)
⊢ LE.le (α := Submodule R M) (span R (range v)) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i))))

Tactic:
simp only [span_le, Set.range_subset_iff, SetLike.mem_coe]

Premises used: SetLike.mem_coe, Set.range_subset_iff, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
refine_1 : Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) j)
refine_1₁ :
  ∀ (hjk : j ≠ k),
    Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) k)
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) k)

Tactic:
obtain rfl | hjk := eq_or_ne j k

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
refine_2 :
  Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v j)
refine_2₁ :
  ∀ (hjk : j ≠ k),
    Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v k)
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v k)

Tactic:
obtain rfl | hjk := eq_or_ne j k

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
refine_1 : Membership.mem (γ := Submodule R M) (span R (range v)) (v j + r • v i)
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) j)

Tactic:
rw [update_self]

Premises used: Function.update_self
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (v j + r • v i)

Tactic:
add_mem (subset_span ⟨j, rfl⟩) <| smul_mem _ _ <| subset_span ⟨i, rfl⟩

Premises used: Exists.intro, AddMemClass.add_mem, Submodule.subset_span, rfl, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (v j + r • v i)

Tactic:
exact add_mem (subset_span ⟨j, rfl⟩) <| smul_mem _ _ <| subset_span ⟨i, rfl⟩

Premises used: Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) k)

Tactic:
subset_span ⟨k, (update_of_ne hjk.symm ..).symm⟩

Premises used: Ne.symm, Exists.intro, Submodule.subset_span, Eq.symm, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) k)

Tactic:
exact subset_span ⟨k, (update_of_ne hjk.symm ..).symm⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
refine_2 :
  Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i))))
    (v j + r • v i - r • v i)
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v j)

Tactic:
nth_rw 2 [← add_sub_cancel_right (v j) (r • v i)]

Premises used: HSMul.hSMul, add_sub_cancel_right
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i))))
    (v j + r • v i - r • v i)

Tactic:
sub_mem (subset_span ⟨j, update_self ..⟩)
      (smul_mem _ _ (subset_span ⟨i, update_of_ne hij ..⟩))

Premises used: sub_mem, Exists.intro, Submodule.subset_span, Function.update_self, Submodule.smul_mem, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i))))
    (v j + r • v i - r • v i)

Tactic:
exact sub_mem (subset_span ⟨j, update_self ..⟩)
      (smul_mem _ _ (subset_span ⟨i, update_of_ne hij ..⟩))
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v k)

Tactic:
subset_span ⟨k, update_of_ne hjk.symm ..⟩

Premises used: Ne.symm, Exists.intro, Submodule.subset_span, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v k)

Tactic:
exact subset_span ⟨k, update_of_ne hjk.symm ..⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
rw : Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + -(r • v i))))) (span R (range v))
rw₁ : Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + -r • v i)))) (span R (range v))
rw₂ rw₃ : Eq (α := Submodule R M) (span R (range v)) (span R (range v))
⊢ Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j - r • v i)))) (span R (range v))

Tactic:
rw [sub_eq_add_neg, ← neg_smul, span_range_update_add_smul hij]

Premises used: neg_smul, sub_eq_add_neg, Submodule.span_range_update_add_smul
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsPrincipal R M ↔ Submodule.IsPrincipal.{u_1, u_4} (R := R) (M := M) ⊤

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
simp_rw : (∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)) ↔ ∃ (a : M), p = R ∙ a
⊢ IsPrincipal.{u_1, u_4} R ↥p ↔ p.IsPrincipal

Tactic:
simp_rw [IsPrincipal, isPrincipal_iff]

Premises used: Module.IsPrincipal, Submodule.isPrincipal_iff
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
mp : (∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)) → ∃ (a : M), p = R ∙ a
mpr : (∃ (a : M), p = R ∙ a) → ∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
⊢ (∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)) ↔ ∃ (a : M), p = R ∙ a

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : ↥p
ha : Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
⊢ ∃ (a : M), p = R ∙ a

Tactic:
⟨a, le_antisymm (fun m hm ↦ ?_) <| (span_singleton_le_iff_mem ..).mpr a.2⟩

Premises used: Iff.mpr, le_antisymm, Exists.intro, Submodule.span_singleton_le_iff_mem, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : ↥p
ha : Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
mp : ∀ (m : M) (hm : m ∈ p), Membership.mem (γ := Submodule R M) (R ∙ (↑a : M)) m
⊢ ∃ (a : M), p = R ∙ a

Tactic:
refine ⟨a, le_antisymm (fun m hm ↦ ?_) <| (span_singleton_le_iff_mem ..).mpr a.2⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : ↥p
ha : Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
m : M
hm : m ∈ p
mp :
  ∀ (r : R) (hr : r • a = Subtype.mk (p := fun (x : M) ↦ x ∈ p) m hm),
    Membership.mem (γ := Submodule R M) (R ∙ (↑a : M)) m
⊢ Membership.mem (γ := Submodule R M) (R ∙ (↑a : M)) m

Tactic:
have ⟨r, hr⟩ := mem_span_singleton.mp (ha ▸ (trivial : (⟨m, hm⟩ : p) ∈ ⊤))
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : ↥p
ha : Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
m : M
hm : m ∈ p
r : R
hr : r • a = Subtype.mk (p := fun (x : M) ↦ x ∈ p) m hm
⊢ Membership.mem (γ := Submodule R M) (R ∙ (↑a : M)) m

Tactic:
mem_span_singleton.mpr ⟨r, congr($hr)⟩

Premises used: Iff.mpr, congrArg, Submodule.mem_span_singleton, id, Exists.intro, Subtype.val
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : ↥p
ha : Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
m : M
hm : m ∈ p
r : R
hr : r • a = Subtype.mk (p := fun (x : M) ↦ x ∈ p) m hm
⊢ Membership.mem (γ := Submodule R M) (R ∙ (↑a : M)) m

Tactic:
exact mem_span_singleton.mpr ⟨r, congr($hr)⟩

Premises used: Iff.mpr, Submodule.mem_span_singleton, id, Exists.intro
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
⊢ ∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)

Tactic:
⟨⟨a, ha ▸ mem_span_singleton_self a⟩, .symm <| top_unique fun x _ ↦ ?_⟩

Premises used: Eq.rec, Submodule.mem_span_singleton_self, Subtype.mk, top_unique, Exists.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
mpr :
  ∀ (x : ↥p),
    Membership.mem (γ := Submodule R ↥p) ⊤ x →
      Membership.mem (γ := Submodule R ↥p) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ p) a ⋯) x
⊢ ∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)

Tactic:
refine ⟨⟨a, ha ▸ mem_span_singleton_self a⟩, .symm <| top_unique fun x _ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
x : ↥p
h : Membership.mem (γ := Submodule R ↥p) ⊤ x
mpr :
  ∀ (r : R) (hr : r • a = (↑x : M)),
    Membership.mem (γ := Submodule R ↥p) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ p) a ⋯) x
⊢ Membership.mem (γ := Submodule R ↥p) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ p) a ⋯) x

Tactic:
have ⟨r, hr⟩ := mem_span_singleton.mp (ha.le x.2)
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
x : ↥p
h : Membership.mem (γ := Submodule R ↥p) ⊤ x
r : R
hr : r • a = (↑x : M)
⊢ Membership.mem (γ := Submodule R ↥p) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ p) a ⋯) x

Tactic:
mem_span_singleton.mpr ⟨r, Subtype.ext hr⟩

Premises used: Iff.mpr, Submodule.mem_span_singleton, Exists.intro, Subtype.ext
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
x : ↥p
h : Membership.mem (γ := Submodule R ↥p) ⊤ x
r : R
hr : r • a = (↑x : M)
⊢ Membership.mem (γ := Submodule R ↥p) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ p) a ⋯) x

Tactic:
exact mem_span_singleton.mpr ⟨r, Subtype.ext hr⟩

Premises used: Iff.mpr, Submodule.mem_span_singleton, Exists.intro, Subtype.ext
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
have : ∀ (m : M) (hm : Eq (α := Submodule R M) ⊤ (R ∙ m)), ∃ (a : M₂), Eq (α := Submodule R M₂) ⊤ (R ∙ a)
⊢ ∃ (a : M₂), Eq (α := Submodule R M₂) ⊤ (R ∙ a)

Tactic:
have ⟨m, hm⟩ := IsPrincipal.principal (⊤ : Submodule R M)
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
m : M
hm : Eq (α := Submodule R M) ⊤ (R ∙ m)
⊢ ∃ (a : M₂), Eq (α := Submodule R M₂) ⊤ (R ∙ a)

Tactic:
⟨f m, .symm <| top_unique fun y _ ↦ ?_⟩

Premises used: top_unique, Exists.intro, Eq.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
m : M
hm : Eq (α := Submodule R M) ⊤ (R ∙ m)
refine :
  ∀ (y : M₂),
    Membership.mem (γ := Submodule R M₂) ⊤ y →
      Membership.mem (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂))) y
⊢ ∃ (a : M₂), Eq (α := Submodule R M₂) ⊤ (R ∙ a)

Tactic:
refine ⟨f m, .symm <| top_unique fun y _ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
m : M
hm : Eq (α := Submodule R M) ⊤ (R ∙ m)
y : M₂
h : Membership.mem (γ := Submodule R M₂) ⊤ y
obtain :
  ∀ (x : M),
    Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R M₂) ⊤ ((f : (a : M) → M₂) x : M₂) →
      Membership.mem (α := M₂) (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂)))
        ((f : (a : M) → M₂) x : M₂)
⊢ Membership.mem (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂))) y

Tactic:
obtain ⟨x, rfl⟩ := hf y

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
m : M
hm : Eq (α := Submodule R M) ⊤ (R ∙ m)
x : M
h : Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R M₂) ⊤ ((f : (a : M) → M₂) x : M₂)
obtain :
  ∀ (r : R),
    Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R M₂) ⊤ ((f : (a : M) → M₂) (r • m) : M₂) →
      Membership.mem (α := M₂) (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂)))
        ((f : (a : M) → M₂) (r • m) : M₂)
⊢ Membership.mem (α := M₂) (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂)))
    ((f : (a : M) → M₂) x : M₂)

Tactic:
obtain ⟨r, rfl⟩ := mem_span_singleton.mp (hm.le (trivial : x ∈ ⊤))

Premises used: Submodule.mem_span_singleton, Eq.le, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
m : M
hm : Eq (α := Submodule R M) ⊤ (R ∙ m)
r : R
h : Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R M₂) ⊤ ((f : (a : M) → M₂) (r • m) : M₂)
⊢ Membership.mem (α := M₂) (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂)))
    ((f : (a : M) → M₂) (r • m) : M₂)

Tactic:
simpa only [map_smul] using smul_mem _ r (mem_span_singleton_self _)

Premises used: Submodule.mem_span_singleton_self, Submodule.smul_mem, map_smul
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
a : A
x : ↥p
⊢ (↑((tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) (a ⊗ₜ[R] x)) : M) = a • (↑x : M)

Tactic:
rfl

Premises used: iInf, Set.Mem, Set.iInter, setOf, rfl
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
v : ↥(span A (↑p : Set M))
obtain :
  ∀ (f : Finsupp.{u_3, u_2} (↑(↑p : Set M) : Type u_3) A)
    (hf :
      (Finsupp.linearCombination A (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M))) :
            (a : (↑(↑p : Set M) : Type u_3) →₀ A) → M)
          f =
        (↑v : M)),
    ∃ (a : TensorProduct.{u_1, u_2, u_3} R A ↥p), (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) a = v
⊢ ∃ (a : TensorProduct.{u_1, u_2, u_3} R A ↥p), (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) a = v

Tactic:
obtain ⟨f, hf⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp v.property

Premises used: Finsupp.mem_span_iff_linearCombination, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
v : ↥(span A (↑p : Set M))
f : Finsupp.{u_3, u_2} (↑(↑p : Set M) : Type u_3) A
hf :
  (Finsupp.linearCombination A (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M))) :
        (a : (↑(↑p : Set M) : Type u_3) →₀ A) → M)
      f =
    (↑v : M)
h :
  (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M)))
      (f.sum fun (x : (↑(↑p : Set M) : Type u_3)) (a : A) ↦ a ⊗ₜ[R] x) =
    v
⊢ ∃ (a : TensorProduct.{u_1, u_2, u_3} R A ↥p), (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) a = v

Tactic:
use f.sum fun x a ↦ a ⊗ₜ x

Premises used: Finsupp.sum, TensorProduct.tmul
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
v : ↥(span A (↑p : Set M))
f : Finsupp.{u_3, u_2} (↑(↑p : Set M) : Type u_3) A
hf :
  (Finsupp.linearCombination A (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M))) :
        (a : (↑(↑p : Set M) : Type u_3) →₀ A) → M)
      f =
    (↑v : M)
h :
  (f.sum fun (a : (↑(↑p : Set M) : Type u_3)) (b : A) ↦
      (Submodule.subtype (span A (↑p : Set M)) : (a : ↥(span A (↑p : Set M))) → M)
        ((tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) (b ⊗ₜ[R] a) : ↥(span A (↑p : Set M)))) =
    (↑v : M)
⊢ (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M)))
      (f.sum fun (x : (↑(↑p : Set M) : Type u_3)) (a : A) ↦ a ⊗ₜ[R] x) =
    v

Tactic:
rw [map_finsuppSum, Subtype.ext_iff, ← Submodule.subtype_apply, map_finsuppSum]

Premises used: Submodule.subtype_apply, Subtype.ext_iff, map_finsuppSum
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
v : ↥(span A (↑p : Set M))
f : Finsupp.{u_3, u_2} (↑(↑p : Set M) : Type u_3) A
hf :
  (Finsupp.linearCombination A (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M))) :
        (a : (↑(↑p : Set M) : Type u_3) →₀ A) → M)
      f =
    (↑v : M)
⊢ (f.sum fun (a : (↑(↑p : Set M) : Type u_3)) (b : A) ↦
      (Submodule.subtype (span A (↑p : Set M)) : (a : ↥(span A (↑p : Set M))) → M)
        ((tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) (b ⊗ₜ[R] a) : ↥(span A (↑p : Set M)))) =
    (↑v : M)

Tactic:
simpa using hf
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
f : TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) →ₗ[A] ↥(span A (↑p : Set M)) :=
  AlgebraTensorModule.lift
    (restrictScalarsₗ R A (↥(span A (↑p : Set M))) (↥(span A (↑p : Set M))) A ∘ₗ lsmul A ↥(span A (↑p : Set M)))
g : TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) :=
  lTensor A (inclusionSpan A p)
⊢ Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M))) (β := ↥(span A (↑p : Set M)))
    (⇑f : (a : A ⊗[R] ↥(span A (↑p : Set M))) → ↥(span A (↑p : Set M)))

Tactic:
have hf : Injective f := Algebra.injective_lift_lsmul R A _