case mp
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) → ∃ x x_1, ∀ (y : M), ∃ r, r • x = y

case mpr
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
⊢ (∃ x x_1, ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) ↔ ∃ x x_1, ∀ (y : M), ∃ r, r • x = y
constructor
case mp.intro
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b✝ b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
b : Basis ι R M
⊢ ∃ x x_1, ∀ (y : M), ∃ r, r • x = y
case mp
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) → ∃ x x_1, ∀ (y : M), ∃ r, r • x = y
rintro ⟨b⟩
case mp.intro
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b✝ b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ r, r • ↑b default = y
case mp.intro
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b✝ b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
b : Basis ι R M
⊢ ∃ x x_1, ∀ (y : M), ∃ r, r • x = y
refine' ⟨b default, b.linearIndependent.ne_zero _, _⟩
no goals
case mp.intro
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b✝ b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ r, r • ↑b default = y
simpa [span_singleton_eq_top_iff, Set.range_unique] using b.span_eq
case mpr.intro.intro
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
⊢ Nonempty (Basis ι R M)
case mpr
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
⊢ (∃ x x_1, ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)
rintro ⟨x, nz, w⟩
case mpr.intro.intro.refine_1
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
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
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c✝ : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ AddHom.toFun
      { toFun := fun f => ↑f default • x,
        map_add' :=
          (_ :
            ∀ (y z : ι →₀ R),
              (fun f => ↑f default • x) (y + z) = (fun f => ↑f default • x) y + (fun f => ↑f default • x) z) }
      (c • y) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun f => ↑f default • x,
          map_add' :=
            (_ :
              ∀ (y z : ι →₀ R),
                (fun f => ↑f default • x) (y + z) = (fun f => ↑f default • x) y + (fun f => ↑f default • x) z) }
        y

case mpr.intro.intro.refine_3
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ↑((fun y => Finsupp.single default (Exists.choose (_ : ∃ r, r • x = y)))
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => ↑f default • x,
                    map_add' :=
                      (_ :
                        ∀ (y z : ι →₀ R),
                          (fun f => ↑f default • x) (y + z) =
                            (fun f => ↑f default • x) y + (fun f => ↑f default • x) z) },
                map_smul' :=
                  (_ :
                    ∀ (c : R) (y : ι →₀ R),
                      AddHom.toFun
                          { toFun := fun f => ↑f default • x,
                            map_add' :=
                              (_ :
                                ∀ (y z : ι →₀ R),
                                  (fun f => ↑f default • x) (y + z) =
                                    (fun f => ↑f default • x) y + (fun f => ↑f default • x) z) }
                          (c • y) =
                        ↑(RingHom.id R) c •
                          AddHom.toFun
                            { toFun := fun f => ↑f default • x,
                              map_add' :=
                                (_ :
                                  ∀ (y z : ι →₀ R),
                                    (fun f => ↑f default • x) (y + z) =
                                      (fun f => ↑f default • x) y + (fun f => ↑f default • x) z) }
                            y) }.toAddHom
            f))
      default =
    ↑f default

case mpr.intro.intro.refine_4
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => ↑f default • x,
              map_add' :=
                (_ :
                  ∀ (y z : ι →₀ R),
                    (fun f => ↑f default • x) (y + z) = (fun f => ↑f default • x) y + (fun f => ↑f default • x) z) },
          map_smul' :=
            (_ :
              ∀ (c : R) (y : ι →₀ R),
                AddHom.toFun
                    { toFun := fun f => ↑f default • x,
                      map_add' :=
                        (_ :
                          ∀ (y z : ι →₀ R),
                            (fun f => ↑f default • x) (y + z) =
                              (fun f => ↑f default • x) y + (fun f => ↑f default • x) z) }
                    (c • y) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      { toFun := fun f => ↑f default • x,
                        map_add' :=
                          (_ :
                            ∀ (y z : ι →₀ R),
                              (fun f => ↑f default • x) (y + z) =
                                (fun f => ↑f default • x) y + (fun f => ↑f default • x) z) }
                      y) }.toAddHom
      ((fun y => Finsupp.single default (Exists.choose (_ : ∃ r, r • x = y))) y) =
    y
