awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
i : ι
R₁ :
  Eq (α := ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ S)
    (mapRange.linearMap (Algebra.linearMap R S) ∘ₗ
      (↑(repr (restrictScalars R b)) : ↥(span R (range (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ R))
    (LinearMap.domRestrict
      ((↑R :
          {S : Type u_7} →
            {M : Type u_5} →
              {M₂ : Type (max u_1 u_7)} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑b.repr : M →ₗ[S] ι →₀ S))
      (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
⊢ Eq.{u_7 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        ((((repr (restrictScalars R b) : (a : ↥(span R (range (⇑b : (a : ι) → M)))) → ι →₀ R) m : ι →₀ R) : (a : ι) → R)
            i :
          R) :
      S)
    ((((b.repr : (a : M) → ι →₀ S) (↑m : M) : ι →₀ S) : (a : ι) → S) i : S)

Tactic:
suffices
    Finsupp.mapRange.linearMap (Algebra.linearMap R S) ∘ₗ (b.restrictScalars R).repr.toLinearMap =
      ((b.repr : M →ₗ[S] ι →₀ S).restrictScalars R).domRestrict _
    by exact DFunLike.congr_fun (LinearMap.congr_fun this m) i
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
i : ι
⊢ Eq (α := ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ S)
    (mapRange.linearMap (Algebra.linearMap R S) ∘ₗ
      (↑(repr (restrictScalars R b)) : ↥(span R (range (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ R))
    (LinearMap.domRestrict
      ((↑R :
          {S : Type u_7} →
            {M : Type u_5} →
              {M₂ : Type (max u_1 u_7)} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑b.repr : M →ₗ[S] ι →₀ S))
      (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))

Tactic:
Basis.ext (b.restrictScalars R) fun _ => ?_

Premises used: Module.Basis.restrictScalars, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
i : ι
refine :
  ∀ (x : ι),
    Eq (α := ι →₀ S)
      ((mapRange.linearMap (Algebra.linearMap R S) ∘ₗ
              (↑(repr (restrictScalars R b)) : ↥(span R (range (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ R) :
            (a : ↥(span R (range (⇑b : (a : ι) → M)))) → ι →₀ S)
          ((restrictScalars R b : (a : ι) → ↥(span R (range (⇑b : (a : ι) → M)))) x) :
        ι →₀ S)
      ((LinearMap.domRestrict
              ((↑R :
                  {S : Type u_7} →
                    {M : Type u_5} →
                      {M₂ : Type (max u_1 u_7)} →
                        [inst : Semiring R] →
                          [inst_10 : Semiring S] →
                            [inst_11 : AddCommMonoid M] →
                              [inst_12 : AddCommMonoid M₂] →
                                [inst_13 : Module R M] →
                                  [inst_14 : Module R M₂] →
                                    [inst_15 : Module S M] →
                                      [inst_16 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (↑b.repr : M →ₗ[S] ι →₀ S))
              (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) :
            (a : ↥(span R (range (⇑b : (a : ι) → M)))) → ι →₀ S)
          ((restrictScalars R b : (a : ι) → ↥(span R (range (⇑b : (a : ι) → M)))) x) :
        ι →₀ S)
⊢ Eq (α := ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ S)
    (mapRange.linearMap (Algebra.linearMap R S) ∘ₗ
      (↑(repr (restrictScalars R b)) : ↥(span R (range (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ R))
    (LinearMap.domRestrict
      ((↑R :
          {S : Type u_7} →
            {M : Type u_5} →
              {M₂ : Type (max u_1 u_7)} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑b.repr : M →ₗ[S] ι →₀ S))
      (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))

Tactic:
refine Basis.ext (b.restrictScalars R) fun _ => ?_

Premises used: Module.Basis.restrictScalars, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
i x : ι
⊢ Eq (α := ι →₀ S)
    ((mapRange.linearMap (Algebra.linearMap R S) ∘ₗ
            (↑(repr (restrictScalars R b)) : ↥(span R (range (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ R) :
          (a : ↥(span R (range (⇑b : (a : ι) → M)))) → ι →₀ S)
        ((restrictScalars R b : (a : ι) → ↥(span R (range (⇑b : (a : ι) → M)))) x) :
      ι →₀ S)
    ((LinearMap.domRestrict
            ((↑R :
                {S : Type u_7} →
                  {M : Type u_5} →
                    {M₂ : Type (max u_1 u_7)} →
                      [inst : Semiring R] →
                        [inst_10 : Semiring S] →
                          [inst_11 : AddCommMonoid M] →
                            [inst_12 : AddCommMonoid M₂] →
                              [inst_13 : Module R M] →
                                [inst_14 : Module R M₂] →
                                  [inst_15 : Module S M] →
                                    [inst_16 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (↑b.repr : M →ₗ[S] ι →₀ S))
            (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) :
          (a : ↥(span R (range (⇑b : (a : ι) → M)))) → ι →₀ S)
        ((restrictScalars R b : (a : ι) → ↥(span R (range (⇑b : (a : ι) → M)))) x) :
      ι →₀ S)

Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_one,
    Basis.repr_self, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
    Algebra.linearMap_apply, LinearMap.domRestrict_apply,
    Basis.restrictScalars_apply, LinearMap.coe_restrictScalars]

Premises used: LinearMap.coe_restrictScalars, Algebra.linearMap_apply, Finsupp.mapRange.linearMap_apply, Module.Basis.restrictScalars_apply, LinearMap.coe_comp, map_one, LinearEquiv.coe_toLinearMap, Function.comp_apply, Finsupp.mapRange_single, Module.Basis.repr_self, LinearMap.domRestrict_apply
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) m ↔
    ∀ (i : ι),
      Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
        ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)

Tactic:
⟨fun hm i => ⟨(b.restrictScalars R).repr ⟨m, hm⟩ i, b.restrictScalars_repr_apply R ⟨m, hm⟩ i⟩,
      fun h => ?_⟩

Premises used: Module.Basis.restrictScalars_repr_apply, Module.Basis.repr, Subtype.mk, Module.Basis.restrictScalars, Iff.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
hm :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem.{u_7, u_7} (α := S) (γ := Set S)
          (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
          ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)),
    Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) m
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) m ↔
    ∀ (i : ι),
      Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
        ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)

Tactic:
refine
    ⟨fun hm i => ⟨(b.restrictScalars R).repr ⟨m, hm⟩ i, b.restrictScalars_repr_apply R ⟨m, hm⟩ i⟩,
      fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
h :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
rw :
  Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (sum ((b.repr : (a : M) → ι →₀ S) m) fun (i : ι) (a : S) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M))
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) m

Tactic:
rw [← b.linearCombination_repr m, Finsupp.linearCombination_apply S _]

Premises used: Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
h :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (sum ((b.repr : (a : M) → ι →₀ S) m) fun (i : ι) (a : S) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M))

Tactic:
sum_mem fun i _ => ?_

Premises used: Set.Mem, Finsupp.sum, sum_mem
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
h :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
refine :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_7} (M := S) ((b.repr : (a : M) → ι →₀ S) m)) i →
      Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
        ((fun (i : ι) (a : S) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) i
          ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i))
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (sum ((b.repr : (a : M) → ι →₀ S) m) fun (i : ι) (a : S) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M))

Tactic:
refine sum_mem fun i _ => ?_

Premises used: sum_mem
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
h :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
i : ι
h_1 : Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_7} (M := S) ((b.repr : (a : M) → ι →₀ S) m)) i
obtain :
  ∀ (w : R)
    (h :
      Eq.{u_7 + 1} (α := S) ((algebraMap R S : (a : R) → S) w : S)
        ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)),
    Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
      ((fun (i : ι) (a : S) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) i
        ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i))
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    ((fun (i : ι) (a : S) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) i
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i))

Tactic:
obtain ⟨_, h⟩ := h i
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
h_1 :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
i : ι
h_2 : Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_7} (M := S) ((b.repr : (a : M) → ι →₀ S) m)) i
w : R
h :
  Eq.{u_7 + 1} (α := S) ((algebraMap R S : (a : R) → S) w : S)
    ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
