awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Operations
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 : A
hx : ∀ y ∈ J, x * y ∈ I
y : A
hy : y ∈ J
⊢ ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = HMul.hMul (α := B) (β := B) ((h : (a : A) → B) x : B) ((h : (a : A) → B) y : B)

Tactic:
⟨x * y, hx _ hy, map_mul h x y⟩

Premises used: HMul.hMul, map_mul, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Operations
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 : A
hx : ∀ y ∈ J, x * y ∈ I
y : A
hy : y ∈ J
⊢ ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = HMul.hMul (α := B) (β := B) ((h : (a : A) → B) x : B) ((h : (a : A) → B) y : B)

Tactic:
exact ⟨x * y, hx _ hy, map_mul h x y⟩
-- Module: Mathlib.Algebra.Algebra.Operations
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

Tactic:
⟨h.symm x, fun z hz => ?_, h.apply_symm_apply x⟩

Premises used: AlgEquiv.symm, AlgEquiv.apply_symm_apply, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Operations
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
h₁ : ∀ (z : A) (hz : z ∈ J), HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z ∈ I
⊢ ∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x

Tactic:
refine ⟨h.symm x, fun z hz => ?_, h.apply_symm_apply x⟩
-- Module: Mathlib.Algebra.Algebra.Operations
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
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
⊢ HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z ∈ I

Tactic:
obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩

Premises used: And.intro, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
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)
⊢ xz ∈ I

Tactic:
xz_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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 (α := A) ((h.symm : (a : B) → A) x : A) z = xz
⊢ HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z ∈ I

Tactic:
convert! xz_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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₁ :
  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)
⊢ HMul.hMul (α := A) ((h.symm : (a : B) → A) x : A) z = xz

Tactic:
apply h.injective

Premises used: AlgEquiv.injective
-- Module: Mathlib.Algebra.Algebra.Operations
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
h₃ h₄ : HMul.hMul (β := B) x ((h : (a : A) → B) z : B) = 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)

Tactic:
rw [map_mul, h.apply_symm_apply, hxz]

Premises used: AlgEquiv.apply_symm_apply, map_mul
-- Module: Mathlib.Algebra.Algebra.Operations
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)

Tactic:
le_antisymm (fun x x_in ↦ ?_) (set_smul_le _ _ _ fun r x r_in x_in ↦ ?_)

Premises used: le_antisymm, Submodule.set_smul_le
-- Module: Mathlib.Algebra.Algebra.Operations
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)
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)
⊢ 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)

Tactic:
refine le_antisymm (fun x x_in ↦ ?_) (set_smul_le _ _ _ fun r x r_in x_in ↦ ?_)

Premises used: le_antisymm, Submodule.set_smul_le
-- Module: Mathlib.Algebra.Algebra.Operations
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.{u, u_2, u_2} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' s) N

Tactic:
rw [restrictScalars_mem] at x_in

Premises used: Submodule.restrictScalars_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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)

Tactic:
set_smul_inductionOn x x_in ?_ ?_ (fun _ _ _ _ h h' ↦ add_mem h h') (zero_mem _)

Premises used: Submodule.set_smul_inductionOn
-- Module: Mathlib.Algebra.Algebra.Operations
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)
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)
⊢ x ∈ 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 _)
-- Module: Mathlib.Algebra.Algebra.Operations
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
refine_1 : r • x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S 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)

Tactic:
rw [algebraMap_smul]

Premises used: algebraMap_smul
-- Module: Mathlib.Algebra.Algebra.Operations
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
⊢ r • x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)

Tactic:
mem_set_smul_of_mem_mem r_in x_in

Premises used: Submodule.mem_set_smul_of_mem_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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
⊢ r • x ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)

Tactic:
exact mem_set_smul_of_mem_mem r_in x_in

Premises used: Submodule.mem_set_smul_of_mem_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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)
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)
⊢ 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

Premises used: Iff.mp, Submodule.mem_set_smul, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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)
refine_1 :
  ∑ x ∈ c.support, HSMul.hSMul (β := M) x (↑((c : (a : R) → ↥N) x) : M) ∈
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)
⊢ r • y ∈ HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)

