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 : Submodule R A
n : ℕ
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
have rw : comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) = map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
Tactic: rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]
-- 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 : Submodule R A
n : ℕ
rw :
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) = map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
have rw₁ : comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
Tactic: rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]
-- 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 : Submodule R A
n : ℕ
rw :
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) = map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
rw₁ :
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
have rw₂ : comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n =
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
Tactic: rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]
-- 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
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
have rw : comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
Tactic: rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]
-- 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
n : ℕ
M : Submodule R Aᵐᵒᵖ
rw :
  comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
⊢ map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
have rw₁ : comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
Tactic: rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]
-- 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
n : ℕ
M : Submodule R Aᵐᵒᵖ
rw :
  comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
rw₁ : comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
⊢ map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
have rw₂ : comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n = comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
Tactic: rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]
-- 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
inst_3 : FaithfulSMul R A
x : A
h : Eq (α := Submodule R A) (R ∙ x) 1
⊢ ∃ (r : Rˣ), x = (algebraMap R A : (a : R) → A) (↑r : R)
have obtain : ∀ (r : R) (h : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1),
  ∃ (r_1 : Rˣ),
    Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)
Tactic: obtain ⟨r, rfl⟩ := mem_one.mp (h ▸ mem_span_singleton_self x)
Cleared hypotheses: x, h
-- 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
inst_3 : FaithfulSMul R A
r : R
h : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
⊢ ∃ (r_1 : Rˣ),
    Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)
have have : ∀ (r' : R) (eq : HSMul.hSMul (β := A) r' ((algebraMap R A : (a : R) → A) r : A) = (algebraMap R A : (a : R) → A) 1),
  ∃ (r_1 : Rˣ),
    Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)
Tactic: have ⟨r', eq⟩ := mem_span_singleton.mp (h ▸ algebraMap_mem 1)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
r : R
h : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
r' : R
eq : HSMul.hSMul (β := A) r' ((algebraMap R A : (a : R) → A) r : A) = (algebraMap R A : (a : R) → A) 1
⊢ ∃ (r_1 : Rˣ),
    Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)
have eq₁ : r' * r = 1
Tactic: rw [Algebra.smul_def, ← map_mul, (FaithfulSMul.algebraMap_injective R A).eq_iff] at eq
Cleared hypotheses: eq
-- 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
inst_3 : FaithfulSMul R A
⊢ Eq (α := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R))
    (Submonoid.map (F := R →+* A) (algebraMap R A) (IsUnit.submonoid R))
have h : ∀ (x : A),
  Membership.mem (γ := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R)) x ↔
    Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) (IsUnit.submonoid R)) x
Tactic: ext
-- 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
inst_3 : FaithfulSMul R A
x : A
⊢ Membership.mem (γ := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R)) x ↔
    Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) (IsUnit.submonoid R)) x
have h : Membership.mem (γ := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R)) x ↔
  ∃ (u : Rˣ), x = (algebraMap R A : (a : R) → A) (↑u : R)
Tactic: simp_rw [Submonoid.mem_map, IsUnit.mem_submonoid_iff, IsUnit, existsAndEq, true_and, eq_comm]
-- 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
inst_3 : FaithfulSMul R A
⊢ Eq (α := Subgroup Aˣ) (MonoidHom.ker (M := (Submodule R A)ˣ) (Units.map (↑(spanSingleton R) : A →* Submodule R A)))
    (MonoidHom.range (G := Rˣ) (Units.map (↑(algebraMap R A) : R →* A)))
have h : ∀ (x : Aˣ),
  Membership.mem (γ := Subgroup Aˣ)
      (MonoidHom.ker (M := (Submodule R A)ˣ) (Units.map (↑(spanSingleton R) : A →* Submodule R A))) x ↔
    Membership.mem (γ := Subgroup Aˣ) (MonoidHom.range (G := Rˣ) (Units.map (↑(algebraMap R A) : R →* A))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s, span R (M i)) (span R (∏ i ∈ s, M i))