simp_rw :
  Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (HSMul.hSMul (β := M) w ((b : (a : ι) → M) i : M))
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    ((fun (i : ι) (a : S) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) i
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i))

Tactic:
simp_rw [← h, algebraMap_smul]

Premises used: algebraMap_smul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
h_1 :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
i : ι
h_2 : Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_7} (M := S) ((b.repr : (a : M) → ι →₀ S) m)) i
w : R
h :
  Eq.{u_7 + 1} (α := S) ((algebraMap R S : (a : R) → S) w : S)
    ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (HSMul.hSMul (β := M) w ((b : (a : ι) → M) i : M))

Tactic:
smul_mem _ _ (subset_span (Set.mem_range_self i))

Premises used: Set.mem_range_self, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : M
h_1 :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := S) (γ := Set S) (range.{u_7, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S))
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
i : ι
h_2 : Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_7} (M := S) ((b.repr : (a : M) → ι →₀ S) m)) i
w : R
h :
  Eq.{u_7 + 1} (α := S) ((algebraMap R S : (a : R) → S) w : S)
    ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (HSMul.hSMul (β := M) w ((b : (a : ι) → M) i : M))

Tactic:
exact smul_mem _ _ (subset_span (Set.mem_range_self i))

Premises used: Set.mem_range_self, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
M_1 : Type u_5
M' : Type u_6
M : Type u_7
R : Type u_8
inst : Ring R
inst_1 : Nontrivial R
inst_2 : IsAddTorsionFree R
inst_3 : AddCommGroup M
inst_4 : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M))
rw :
  Eq.{u_7 + 1} (α := Submodule ℤ M) (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M)
      (AddSubgroup.closure (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M))))
