awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
    ∀ (i j : ι),
      z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
          HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
        HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
          HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)
c d : A
⊢ c * d * z = c * (d * z)
have rw : (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) i : R)
          ((b : (a : ι) → A) i : A) *
        ∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R)
            ((b : (a : ι) → A) a : A)) *
    z =
  (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) a : R)
        ((b : (a : ι) → A) a : A)) *
    ((∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R)
          ((b : (a : ι) → A) a : A)) *
      z)
Tactic: rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
    ∀ (i j : ι),
      z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
          HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
        HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
          HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)
c d : A
⊢ (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) i : R)
            ((b : (a : ι) → A) i : A) *
          ∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
            HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A)
              ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → A) a : A)) *
      z =
    (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) a : R)
          ((b : (a : ι) → A) a : A)) *
      ((∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R)
            ((b : (a : ι) → A) a : A)) *
        z)
have simp_rw : (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
        (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A)
          (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
              HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A)
                ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → A) a : A) :
            A))) *
    z =
  (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) a : R)
        ((b : (a : ι) → A) a : A)) *
    ((∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R)
          ((b : (a : ι) → A) a : A)) *
      z)
Tactic: simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
               Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
               (h.2 _ _).2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
    ∀ (i j : ι),
      z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
          HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
        HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
          HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)
case case₁ : ∀ (c d : A), c * d * z = c * (d * z)
⊢ ∀ (a b : A), a * b * z = a * (b * z)
have case₂ : ∀ (c d : A),
  (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) i : R)
            ((b : (a : ι) → A) i : A) *
          ∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
            HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A)
              ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → A) a : A)) *
      z =
    (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) a : R)
          ((b : (a : ι) → A) a : A)) *
      ((∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R)
            ((b : (a : ι) → A) a : A)) *
        z)
Tactic: case right_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
               Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
               (h.2 _ _).2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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.{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)
have 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))))
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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))))
have 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)
Tactic: refine Basis.ext (b.restrictScalars R) fun _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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)
have 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
Tactic: refine
    ⟨fun hm i => ⟨(b.restrictScalars R).repr ⟨m, hm⟩ i, b.restrictScalars_repr_apply R ⟨m, hm⟩ i⟩,
      fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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))) m
have 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))
Tactic: rw [← b.linearCombination_repr m, Finsupp.linearCombination_apply S _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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))
have 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))
Tactic: refine sum_mem fun i _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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
⊢ 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))
have 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))
Tactic: obtain ⟨_, h⟩ := h i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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)))
    ((fun (i : ι) (a : S) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) i
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i))
have 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))
Tactic: simp_rw [← h, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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))
⊢ Eq.{u_7 + 1} (α := Submodule ℤ M) (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)
have 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))))
Tactic: rw [h, ← Submodule.span_int_eq_addSubgroupClosure, toAddSubgroup_toIntSubmodule]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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))))
⊢ Eq.{u_7 + 1} (α := Submodule ℤ M) (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)
have 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)))))
Tactic: rw [h, ← Submodule.span_int_eq_addSubgroupClosure, toAddSubgroup_toIntSubmodule]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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)))))
⊢ Eq.{u_7 + 1} (α := Submodule ℤ M) (span ℤ (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)
have 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)))
Tactic: rw [h, ← Submodule.span_int_eq_addSubgroupClosure, toAddSubgroup_toIntSubmodule]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
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 : ι
⊢ 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)
have suffices : 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))
Tactic: suffices Finsupp.mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (b.addSubgroupOfClosure A h).repr.toLinearMap =
        ((b.repr : M →ₗ[R] ι →₀ R).restrictScalars ℤ).domRestrict A.toIntSubmodule by
    exact DFunLike.congr_fun (LinearMap.congr_fun this x) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
hs : LinearIndepOn K id s
⊢ range (ι := (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4))
      (⇑(extend (s := s) hs) : (a : (↑(hs.extend ⋯) : Type u_4)) → V) =
    hs.extend (s := s) (t := univ) ⋯
have rw : range (ι := (↑(hs.extend (s := s) (t := univ) sorry) : Type u_4))
    (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := univ) sorry)) =
  hs.extend (s := s) (t := univ) sorry
Tactic: rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]