-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem basis_singleton_iff {R M : Type*} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M]
    [NoZeroSMulDivisors R M] (ι : Type*) [Unique ι] :
    Nonempty (Basis ι R M) ↔ ∃ x ≠ 0, ∀ y : M, ∃ r : R, r • x = y

Proof state:
case mp
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) → ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

Tactic:
rintro ⟨b⟩

Result:
case mp.intro
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
b : Basis ι R M
⊢ ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

Proof state:
case mpr.intro.intro.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ { toFun := fun f => f default • x, map_add' := ⋯ }.toFun (c • y) =
    (RingHom.id R) c • { toFun := fun f => f default • x, map_add' := ⋯ }.toFun y

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

Result:
case mpr.intro.intro.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y default) • x = c • y default • x

Proof state:
case mpr.intro.intro.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y default) • x = c • y default • x

Tactic:
rw [← smul_assoc]

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = 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 => ?_ }⟩

Result:
case mpr.intro.intro.refine_1
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y z : ι →₀ R
⊢ (fun f => f default • x) (y + z) = (fun f => f default • x) y + (fun f => f default • x) z

case mpr.intro.intro.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ { toFun := fun f => f default • x, map_add' := ⋯ }.toFun (c • y) =
    (RingHom.id R) c • { toFun := fun f => f default • x, map_add' := ⋯ }.toFun y

case mpr.intro.intro.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y => single default ⋯.choose) ({ toFun := fun f => f default • x, map_add' := ⋯, map_smul' := ⋯ }.toFun f))
      default =
    f default

case mpr.intro.intro.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ { toFun := fun f => f default • x, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun y => single default ⋯.choose) y) = y

Proof state:
case mpr.intro.intro.refine_1
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y z : ι →₀ R
⊢ (fun f => f default • x) (y + z) = (fun f => f default • x) y + (fun f => f default • x) z

Tactic:
simp [Finsupp.add_apply, add_smul]

Result:
no goals

Proof state:
case mp.intro
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
b : Basis ι R M
⊢ ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

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

Result:
case mp.intro
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ r, r • b default = y

Proof state:
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) ↔ ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

Tactic:
constructor

Result:
case mp
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) → ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

case mpr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
⊢ (∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)

Proof state:
case mpr.intro.intro.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ⋯.choose • x = f default • x

Tactic:
exact (w (f default • x)).choose_spec

Result:
no goals

Proof state:
case mpr.intro.intro.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ { toFun := fun f => f default • x, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun y => single default ⋯.choose) y) = y

Tactic:
simp only [Finsupp.single_eq_same]

Result:
case mpr.intro.intro.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ ⋯.choose • x = y

Proof state:
case mpr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
⊢ (∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)

Tactic:
rintro ⟨x, nz, w⟩

Result:
case mpr.intro.intro
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
⊢ Nonempty (Basis ι R M)