rw₁ :
  Eq.{u_7 + 1} (α := Submodule ℤ M) (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M)
      (toAddSubgroup (module_M := AddCommGroup.toIntModule M)
        (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
rw₂ rw₃ :
  Eq.{u_7 + 1} (α := Submodule ℤ M) (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq.{u_7 + 1} (α := Submodule ℤ M) (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)

Tactic:
rw [h, ← Submodule.span_int_eq_addSubgroupClosure, toAddSubgroup_toIntSubmodule]

Premises used: Submodule.toAddSubgroup_toIntSubmodule, Submodule.span_int_eq_addSubgroupClosure
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
M : Type u_7
R : Type u_8
inst : Ring R
inst_1 : Nontrivial R
inst_2 : IsAddTorsionFree R
inst_3 : AddCommGroup M
inst_4 : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M))
i : ι
⊢ Eq.{u_7 + 1} (α := M)
    ((↑((addSubgroupOfClosure A b h : (a : ι) → ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A))
            i) :
        M) :
      M)
    ((b : (a : ι) → M) i : M)

Tactic:
simp [addSubgroupOfClosure]

Premises used: Module.Basis.addSubgroupOfClosure
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
M : Type u_7
R : Type u_8
inst : Ring R
inst_1 : Nontrivial R
inst_2 : IsAddTorsionFree R
inst_3 : AddCommGroup M
inst_4 : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M))
x : ↥A
i : ι
this :
  Eq (α := ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A : Submodule ℤ M) →ₗ[ℤ] ι →₀ R)
    (mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (↑(addSubgroupOfClosure A b h).repr :
        ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A) →ₗ[ℤ] ι →₀ ℤ))
    (LinearMap.domRestrict
      ((↑ℤ :
          {S : Type u_8} →
            {M : Type u_7} →
              {M₂ : Type (max u_8 u_9)} →
                [inst : Semiring ℤ] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module ℤ M] →
                          [inst_9 : Module ℤ M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
        (↑b.repr : M →ₗ[R] ι →₀ R))
      ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A))
⊢ Eq.{u_8 + 1} (α := R)
    ((↑(((((addSubgroupOfClosure A b h).repr :
                    (a : ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)) → ι →₀ ℤ)
                  x :
                ι →₀ ℤ) :
              (a : ι) → ℤ)
            i) :
        R) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) (↑x : M) : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
DFunLike.congr_fun (LinearMap.congr_fun this x) i

Premises used: DFunLike.congr_fun, LinearMap.congr_fun