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 : CommSemiring A
inst_2 : Algebra R A
a : A
M : Submodule R A
⊢ 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
have rw : span R ((fun (x : A) ↦ a * x) '' (↑M : Set A)) = map (LinearMap.mulLeft R a) M
Tactic: rw [setSemiring_smul_def, SetSemiring.down_up, span_mul_span, singleton_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
I J : Submodule R A
a b : A
ha : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} a
hb : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} b
y : A
hy : y ∈ J
⊢ (a + b) * y ∈ I
have rw : a * y + b * y ∈ I
Tactic: rw [add_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
I J : Submodule R A
y : A
h : y ∈ J
⊢ 0 * y ∈ I
have rw : 0 ∈ I
Tactic: rw [zero_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
I J : Submodule R A
r : R
x : A
hx : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} x
y : A
hy : y ∈ J
⊢ r • x * y ∈ I
have rw : r • (x * y) ∈ I
Tactic: rw [Algebra.smul_mul_assoc]
-- 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
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
h_1 : y ∈ x • (↑J : Set A)
y' : A
hy' : y' ∈ (↑J : Set A)
xy'_eq_y : (fun (x_1 : A) ↦ x • x_1) y' = y
⊢ y ∈ (↑I : Set A)
have rw : (fun (x_1 : A) ↦ x • x_1) y' ∈ (↑I : Set A)
Tactic: rw [← xy'_eq_y]
-- 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
I J K : Submodule R A
⊢ I ≤ J / K ↔ I * K ≤ J
have rw : (∀ x ∈ I, ∀ z ∈ K, x * z ∈ J) ↔ I * K ≤ J
Tactic: rw [le_div_iff, mul_le]
-- 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
I J K : Submodule R A
rw : (∀ x ∈ I, ∀ z ∈ K, x * z ∈ J) ↔ I * K ≤ J
⊢ I ≤ J / K ↔ I * K ≤ J
have rw₁ : (∀ x ∈ I, ∀ z ∈ K, x * z ∈ J) ↔ ∀ m ∈ I, ∀ n ∈ K, m * n ∈ J
Tactic: rw [le_div_iff, mul_le]
-- 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
I : Submodule R A
⊢ 1 ≤ 1 / I ↔ I ≤ 1
have rw : 1 * I ≤ 1 ↔ I ≤ 1
Tactic: rw [le_div_iff_mul_le, one_mul]
-- 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
I : Submodule R A
rw : 1 * I ≤ 1 ↔ I ≤ 1
⊢ 1 ≤ 1 / I ↔ I ≤ 1
have rw₁ : I ≤ 1 ↔ I ≤ 1
Tactic: rw [le_div_iff_mul_le, one_mul]
-- 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
I J : Submodule R A
⊢ 1 ∈ I / J ↔ J ≤ I
have rw : 1 ≤ I / J ↔ J ≤ I
Tactic: rw [← one_le, le_div_iff_mul_le, one_mul]
-- 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
I J : Submodule R A
rw : 1 ≤ I / J ↔ J ≤ I
⊢ 1 ∈ I / J ↔ J ≤ I
have rw₁ : 1 * J ≤ I ↔ J ≤ I
Tactic: rw [← one_le, le_div_iff_mul_le, one_mul]
-- 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
I J : Submodule R A
rw : 1 ≤ I / J ↔ J ≤ I
rw₁ : 1 * J ≤ I ↔ J ≤ I
⊢ 1 ∈ I / J ↔ J ≤ I
have rw₂ : J ≤ I ↔ J ≤ I
Tactic: rw [← one_le, le_div_iff_mul_le, one_mul]
-- 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
I : Submodule R A
⊢ I * (1 / I) ≤ 1
have rw : ∀ m ∈ I, ∀ n ∈ 1 / I, Membership.mem (γ := Submodule R A) 1 (m * n)
Tactic: rw [Submodule.mul_le]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : n ∈ 1 / I
⊢ Membership.mem (γ := Submodule R A) 1 (m * n)
have hn₁ : ∀ y ∈ I, Membership.mem (γ := Submodule R A) 1 (n * y)
Tactic: rw [Submodule.mem_div_iff_forall_mul_mem] at hn
Cleared hypotheses: hn
-- 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
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, Membership.mem (γ := Submodule R A) 1 (n * y)
⊢ Membership.mem (γ := Submodule R A) 1 (m * n)
have rw : Membership.mem (γ := Submodule R A) 1 (n * m)
Tactic: rw [mul_comm]
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
⊢ map h.toLinearMap (I / J) = map h.toLinearMap I / map h.toLinearMap J
have h₁ : ∀ (x : B), x ∈ map h.toLinearMap (I / J) ↔ x ∈ map h.toLinearMap I / map h.toLinearMap J
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 : CommSemiring A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ x ∈ map h.toLinearMap (I / J) ↔ x ∈ map h.toLinearMap I / map h.toLinearMap J
have h₁ : (∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x) ↔
  ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
Tactic: simp only [mem_map, mem_div_iff_forall_mul_mem, AlgEquiv.toLinearMap_apply]
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ (∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x) ↔
    ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
have h₁ : (∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x) →
  ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
Tactic: constructor
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
h₁ :
  (∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x) →
    ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
⊢ (∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x) ↔
    ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
have h₂ : (∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y) →
  ∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x
Tactic: constructor
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
⊢ ∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x
have h₁ : ∀ (z : A) (hz : z ∈ J), HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z ∈ I
Tactic: refine ⟨h.symm x, fun z hz => ?_, h.apply_symm_apply x⟩
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
z : A
hz : z ∈ J
⊢ HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z ∈ I
have h₁ : ∀ (xz : A) (xz_mem : xz ∈ I) (hxz : (h : (a : A) → B) xz = HMul.hMul (β := B) x ((h : (a : A) → B) z : B)),
  HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z ∈ I
Tactic: obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : (h : (a : A) → B) xz = HMul.hMul (β := B) x ((h : (a : A) → B) z : B)
⊢ HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z ∈ I
have h₁ : HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z = xz
Tactic: convert! xz_mem
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : (h : (a : A) → B) xz = HMul.hMul (β := B) x ((h : (a : A) → B) z : B)
⊢ HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z = xz
have h₁ : Eq.{u_1 + 1} (α := B) ((h : (a : A) → B) (HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z) : B)
  ((h : (a : A) → B) xz : B)
Tactic: apply h.injective
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : (h : (a : A) → B) xz = HMul.hMul (β := B) x ((h : (a : A) → B) z : B)
⊢ Eq.{u_1 + 1} (α := B) ((h : (a : A) → B) (HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z) : B)
    ((h : (a : A) → B) xz : B)
have h₁ : HMul.hMul (α := B) (β := B) ((h : (a : A) → B) ((h.symm : (a : B) → A) x : A) : B) ((h : (a : A) → B) z : B) =
  (h : (a : A) → B) xz
Tactic: rw [map_mul, h.apply_symm_apply, hxz]
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : (h : (a : A) → B) xz = HMul.hMul (β := B) x ((h : (a : A) → B) z : B)
h₁ :
  HMul.hMul (α := B) (β := B) ((h : (a : A) → B) ((h.symm : (a : B) → A) x : A) : B) ((h : (a : A) → B) z : B) =
    (h : (a : A) → B) xz
⊢ Eq.{u_1 + 1} (α := B) ((h : (a : A) → B) (HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z) : B)
    ((h : (a : A) → B) xz : B)
have h₂ : HMul.hMul (β := B) x ((h : (a : A) → B) z : B) = (h : (a : A) → B) xz
Tactic: rw [map_mul, h.apply_symm_apply, hxz]
-- 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
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : (h : (a : A) → B) xz = HMul.hMul (β := B) x ((h : (a : A) → B) z : B)
h₁ :
  HMul.hMul (α := B) (β := B) ((h : (a : A) → B) ((h.symm : (a : B) → A) x : A) : B) ((h : (a : A) → B) z : B) =
    (h : (a : A) → B) xz
h₂ : HMul.hMul (β := B) x ((h : (a : A) → B) z : B) = (h : (a : A) → B) xz
⊢ Eq.{u_1 + 1} (α := B) ((h : (a : A) → B) (HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z) : B)
    ((h : (a : A) → B) xz : B)
have h₃ : HMul.hMul (β := B) x ((h : (a : A) → B) z : B) = HMul.hMul (β := B) x ((h : (a : A) → B) z : B)
Tactic: rw [map_mul, h.apply_symm_apply, hxz]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
⊢ restrictScalars S (HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N) =
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1 : ∀ (x : M)
  (x_in :
    Membership.mem (γ := Submodule S M)
      (restrictScalars S (HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N)) x),
  x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: refine le_antisymm (fun x x_in ↦ ?_) (set_smul_le _ _ _ fun r x r_in x_in ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
refine_1 :
  ∀ (x : M)
    (x_in :
      Membership.mem (γ := Submodule S M)
        (restrictScalars S (HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N)) x),
    x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
⊢ restrictScalars S (HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N) =
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_2 : ∀ (r : S) (x : M) (r_in : r ∈ s) (x_in : Membership.mem (γ := Submodule S M) (restrictScalars S N) x),
  Membership.mem (γ := Submodule S M)
    (restrictScalars S (HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N)) (r • x)
Tactic: refine le_antisymm (fun x x_in ↦ ?_) (set_smul_le _ _ _ fun r x r_in x_in ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in :
  Membership.mem (γ := Submodule S M)
    (restrictScalars S (HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N)) x
⊢ x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have x_in₁ : x ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
Tactic: rw [restrictScalars_mem] at x_in
Cleared hypotheses: x_in
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
⊢ x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1 : ∀ ⦃r : R⦄ ⦃n : M⦄ (mem₁ : Membership.mem (γ := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) r) (mem₂ : n ∈ N),
  r • n ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: refine set_smul_inductionOn x x_in ?_ ?_ (fun _ _ _ _ h h' ↦ add_mem h h') (zero_mem _)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
refine_1 :
  ∀ ⦃r : R⦄ ⦃n : M⦄ (mem₁ : Membership.mem (γ := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) r) (mem₂ : n ∈ N),
    r • n ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
⊢ x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N),
  m ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N) →
    r • m ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: refine set_smul_inductionOn x x_in ?_ ?_ (fun _ _ _ _ h h' ↦ add_mem h h') (zero_mem _)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x_1 : M
x_in_1 : x_1 ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
x : M
r : S
r_in : r ∈ s
x_in : x ∈ N
⊢ HSMul.hSMul.{u, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x ∈
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1 : r • x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: rw [algebraMap_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
r : R
y : M
h : y ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
h' : y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
⊢ r • y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1 : ∀ (c : Finsupp.{u, u_2} R ↥N) (c_supp : (↑c.support : Set R) ⊆ (⇑(algebraMap S R) : (a : S) → R) '' s)
  (hc : r • y = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)),
  r • y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: obtain ⟨c, c_supp, hc⟩ := (mem_set_smul ..).mp <| smul_mem _ r h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
r : R
y : M
h : y ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
h' : y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
c : Finsupp.{u, u_2} R ↥N
c_supp : (↑c.support : Set R) ⊆ (⇑(algebraMap S R) : (a : S) → R) '' s
hc : r • y = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
⊢ r • y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1 : ∑ x ∈ c.support, HSMul.hSMul (β := M) x (↑((c : (a : R) → ↥N) x) : M) ∈
  HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: simp only [hc, Finsupp.sum, AddSubmonoidClass.coe_finsetSum, SetLike.val_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
r : R
y : M
h : y ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
h' : y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
c : Finsupp.{u, u_2} R ↥N
c_supp : (↑c.support : Set R) ⊆ (⇑(algebraMap S R) : (a : S) → R) '' s
hc : r • y = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
⊢ ∑ x ∈ c.support, HSMul.hSMul (β := M) x (↑((c : (a : R) → ↥N) x) : M) ∈
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1 : ∀ (u : R) (u_in : u ∈ c.support),
  HSMul.hSMul (β := M) u (↑((c : (a : R) → ↥N) u) : M) ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: refine sum_mem fun u u_in ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
r : R
y : M
h : y ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
h' : y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
c : Finsupp.{u, u_2} R ↥N
c_supp : (↑c.support : Set R) ⊆ (⇑(algebraMap S R) : (a : S) → R) '' s
hc : r • y = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
u : R
u_in : u ∈ c.support
⊢ HSMul.hSMul (β := M) u (↑((c : (a : R) → ↥N) u) : M) ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1 : ∀ (u : S) (u_in' : u ∈ s) (u_in : Membership.mem (α := R) c.support ((algebraMap S R : (a : S) → R) u : R)),
  HSMul.hSMul.{u, u_2, u_2} (α := R) (β := M) ((algebraMap S R : (a : S) → R) u : R)
      (↑((c : (a : R) → ↥N) ((algebraMap S R : (a : S) → R) u)) : M) ∈
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: obtain ⟨u, u_in', rfl⟩ := c_supp (Finset.mem_coe.mpr u_in)
Cleared hypotheses: u, u_in
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
r : R
y : M
h : y ∈ HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
h' : y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
c : Finsupp.{u, u_2} R ↥N
c_supp : (↑c.support : Set R) ⊆ (⇑(algebraMap S R) : (a : S) → R) '' s
hc : r • y = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
u : S
u_in' : u ∈ s
u_in : Membership.mem (α := R) c.support ((algebraMap S R : (a : S) → R) u : R)
⊢ HSMul.hSMul.{u, u_2, u_2} (α := R) (β := M) ((algebraMap S R : (a : S) → R) u : R)
      (↑((c : (a : R) → ↥N) ((algebraMap S R : (a : S) → R) u)) : M) ∈
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
have refine_1 : HSMul.hSMul (β := M) u (↑((c : (a : R) → ↥N) ((algebraMap S R : (a : S) → R) u)) : M) ∈
  HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
Tactic: rw [algebraMap_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
M : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
s : Set S
N : Submodule R M
r : S
x : M
r_in : r ∈ s
x_in : Membership.mem (γ := Submodule S M) (restrictScalars S N) x
⊢ Membership.mem (γ := Submodule S M)
    (restrictScalars S (HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N)) (r • x)
have refine_2 : HSMul.hSMul.{u, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x ∈
  HSMul.hSMul.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N
Tactic: rw [restrictScalars_mem, ← algebraMap_smul R r]