awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
succ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
succ₁ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = 1 * M.toAddSubmonoid
succ₂ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = M.toAddSubmonoid
succ₃ : (1 * M).toAddSubmonoid = M.toAddSubmonoid
⊢ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
have succ₄ : M.toAddSubmonoid = M.toAddSubmonoid
Tactic: rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : ∀ (h : n + 1 ≠ 0), (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
h : n + 1 + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid
have succ : M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid
Tactic: rw [ih n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : ∀ (h : n ≠ 0), (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid
have succ : ∀ (ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0)
  (h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
  (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
Tactic: cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]
Cleared hypotheses: n, ih, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : ∀ (h : n ≠ 0), (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
succ :
  ∀ (ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0)
    (h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
    (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid =
      HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
⊢ (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid
have succ₁ : ∀ (n : ℕ) (ih : ∀ (h : n + 1 ≠ 0), (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)) (h : n + 1 + 1 ≠ 0),
  (M ^ (n + 1)).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid
Tactic: cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]
Cleared hypotheses: n, ih, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
⊢ (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
have zero : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
Tactic: induction n with
  | zero => exact (h rfl).elim
  | succ n ih =>
    rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]
    cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
zero : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
⊢ (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
have succ : ∀ (n : ℕ) (ih : ∀ (h : n ≠ 0), (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n) (h : n + 1 ≠ 0),
  (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
Tactic: induction n with
  | zero => exact (h rfl).elim
  | succ n ih =>
    rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]
    cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
have inl : HPow.hPow (β := ℕ) M.toAddSubmonoid 0 ≤ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid
Tactic: obtain rfl | hn := Decidable.eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
inl : HPow.hPow (β := ℕ) M.toAddSubmonoid 0 ≤ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
have inr : ∀ (hn : n ≠ 0), M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
Tactic: obtain rfl | hn := Decidable.eq_or_ne n 0
-- 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
⊢ Eq (α := Submodule R A) 1 (LinearMap.range (Algebra.linearMap R A))
have rw : Eq (α := Submodule R A) (R ∙ 1) (LinearMap.range (Algebra.linearMap R A))
Tactic: rw [one_eq_span, LinearMap.span_singleton_eq_range,
    LinearMap.toSpanSingleton_one_eq_algebraLinearMap]
-- 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
rw : Eq (α := Submodule R A) (R ∙ 1) (LinearMap.range (Algebra.linearMap R A))
⊢ Eq (α := Submodule R A) 1 (LinearMap.range (Algebra.linearMap R A))
have rw₁ : Eq (α := Submodule R A) (LinearMap.range (LinearMap.toSpanSingleton R A 1)) (LinearMap.range (Algebra.linearMap R A))
Tactic: rw [one_eq_span, LinearMap.span_singleton_eq_range,
    LinearMap.toSpanSingleton_one_eq_algebraLinearMap]
-- 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
rw : Eq (α := Submodule R A) (R ∙ 1) (LinearMap.range (Algebra.linearMap R A))
rw₁ :
  Eq (α := Submodule R A) (LinearMap.range (LinearMap.toSpanSingleton R A 1)) (LinearMap.range (Algebra.linearMap R A))
⊢ Eq (α := Submodule R A) 1 (LinearMap.range (Algebra.linearMap R A))
have rw₂ : Eq (α := Submodule R A) (LinearMap.range (Algebra.linearMap R A)) (LinearMap.range (Algebra.linearMap R A))
Tactic: rw [one_eq_span, LinearMap.span_singleton_eq_range,
    LinearMap.toSpanSingleton_one_eq_algebraLinearMap]
-- 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
x : A
⊢ HSMul.hSMul (β := Submodule R A) x 1 = R ∙ x
have rw : HSMul.hSMul (β := Submodule R A) x (R ∙ 1) = R ∙ x
Tactic: rw [one_eq_span, smul_span, smul_set_singleton, smul_eq_mul, mul_one]
-- 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
x : A
rw : HSMul.hSMul (β := Submodule R A) x (R ∙ 1) = R ∙ x
⊢ HSMul.hSMul (β := Submodule R A) x 1 = R ∙ x
have rw₁ : Eq (α := Submodule R A) (span R (HSMul.hSMul (β := Set A) x {1})) (R ∙ x)
Tactic: rw [one_eq_span, smul_span, smul_set_singleton, smul_eq_mul, mul_one]
-- 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
x : A
rw : HSMul.hSMul (β := Submodule R A) x (R ∙ 1) = R ∙ x
rw₁ : Eq (α := Submodule R A) (span R (HSMul.hSMul (β := Set A) x {1})) (R ∙ x)
⊢ HSMul.hSMul (β := Submodule R A) x 1 = R ∙ x
have rw₂ : Eq (α := Submodule R A) (R ∙ HSMul.hSMul (β := A) x 1) (R ∙ x)
Tactic: rw [one_eq_span, smul_span, smul_set_singleton, smul_eq_mul, mul_one]
-- 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
x : A
rw : HSMul.hSMul (β := Submodule R A) x (R ∙ 1) = R ∙ x
rw₁ : Eq (α := Submodule R A) (span R (HSMul.hSMul (β := Set A) x {1})) (R ∙ x)
rw₂ : Eq (α := Submodule R A) (R ∙ HSMul.hSMul (β := A) x 1) (R ∙ x)
⊢ HSMul.hSMul (β := Submodule R A) x 1 = R ∙ x
have rw₃ : Eq (α := Submodule R A) (R ∙ x * 1) (R ∙ x)
Tactic: rw [one_eq_span, smul_span, smul_set_singleton, smul_eq_mul, mul_one]
-- 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
x : A
rw : HSMul.hSMul (β := Submodule R A) x (R ∙ 1) = R ∙ x
rw₁ : Eq (α := Submodule R A) (span R (HSMul.hSMul (β := Set A) x {1})) (R ∙ x)
rw₂ : Eq (α := Submodule R A) (R ∙ HSMul.hSMul (β := A) x 1) (R ∙ x)
rw₃ : Eq (α := Submodule R A) (R ∙ x * 1) (R ∙ x)
⊢ HSMul.hSMul (β := Submodule R A) x 1 = R ∙ x
have rw₄ : Eq (α := Submodule R A) (R ∙ x) (R ∙ x)
Tactic: rw [one_eq_span, smul_span, smul_set_singleton, smul_eq_mul, mul_one]
-- 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
r : R
h : IsUnit r
| 1
have rw : span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))
Tactic: rw [one_eq_span, ← span_singleton_smul_eq h, ← algebraMap_eq_smul_one]
-- 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
r : R
h : IsUnit r
⊢ Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
have conv_rhs : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
Tactic: conv_rhs => rw [one_eq_span, ← span_singleton_smul_eq h, ← algebraMap_eq_smul_one]
-- 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
r : R
h : IsUnit r
conv_rhs : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
⊢ Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
have conv_rhs₁ : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A)))
  (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A)))
Tactic: conv_rhs => rw [one_eq_span, ← span_singleton_smul_eq h, ← algebraMap_eq_smul_one]
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap 1 = 1
have h : ∀ (x : A'), x ∈ map f.toLinearMap 1 ↔ Membership.mem (γ := Submodule R A') 1 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
⊢ Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1
have h : ∀ (x : Aᵐᵒᵖ),
  Membership.mem (γ := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) x ↔
    Membership.mem (γ := Submodule R Aᵐᵒᵖ) 1 x
Tactic: ext x
-- 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
x : Aᵐᵒᵖ
⊢ Membership.mem (γ := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) x ↔
    Membership.mem (γ := Submodule R Aᵐᵒᵖ) 1 x
have h : ∀ (X : A),
  Membership.mem (γ := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) (op X) ↔
    Membership.mem (γ := Submodule R Aᵐᵒᵖ) 1 (op X)
Tactic: induction x
Cleared hypotheses: x
-- 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
⊢ Eq.{v + 1} (α := Submodule R A) (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1
have h : ∀ (x : A),
  Membership.mem (γ := Submodule R A) (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) x ↔
    Membership.mem (γ := Submodule R A) 1 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
⊢ Eq.{v + 1} (α := Submodule R A) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) 1) 1
have rw : Eq.{v + 1} (α := Submodule R A) (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1
Tactic: rw [← comap_equiv_eq_map_symm, comap_op_one]
-- 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
rw : Eq.{v + 1} (α := Submodule R A) (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1
⊢ Eq.{v + 1} (α := Submodule R A) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) 1) 1
have rw₁ : Eq.{v + 1} (α := Submodule R A) 1 1
Tactic: rw [← comap_equiv_eq_map_symm, comap_op_one]
-- 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
⊢ Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) (comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) 1) 1
have rw : Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1
Tactic: rw [← map_equiv_eq_comap_symm, map_op_one]
-- 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
rw : Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1
⊢ Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) (comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) 1) 1
have rw₁ : Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) 1 1
Tactic: rw [← map_equiv_eq_comap_symm, map_op_one]
-- 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
S T : Set A
⊢ HMul.hMul (α := Submodule R A) (span R S) (span R T) = span R (S * T)
have rw : Eq (α := Submodule R A) (map₂ (LinearMap.mul R A) (span R S) (span R T)) (span R (S * T))
Tactic: rw [mul_eq_map₂]
-- 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
| M * 1
have rw : HMul.hMul (α := Submodule R A) (span R (↑M : Set A)) (R ∙ 1)
Tactic: rw [one_eq_span, ← 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 : Semiring A
inst_2 : Algebra R A
M : Submodule R A
⊢ M * 1 = M
have conv_lhs : HMul.hMul (α := Submodule R A) (span R (↑M : Set A)) (R ∙ 1) = M
Tactic: conv_lhs => rw [one_eq_span, ← 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 : Semiring A
inst_2 : Algebra R A
M : Submodule R A
⊢ HMul.hMul (α := Submodule R A) (span R (↑M : Set A)) (R ∙ 1) = M
have rw : span R ((↑M : Set A) * {1}) = M
Tactic: rw [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 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap (M * N) =
    ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N)
have rw : map f.toLinearMap (map₂ (LinearMap.mul R A) M N) =
  ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N)
Tactic: rw [mul_eq_map₂]
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
⊢ ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N) =
    map f.toLinearMap M * map f.toLinearMap N