have refine_1 : Eq.{v + 1} (α := Submodule R A) (∏ i ∈ ∅, span R (M i)) (span R (∏ i ∈ ∅, M i))
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
refine_1 : Eq.{v + 1} (α := Submodule R A) (∏ i ∈ ∅, span R (M i)) (span R (∏ i ∈ ∅, M i))
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s, span R (M i)) (span R (∏ i ∈ s, M i))
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s, span R (M i)) (span R (∏ i ∈ s, M i)) →
      Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s, span R (M i)) (span R (∏ i ∈ insert a s, M i))
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a : ι
s_1 : Finset ι
H : a ∉ s_1
ih : Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s_1, span R (M i)) (span R (∏ i ∈ s_1, M i))
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s_1, span R (M i)) (span R (∏ i ∈ insert a s_1, M i))
have refine_2 : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (∏ i ∈ insert a s_1, M i)
Tactic: rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a : ι
s_1 : Finset ι
H : a ∉ s_1
ih : Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s_1, span R (M i)) (span R (∏ i ∈ s_1, M i))
refine_2 : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (∏ i ∈ insert a s_1, M i)
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s_1, span R (M i)) (span R (∏ i ∈ insert a s_1, M i))
have refine_2₁ : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (M a * ∏ x ∈ s_1, M x)
Tactic: rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a : ι
s_1 : Finset ι
H : a ∉ s_1
ih : Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s_1, span R (M i)) (span R (∏ i ∈ s_1, M i))
refine_2 : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (∏ i ∈ insert a s_1, M i)
refine_2₁ : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (M a * ∏ x ∈ s_1, M x)
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s_1, span R (M i)) (span R (∏ i ∈ insert a s_1, M i))
have refine_2₂ : HMul.hMul (α := Submodule R A) (span R (M a)) (span R (∏ i ∈ s_1, M i)) = span R (M a * ∏ x ∈ s_1, M x)
Tactic: rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a : ι
s_1 : Finset ι
H : a ∉ s_1
ih : Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s_1, span R (M i)) (span R (∏ i ∈ s_1, M i))
refine_2 : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (∏ i ∈ insert a s_1, M i)
refine_2₁ : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (M a * ∏ x ∈ s_1, M x)
refine_2₂ : HMul.hMul (α := Submodule R A) (span R (M a)) (span R (∏ i ∈ s_1, M i)) = span R (M a * ∏ x ∈ s_1, M x)
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s_1, span R (M i)) (span R (∏ i ∈ insert a s_1, M i))
have refine_2₃ : Eq (α := Submodule R A) (span R (M a * ∏ i ∈ s_1, M i)) (span R (M a * ∏ x ∈ s_1, M x))
Tactic: rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
x : ι → A
⊢ Eq (α := Submodule R A) (∏ i ∈ s, R ∙ x i) (R ∙ ∏ i ∈ s, x i)
have rw : Eq (α := Submodule R A) (span R (∏ i ∈ s, {x i})) (R ∙ ∏ i ∈ s, x i)
Tactic: rw [prod_span, Set.finsetProd_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
x : ι → A
rw : Eq (α := Submodule R A) (span R (∏ i ∈ s, {x i})) (R ∙ ∏ i ∈ s, x i)
⊢ Eq (α := Submodule R A) (∏ i ∈ s, R ∙ x i) (R ∙ ∏ i ∈ s, x i)
have rw₁ : Eq (α := Submodule R A) (R ∙ ∏ i ∈ s, x i) (R ∙ ∏ i ∈ s, x i)
Tactic: rw [prod_span, Set.finsetProd_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
⊢ (s * t) • P = s • t • P
have simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s * t)) * P =
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) *
    (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P)
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
simp_rw :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s * t)) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) *
      (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P)
⊢ (s * t) • P = s • t • P
have simp_rw₁ : span R
      (HMul.hMul (α := Set A) (β := Set A) ((SetSemiring.down : (a : SetSemiring A) → Set A) s : Set A)
        ((SetSemiring.down : (a : SetSemiring A) → Set A) t : Set A)) *
    P =
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) *
    (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P)
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
simp_rw :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s * t)) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) *
      (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P)