case mpr.intro.intro
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
⊢ Nonempty (Basis ι R M)
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 => ?_ }⟩
no goals
case mpr.intro.intro.refine_1
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
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
simp [Finsupp.add_apply, add_smul]
case mpr.intro.intro.refine_2
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c✝ : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
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
case mpr.intro.intro.refine_2
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c✝ : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ AddHom.toFun
      { toFun := fun f => ↑f default • x,
        map_add' := (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
      (c • y) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun f => ↑f default • x,
          map_add' := (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
        y
simp only [Finsupp.coe_smul, Pi.smul_apply, RingHom.id_apply]
no goals
case mpr.intro.intro.refine_2
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c✝ : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
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
rw [← smul_assoc, smul_eq_mul]
case mpr.intro.intro.refine_3
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ (fun c => c • x)
      (↑((fun y => Finsupp.single default (Exists.choose (_ : ∃ r, r • x = y)))
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := fun f => ↑f default • x,
                      map_add' :=
                        (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (y : ι →₀ R),
                        AddHom.toFun
                            { toFun := fun f => ↑f default • x,
                              map_add' :=
                                (_ :
                                  ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                            (c • y) =
                          ↑(RingHom.id R) c •
                            AddHom.toFun
                              { toFun := fun f => ↑f default • x,
                                map_add' :=
                                  (_ :
                                    ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                              y) }.toAddHom
              f))
        default) =
    (fun c => c • x) (↑f default)
case mpr.intro.intro.refine_3
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ↑((fun y => Finsupp.single default (Exists.choose (_ : ∃ r, r • x = y)))
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => ↑f default • x,
                    map_add' :=
                      (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) },
                map_smul' :=
                  (_ :
                    ∀ (c : R) (y : ι →₀ R),
                      AddHom.toFun
                          { toFun := fun f => ↑f default • x,
                            map_add' :=
                              (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                          (c • y) =
                        ↑(RingHom.id R) c •
                          AddHom.toFun
                            { toFun := fun f => ↑f default • x,
                              map_add' :=
                                (_ :
                                  ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                            y) }.toAddHom
            f))
      default =
    ↑f default
refine' smul_left_injective _ nz _
case mpr.intro.intro.refine_3
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ Exists.choose
        (_ :
          ∃ r,
            r • x =
              AddHom.toFun
                {
                    toAddHom :=
                      { toFun := fun f => ↑f default • x,
                        map_add' :=
                          (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) },
                    map_smul' :=
                      (_ :
                        ∀ (c : R) (y : ι →₀ R),
                          AddHom.toFun
                              { toFun := fun f => ↑f default • x,
                                map_add' :=
                                  (_ :
                                    ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                              (c • y) =
                            ↑(RingHom.id R) c •
                              AddHom.toFun
                                { toFun := fun f => ↑f default • x,
                                  map_add' :=
                                    (_ :
                                      ∀ (y z : ι →₀ R),
                                        (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                                y) }.toAddHom
                f) •
      x =
    ↑f default • x
case mpr.intro.intro.refine_3
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ (fun c => c • x)
      (↑((fun y => Finsupp.single default (Exists.choose (_ : ∃ r, r • x = y)))
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := fun f => ↑f default • x,
                      map_add' :=
                        (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (y : ι →₀ R),
                        AddHom.toFun
                            { toFun := fun f => ↑f default • x,
                              map_add' :=
                                (_ :
                                  ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                            (c • y) =
                          ↑(RingHom.id R) c •
                            AddHom.toFun
                              { toFun := fun f => ↑f default • x,
                                map_add' :=
                                  (_ :
                                    ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                              y) }.toAddHom
              f))
        default) =
    (fun c => c • x) (↑f default)
simp only [Finsupp.single_eq_same]
no goals
case mpr.intro.intro.refine_3
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ Exists.choose
        (_ :
          ∃ r,
            r • x =
              AddHom.toFun
                {
                    toAddHom :=
                      { toFun := fun f => ↑f default • x,
                        map_add' :=
                          (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) },
                    map_smul' :=
                      (_ :
                        ∀ (c : R) (y : ι →₀ R),
                          AddHom.toFun
                              { toFun := fun f => ↑f default • x,
                                map_add' :=
                                  (_ :
                                    ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                              (c • y) =
                            ↑(RingHom.id R) c •
                              AddHom.toFun
                                { toFun := fun f => ↑f default • x,
                                  map_add' :=
                                    (_ :
                                      ∀ (y z : ι →₀ R),
                                        (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                                y) }.toAddHom
                f) •
      x =
    ↑f default • x
exact (w (f default • x)).choose_spec
case mpr.intro.intro.refine_4
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ Exists.choose (_ : ∃ r, r • x = y) • x = y
case mpr.intro.intro.refine_4
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => ↑f default • x,
              map_add' := (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) },
          map_smul' :=
            (_ :
              ∀ (c : R) (y : ι →₀ R),
                AddHom.toFun
                    { toFun := fun f => ↑f default • x,
                      map_add' :=
                        (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                    (c • y) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      { toFun := fun f => ↑f default • x,
                        map_add' :=
                          (_ : ∀ (y z : ι →₀ R), (↑y default + ↑z default) • x = ↑y default • x + ↑z default • x) }
                      y) }.toAddHom
      ((fun y => Finsupp.single default (Exists.choose (_ : ∃ r, r • x = y))) y) =
    y
simp only [Finsupp.single_eq_same]
no goals
case mpr.intro.intro.refine_4
ι✝ : Type ?u.616874
ι' : Type ?u.616877
R✝ : Type ?u.616880
R₂ : Type ?u.616883
K : Type ?u.616886
M✝ : Type ?u.616889
M' : Type ?u.616892
M'' : Type ?u.616895
V : Type u
V' : Type ?u.616900
inst✝¹⁰ : Semiring R✝
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R✝ M'
b b₁ : Basis ι✝ R✝ M✝
i : ι✝
c : R✝
x✝ : M✝
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_3
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ Exists.choose (_ : ∃ r, r • x = y) • x = y
exact (w y).choose_spec