have rw : ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N) =
  map₂ (LinearMap.mul R A') (map f.toLinearMap M) (map f.toLinearMap N)
Tactic: rw [mul_eq_map₂]
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
⊢ ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N) =
    map₂ (LinearMap.mul R A') (map f.toLinearMap M) (map f.toLinearMap N)
have apply : Eq.{u_1 + 1} (α := Set (Submodule R A'))
  (range fun (i : ↥M) ↦
    map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
  (range fun (s : ↥(map f.toLinearMap M)) ↦
    map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
Tactic: apply congr_arg sSup
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
⊢ Eq.{u_1 + 1} (α := Set (Submodule R A'))
    (range fun (i : ↥M) ↦
      map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    (range fun (s : ↥(map f.toLinearMap M)) ↦
      map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
have h : ∀ (S : Submodule R A'),
  Membership.mem (γ := Set (Submodule R A'))
      (range fun (i : ↥M) ↦
        map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      S ↔
    Membership.mem (γ := Set (Submodule R A'))
      (range fun (s : ↥(map f.toLinearMap M)) ↦
        map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
      S
Tactic: ext S
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ Membership.mem (γ := Set (Submodule R A'))
      (range fun (i : ↥M) ↦
        map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      S ↔
    Membership.mem (γ := Set (Submodule R A'))
      (range fun (s : ↥(map f.toLinearMap M)) ↦
        map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
      S
have h : Membership.mem (γ := Set (Submodule R A'))
    (range fun (i : ↥M) ↦
      map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    S →
  Membership.mem (γ := Set (Submodule R A'))
    (range fun (s : ↥(map f.toLinearMap M)) ↦
      map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
    S
Tactic: constructor
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
h :
  Membership.mem (γ := Set (Submodule R A'))
      (range fun (i : ↥M) ↦
        map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      S →
    Membership.mem (γ := Set (Submodule R A'))
      (range fun (s : ↥(map f.toLinearMap M)) ↦
        map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
      S
⊢ Membership.mem (γ := Set (Submodule R A'))
      (range fun (i : ↥M) ↦
        map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      S ↔
    Membership.mem (γ := Set (Submodule R A'))
      (range fun (s : ↥(map f.toLinearMap M)) ↦
        map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
      S
have h₁ : Membership.mem (γ := Set (Submodule R A'))
    (range fun (s : ↥(map f.toLinearMap M)) ↦
      map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
    S →
  Membership.mem (γ := Set (Submodule R A'))
    (range fun (i : ↥M) ↦
      map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    S
Tactic: constructor
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy :
  (fun (i : ↥M) ↦ map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      y =
    S
⊢ Membership.mem (γ := Set (Submodule R A'))
    (range fun (s : ↥(map f.toLinearMap M)) ↦
      map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N))
    S
have h : (fun (s : ↥(map f.toLinearMap M)) ↦
      (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
        Submodule R A'))
    (Subtype.mk (p := fun (x : A') ↦ x ∈ map f.toLinearMap M) ((f : (a : A) → A') (↑y : A)) sorry) =
  S
Tactic: use ⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy :
  (fun (i : ↥M) ↦ map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      y =
    S
⊢ (fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      (Subtype.mk (p := fun (x : A') ↦ x ∈ map f.toLinearMap M) ((f : (a : A) → A') (↑y : A)) ⋯) =
    S
have h : Eq.{u_1 + 1} (α := Submodule R A')
  ((fun (s : ↥(map f.toLinearMap M)) ↦
      (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
        Submodule R A'))
    (Subtype.mk (p := fun (x : A') ↦ x ∈ map f.toLinearMap M) ((f : (a : A) → A') (↑y : A)) sorry))
  ((fun (i : ↥M) ↦ map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    y)
Tactic: refine Eq.trans ?_ hy