awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
rw₁ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₂ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₃ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) N
rw₄ :
  map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M *
      map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
rw₅ :
  map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M * map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₆ : map LinearMap.id (M * N) = map LinearMap.id M * map LinearMap.id N
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
rw₁ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₂ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₃ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) N
rw₄ :
  map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M *
      map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
rw₅ :
  map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M * map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
rw₆ : map LinearMap.id (M * N) = map LinearMap.id M * map LinearMap.id N
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₇ : M * N = map LinearMap.id M * map LinearMap.id N
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
rw₁ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₂ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₃ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) N
rw₄ :
  map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M *
      map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
rw₅ :
  map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M * map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
rw₆ : map LinearMap.id (M * N) = map LinearMap.id M * map LinearMap.id N
rw₇ : M * N = map LinearMap.id M * map LinearMap.id N
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₈ : M * N = M * map LinearMap.id N
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
rw₁ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₂ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₃ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) N
rw₄ :
  map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M *
      map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
rw₅ :
  map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M * map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
rw₆ : map LinearMap.id (M * N) = map LinearMap.id M * map LinearMap.id N
rw₇ : M * N = map LinearMap.id M * map LinearMap.id N
rw₈ : M * N = M * map LinearMap.id N
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₉ : M * N = M * N
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
    comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
have simp_rw : map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
  map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
    map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M
Tactic: simp_rw [comap_equiv_eq_map_symm, map_unop_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
⊢ (a • S) • T = a • S • T
have rw : HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
  a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
⊢ (a • S) • T = a • S • T
have rw₁ : HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
  a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
rw₁ :
  HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
⊢ (a • S) • T = a • S • T
have rw₂ : HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
  a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
rw₁ :
  HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₂ :
  HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
⊢ (a • S) • T = a • S • T
have rw₃ : HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
  a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
rw₁ :
  HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₂ :
  HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₃ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
⊢ (a • S) • T = a • S • T
have rw₄ : HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
  a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
rw₁ :
  HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₂ :
  HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₃ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₄ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
⊢ (a • S) • T = a • S • T
have rw₅ : span R (a • (↑S : Set A) * (↑T : Set A)) =
  a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
rw₁ :
  HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₂ :
  HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₃ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₄ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₅ :
  span R (a • (↑S : Set A) * (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
⊢ (a • S) • T = a • S • T
have rw₆ : span R (a • (↑S : Set A) * (↑T : Set A)) = HSMul.hSMul (β := Submodule R A) a (span R ((↑S : Set A) * (↑T : Set A)))
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
rw₁ :
  HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₂ :
  HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₃ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₄ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₅ :
  span R (a • (↑S : Set A) * (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₆ :
  span R (a • (↑S : Set A) * (↑T : Set A)) = HSMul.hSMul (β := Submodule R A) a (span R ((↑S : Set A) * (↑T : Set A)))
⊢ (a • S) • T = a • S • T
have rw₇ : Eq (α := Submodule R A) (span R (a • (↑S : Set A) * (↑T : Set A))) (span R (a • ((↑S : Set A) * (↑T : Set A))))
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
rw₁ :
  HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₂ :
  HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₃ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₄ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₅ :
  span R (a • (↑S : Set A) * (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₆ :
  span R (a • (↑S : Set A) * (↑T : Set A)) = HSMul.hSMul (β := Submodule R A) a (span R ((↑S : Set A) * (↑T : Set A)))
rw₇ : Eq (α := Submodule R A) (span R (a • (↑S : Set A) * (↑T : Set A))) (span R (a • ((↑S : Set A) * (↑T : Set A))))
⊢ (a • S) • T = a • S • T
have rw₈ : Eq (α := Submodule R A) (span R (a • ((↑S : Set A) * (↑T : Set A)))) (span R (a • ((↑S : Set A) * (↑T : Set A))))
Tactic: rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]