simp_rw₁ :
  span R
        (HMul.hMul (α := Set A) (β := Set A) ((SetSemiring.down : (a : SetSemiring A) → Set A) s : Set A)
          ((SetSemiring.down : (a : SetSemiring A) → Set A) t : Set A)) *
      P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) *
      (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P)
⊢ (s * t) • P = s • t • P
have simp_rw₂ : span R
      (HMul.hMul (α := Set A) (β := Set A) ((SetSemiring.down : (a : SetSemiring A) → Set A) s : Set A)
        ((SetSemiring.down : (a : SetSemiring A) → Set A) t : Set A)) *
    P =
  HMul.hMul (α := Submodule R A) (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s))
      (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t)) *
    P
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
⊢ HSMul.hSMul (α := SetSemiring A) 1 P = P
have simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 1) * P = P
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_one, ← one_eq_span_one_set, one_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 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 1) * P = P
⊢ HSMul.hSMul (α := SetSemiring A) 1 P = P
have simp_rw₁ : span R 1 * P = P
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_one, ← one_eq_span_one_set, one_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 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 1) * P = P
simp_rw₁ : span R 1 * P = P
⊢ HSMul.hSMul (α := SetSemiring A) 1 P = P
have simp_rw₂ : 1 * P = P
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_one, ← one_eq_span_one_set, one_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 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
⊢ (s + t) • P = s • P + t • P
have simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s + t)) * P =
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
simp_rw :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s + t)) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
⊢ (s + t) • P = s • P + t • P
have simp_rw₁ : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s ∪ (SetSemiring.down : (a : SetSemiring A) → Set A) t) * P =
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
simp_rw :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s + t)) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
simp_rw₁ :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s ∪ (SetSemiring.down : (a : SetSemiring A) → Set A) t) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
⊢ (s + t) • P = s • P + t • P
have simp_rw₂ : (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) ⊔
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t)) *
    P =
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
simp_rw :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s + t)) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
simp_rw₁ :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s ∪ (SetSemiring.down : (a : SetSemiring A) → Set A) t) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
simp_rw₂ :
  (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) ⊔
        span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t)) *
      P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
⊢ (s + t) • P = s • P + t • P
have simp_rw₃ : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P ⊔
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P =
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
⊢ HSMul.hSMul (α := SetSemiring A) 0 P = 0
have simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 0) * P = 0
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 0) * P = 0
⊢ HSMul.hSMul (α := SetSemiring A) 0 P = 0
have simp_rw₁ : span R ∅ * P = 0
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 0) * P = 0
simp_rw₁ : span R ∅ * P = 0
⊢ HSMul.hSMul (α := SetSemiring A) 0 P = 0
have simp_rw₂ : ⊥ * P = 0
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 0) * P = 0
simp_rw₁ : span R ∅ * P = 0
simp_rw₂ : ⊥ * P = 0
⊢ HSMul.hSMul (α := SetSemiring A) 0 P = 0
have simp_rw₃ : Eq.{v + 1} (α := Submodule R A) ⊥ 0
Tactic: simp_rw [HSMul.hSMul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
a : A
M : Submodule R A
| HSMul.hSMul (α := SetSemiring A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A) M
have rw : HSMul.hSMul (α := SetSemiring A) (β := Submodule R A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A)
  (span R (↑M : Set A))
Tactic: rw [← span_eq M]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
a : A
M : Submodule R A
⊢ HSMul.hSMul (α := SetSemiring A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A) M =
    map (LinearMap.mulLeft R a) M
have conv_lhs : HSMul.hSMul (α := SetSemiring A) (β := Submodule R A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A)
    (span R (↑M : Set A)) =
  map (LinearMap.mulLeft R a) M
Tactic: conv_lhs => rw [← span_eq M]