Tactic:
simp only [hc, Finsupp.sum, AddSubmonoidClass.coe_finsetSum, SetLike.val_smul]

Premises used: Finsupp.sum, AddSubmonoidClass.coe_finsetSum, SetLike.val_smul
-- Module: Mathlib.Algebra.Algebra.Operations
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)

Tactic:
sum_mem fun u u_in ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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)
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)
⊢ ∑ x ∈ c.support, HSMul.hSMul (β := M) x (↑((c : (a : R) → ↥N) x) : M) ∈
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)

Tactic:
refine sum_mem fun u u_in ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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
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)
⊢ HSMul.hSMul (β := M) u (↑((c : (a : R) → ↥N) 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)

Premises used: Iff.mpr, Finset.mem_coe, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
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)
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)
⊢ 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:
rw [algebraMap_smul]

Premises used: algebraMap_smul
-- Module: Mathlib.Algebra.Algebra.Operations
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 (β := M) u (↑((c : (a : R) → ↥N) ((algebraMap S R : (a : S) → R) u)) : M) ∈
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)

Tactic:
mem_set_smul_of_mem_mem u_in' (coe_mem (c ((algebraMap S R) u)))

Premises used: Algebra.algebraMap, Submodule.coe_mem, Submodule.mem_set_smul_of_mem_mem, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Operations
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 (β := M) u (↑((c : (a : R) → ↥N) ((algebraMap S R : (a : S) → R) u)) : M) ∈
    HSMul.hSMul (β := Submodule S M) s (restrictScalars S N)

Tactic:
exact mem_set_smul_of_mem_mem u_in' (coe_mem (c ((algebraMap S R) u)))

Premises used: Algebra.algebraMap, Submodule.coe_mem, Submodule.mem_set_smul_of_mem_mem, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Operations
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
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
⊢ 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:
rw [restrictScalars_mem, ← algebraMap_smul R r]

Premises used: algebraMap_smul, Submodule.restrictScalars_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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
⊢ 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:
mem_set_smul_of_mem_mem (Set.mem_image_of_mem _ r_in) x_in

Premises used: Submodule.mem_set_smul_of_mem_mem, Set.mem_image_of_mem
-- Module: Mathlib.Algebra.Algebra.Operations
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
⊢ 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:
exact mem_set_smul_of_mem_mem (Set.mem_image_of_mem _ r_in) x_in

Premises used: Submodule.mem_set_smul_of_mem_mem, Set.mem_image_of_mem
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : SMulCommClass R S A
inst_9 : IsScalarTower R S A
r : R
x : A
⊢ HMul.hMul (α := Aᵐᵒᵖ)
      (((RingHom.toOpposite (algebraMap R A) ⋯ : RingHom.{u_1, u_3} R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) r : Aᵐᵒᵖ) (op x) =
    HMul.hMul (β := Aᵐᵒᵖ) (op x)
      (((RingHom.toOpposite (algebraMap R A) ⋯ : RingHom.{u_1, u_3} R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) r : Aᵐᵒᵖ)

Tactic:
simp only [RingHom.toOpposite_apply, Function.comp_apply, ← op_mul, Algebra.commutes]

Premises used: RingHom.toOpposite_apply, MulOpposite.op_mul, Function.comp_apply, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : SMulCommClass R S A
inst_9 : IsScalarTower R S A
c : R
x : Aᵐᵒᵖ
⊢ unop (c • x) =
    unop
      (HMul.hMul (α := Aᵐᵒᵖ)
        (((RingHom.toOpposite (algebraMap R A) ⋯ : RingHom.{u_1, u_3} R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) c : Aᵐᵒᵖ) x)

Tactic:
simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul,
      Algebra.smul_def, Algebra.commutes, unop_op]

Premises used: RingHom.toOpposite_apply, MulOpposite.unop_smul, MulOpposite.unop_mul, MulOpposite.unop_op, Algebra.smul_def, Function.comp_apply, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
c : R
⊢ Eq.{u_3 + 1} (α := Aᵐᵒᵖ) ((algebraMap R Aᵐᵒᵖ : (a : R) → Aᵐᵒᵖ) c : Aᵐᵒᵖ)
    (op ((algebraMap R A : (a : R) → A) c) : Aᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl, MulOpposite.op