awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
apply : w ≤ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
⊢ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) = w

Tactic:
apply le_antisymm h

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
by_contra : ∀ (q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)), False
⊢ Membership.mem (γ := Set M) (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)) x

Tactic:
by_contra q
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
⊢ (linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x

Tactic:
have e := b.linearCombination_repr x
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
e : (linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x
i i' : ι
r :
  Eq.{u_5 + 1} (α := (↑w : Type u_5))
    ((fun (i : ι) ↦ (Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯ : { x : M // x ∈ w })) i)
    ((fun (i : ι) ↦ (Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯ : { x : M // x ∈ w })) i')
⊢ Eq.{u_5 + 1} (α := M) ((b : (a : ι) → M) i : M) ((b : (a : ι) → M) i' : M)

Tactic:
simpa only [Subtype.mk_eq_mk] using r

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
e : (sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (a : R) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) = x
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
⊢ (sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (a : R) ↦
      HSMul.hSMul (β := M) a (↑((u : (a : ι) → (↑w : Type u_5)) i) : M)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)

Tactic:
change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e

Premises used: Finsupp.sum, Module.Basis.repr, Subtype.mk, HSMul.hSMul, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (a : R) ↦
      HSMul.hSMul (β := M) a (↑((u : (a : ι) → (↑w : Type u_5)) i) : M)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
⊢ (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)

Tactic:
rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)),
      ← Finsupp.linearCombination_apply] at e

Premises used: Finsupp.sum_embDomain, Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
⊢ False

Tactic:
hi.linearCombination_ne_of_notMem_support _ ?_ e

Premises used: LinearIndependent.linearCombination_ne_of_notMem_support
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
refine :
  Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p ∉
    Finsupp.support.{u_5, u_3} (M := R) (embDomain u ((b.repr : (a : M) → ι →₀ R) x))
⊢ False

Tactic:
refine hi.linearCombination_ne_of_notMem_support _ ?_ e

Premises used: LinearIndependent.linearCombination_ne_of_notMem_support
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
simp :
  ¬∃ (a : ι),
      Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : M) → ι →₀ R) x)) a ∧
        (u : (a : ι) → { x : M // x ∈ w }) a = Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p ∉
    Finsupp.support.{u_5, u_3} (M := R) (embDomain u ((b.repr : (a : M) → ι →₀ R) x))

Tactic:
simp only [Finset.mem_map, Finsupp.support_embDomain]

Premises used: Finset.mem_map, Finsupp.support_embDomain
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
j : ι
W : (u : (a : ι) → { x : M // x ∈ w }) j = Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p
⊢ (b : (a : ι) → M) j = x

Tactic:
simp only [u, Embedding.coeFn_mk, Subtype.mk_eq_mk] at W

Premises used: Subtype.mk_eq_mk, Function.Embedding.coeFn_mk
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
j : ι
W : (b : (a : ι) → M) j = x
⊢ False

Tactic:
apply q ⟨j, W⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b_1 : Basis ι R M
v : ι → M
x y : M
inst_5 : Subsingleton R
x_1 : Basis ι R M
b : M ≃ₗ[R] ι →₀ R
rw : Eq (α := Basis ι R M) { repr := repr default } default
rw₁ : M ≃ₗ[R] ι →₀ R
rw₂ : Eq (α := Basis ι R M) { repr := repr default } default
rw₃ : M ≃ₗ[R] ι →₀ R
⊢ { repr := b : Basis ι R M } = default

Tactic:
rw [Subsingleton.elim b]

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R_1
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
b_1 : Basis ι_1 R_1 M
v : ι_1 → M
x_1 y_1 : M
b : Basis ι_1 R_1 M
ι : Type u_7
R : Type u_8
inst_5 : Unique ι
inst_6 : Semiring R
x y : R
⊢ single default (x + y) = HAdd.hAdd (α := ι →₀ R) (single default x) (single default y)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R_1
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
b_1 : Basis ι_1 R_1 M
v : ι_1 → M
x_1 y : M
b : Basis ι_1 R_1 M
ι : Type u_7
R : Type u_8
inst_5 : Unique ι
inst_6 : Semiring R
c x : R
⊢ single default (c • x) = HSMul.hSMul (α := R) (β := ι →₀ R) ((RingHom.id R : (a : R) → R) c : R) (single default x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R_1
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
b_1 : Basis ι_1 R_1 M
v : ι_1 → M
x_1 y : M
b : Basis ι_1 R_1 M
ι : Type u_7
R : Type u_8
inst_5 : Unique ι
inst_6 : Semiring R
x : R
⊢ (fun (f : ι →₀ R) ↦ ((f : (a : ι) → R) default : R)) ((fun (x : R) ↦ (single default x : ι →₀ R)) x) = x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R_1
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
b_1 : Basis ι_1 R_1 M
v : ι_1 → M
x y : M
b : Basis ι_1 R_1 M
ι : Type u_7
R : Type u_8
inst_5 : Unique ι
inst_6 : Semiring R
f : ι →₀ R
⊢ Eq.{u_8 + 1} (α := R)
    (((fun (x : R) ↦ (single default x : ι →₀ R)) ((fun (f : ι →₀ R) ↦ ((f : (a : ι) → R) default : R)) f) :
          (a : ι) → R)
        default :
      R)
    ((f : (a : ι) → R) default : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_7
R : Type u_8
inst : Unique ι
inst_1 : Semiring R
i : ι
⊢ Eq (α := ι →₀ R) ((repr (Basis.singleton ι R) : (a : R) → ι →₀ R) 1) (single i 1)

Tactic:
simp [Basis.singleton]

Premises used: Module.Basis.singleton
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_7
R : Type u_8
inst : Unique ι
inst_1 : Semiring R
x : R
i : ι
⊢ (((repr (Basis.singleton ι R) : (a : R) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i = x

Tactic:
simp [Basis.singleton, Unique.eq_default i]

Premises used: Unique.eq_default, Module.Basis.singleton
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_7
R : Type u_8
inst : Unique ι
inst_1 : Semiring R
h : ∀ (x : ι), Eq.{u_8 + 1} (α := R) ((Basis.singleton ι R : (a : ι) → R) x : R) (1 x : R)
⊢ Eq (α := (a : ι) → R) (⇑(Basis.singleton ι R) : (a : ι) → R) 1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_7
R : Type u_8
inst : Unique ι
inst_1 : Semiring R
x : ι
⊢ Eq.{u_8 + 1} (α := R) ((Basis.singleton ι R : (a : ι) → R) x : R) (1 x : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
⊢ ∀ (r : R) (m : M),
    (b.repr : (a : M) → ι →₀ R) (r • m) = HSMul.hSMul (β := ι →₀ R) r ((b.repr : (a : M) → ι →₀ R) m : ι →₀ R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
c : R
x : M
⊢ IsTorsionFree R M

Tactic:
have := b.isTorsionFree
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
c : R
x : M
this : IsTorsionFree R M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0

Tactic:
smul_eq_zero

Premises used: smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
c : R
x : M
this : IsTorsionFree R M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0

Tactic:
exact smul_eq_zero

Premises used: smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
mp : Nonempty (Basis ι R M) → ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y
mpr : (∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y) → Nonempty (Basis ι R M)
⊢ Nonempty (Basis ι R M) ↔ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
b : Basis ι R M
⊢ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y

Tactic:
⟨b default, b.linearIndependent.ne_zero _, ?_⟩

Premises used: Inhabited.default, LinearIndependent.ne_zero, Module.Basis.linearIndependent, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
b : Basis ι R M
mp : ∀ (y : M), ∃ (r : R), HSMul.hSMul (β := M) r ((b : (a : ι) → M) default : M) = y
⊢ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y

Tactic:
refine ⟨b default, b.linearIndependent.ne_zero _, ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ (r : R), HSMul.hSMul (β := M) r ((b : (a : ι) → M) default : M) = y

Tactic:
simpa [span_singleton_eq_top_iff, Set.range_unique] using b.span_eq

Premises used: Set.range_unique, Submodule.span_singleton_eq_top_iff, Module.Basis.span_eq
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
⊢ Nonempty (Basis ι R M)

Tactic:
⟨ofRepr <| LinearEquiv.symm
      { toFun := fun f => f default • x
        invFun := fun y => Finsupp.single default (w y).choose
        left_inv := fun f => Finsupp.unique_ext ?_
        right_inv := fun y => ?_
        map_add' := fun y z => ?_
        map_smul' := fun c y => ?_ }⟩

Premises used: Inhabited.default, Module.Basis.ofRepr, LinearEquiv.symm, LinearEquiv.mk, Finsupp.unique_ext, Nonempty.intro, LinearMap.mk, HSMul.hSMul, Exists.choose, AddHom.mk, DFunLike.coe, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
mpr :
  ∀ (y z : ι →₀ R),
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y + z : (a : ι) → R) default : R) x =
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x +
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((z : (a : ι) → R) default : R) x
mpr₁ :
  ∀ (c : R) (y : ι →₀ R),
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((c • y : (a : ι) → R) default : R) x =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
        (HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x)
mpr₂ :
  ∀ (f : ι →₀ R),
    Eq.{u_7 + 1} (α := R)
      (((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
              ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
            (a : ι) → R)
          default :
        R)
      ((f : (a : ι) → R) default : R)
mpr₃ :
  ∀ (y : M),
    (fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x)
        ((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R)) y) =
      y
⊢ Nonempty (Basis ι R M)

Tactic:
refine ⟨ofRepr <| LinearEquiv.symm
      { toFun := fun f => f default • x
        invFun := fun y => Finsupp.single default (w y).choose
        left_inv := fun f => Finsupp.unique_ext ?_
        right_inv := fun y => ?_
        map_add' := fun y z => ?_
        map_smul' := fun c y => ?_ }⟩
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
y z : ι →₀ R
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y + z : (a : ι) → R) default : R) x =
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x +
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((z : (a : ι) → R) default : R) x

Tactic:
simp [Finsupp.add_apply, add_smul]

Premises used: Finsupp.add_apply, add_smul
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
c : R
y : ι →₀ R
mpr :
  HSMul.hSMul (β := R) c ((y : (a : ι) → R) default : R) • x =
    c • HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((c • y : (a : ι) → R) default : R) x =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
      (HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x)

Tactic:
simp only [Finsupp.coe_smul, Pi.smul_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, Finsupp.coe_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
c : R
y : ι →₀ R
mpr mpr₁ :
  HSMul.hSMul (β := R) c ((y : (a : ι) → R) default : R) • x =
    HSMul.hSMul (β := R) c ((y : (a : ι) → R) default : R) • x
⊢ HSMul.hSMul (β := R) c ((y : (a : ι) → R) default : R) • x =
    c • HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x

Tactic:
rw [← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
f : ι →₀ R
⊢ Eq.{u_7 + 1} (α := R)
    (((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
            ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
          (a : ι) → R)
        default :
      R)
    ((f : (a : ι) → R) default : R)

Tactic:
smul_left_injective _ nz ?_

Premises used: smul_left_injective
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
f : ι →₀ R
mpr :
  Eq.{u_8 + 1} (α := M)
    ((fun (x_1 : R) ↦ x_1 • x)
      (((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
            ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
          (a : ι) → R)
        default))
    ((fun (x_1 : R) ↦ x_1 • x) ((f : (a : ι) → R) default))
⊢ Eq.{u_7 + 1} (α := R)
    (((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
            ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
          (a : ι) → R)
        default :
      R)
    ((f : (a : ι) → R) default : R)

Tactic:
refine smul_left_injective _ nz ?_

Premises used: smul_left_injective
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
f : ι →₀ R
mpr :
  Exists.choose (p := fun (r : R) ↦ r • x = HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) ⋯ •
      x =
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x
⊢ Eq.{u_8 + 1} (α := M)
    ((fun (x_1 : R) ↦ x_1 • x)
      (((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
            ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
          (a : ι) → R)
        default))
    ((fun (x_1 : R) ↦ x_1 • x) ((f : (a : ι) → R) default))

Tactic:
simp only [Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same