awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ Eq.{u_3 + 1} (α := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ (b : r ∈ s), ∀ a ∈ N, r • a ∈ p}
    {x : Submodule R M | ∀ (i : S) (i_1 : i ∈ s), i • N ≤ x}

Tactic:
Set.ext fun _ => forall₂_congr (fun _ _ => Iff.symm map_le_iff_le_comap)

Premises used: Set.ext, forall₂_congr, Submodule.map_le_iff_le_comap, Iff.symm
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ Eq.{u_3 + 1} (α := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ (b : r ∈ s), ∀ a ∈ N, r • a ∈ p}
    {x : Submodule R M | ∀ (i : S) (i_1 : i ∈ s), i • N ≤ x}

Tactic:
exact Set.ext fun _ => forall₂_congr (fun _ _ => Iff.symm map_le_iff_le_comap)

Premises used: Set.ext, forall₂_congr, Submodule.map_le_iff_le_comap, Iff.symm
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
N : Submodule R M
motive : (x : M) → x ∈ s • N → Prop
x : M
hx : x ∈ s • N
smul₀ : ∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N), motive (r • n) ⋯
smul₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) ⋯
add : ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N), motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) ⋯
zero : motive 0 ⋯
⊢ motive x hx

Tactic:
let ⟨_, h⟩ := set_smul_le s N
    { carrier := { m | ∃ (mem : m ∈ s • N), motive m mem },
      zero_mem' := ⟨Submodule.zero_mem _, zero⟩
      add_mem' := fun ⟨mem, h⟩ ⟨mem', h'⟩ ↦ ⟨_, add mem mem' h h'⟩
      smul_mem' := fun r _ ⟨mem, h⟩ ↦ ⟨_, smul₁ r mem h⟩ }
    (fun _ _ mem mem' ↦ ⟨mem_set_smul_of_mem_mem mem mem', smul₀ mem mem'⟩) hx
  h

Premises used: setOf, _private.0.Submodule.set_smul_inductionOn.match_1, Membership.mem, Exists, Submodule.mem_set_smul_of_mem_mem, AddSubmonoid.mk, AddSubsemigroup.mk, HAdd.hAdd, Submodule.zero_mem, Exists.intro, HSMul.hSMul, Submodule.mk, Submodule.set_smul_le, _private.0.Submodule.set_smul_inductionOn.match_2, Submodule.smul_mem, Submodule.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
h : ∀ (x : M), x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N ↔ Membership.mem (γ := Submodule R M) ⊥ x
⊢ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N = ⊥

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
x : M
h : x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N → Membership.mem (γ := Submodule R M) ⊥ x
h₁ : Membership.mem (γ := Submodule R M) ⊥ x → x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N
⊢ x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N ↔ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
fconstructor
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
x : M
hx : x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N
⊢ ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, Membership.mem (γ := Set S) ∅ r → n ∈ N → r • n ∈ p} p →
      x ∈ p

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf] at hx

Premises used: Submodule.mem_set_smul_def, Submodule.mem_sInf
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
x : M
hx :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, Membership.mem (γ := Set S) ∅ r → n ∈ N → r • n ∈ p} p →
      x ∈ p
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
hx ⊥ (fun r _ hr ↦ hr.elim)

Premises used: False.elim, Bot.bot
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
x : M
hx :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, Membership.mem (γ := Set S) ∅ r → n ∈ N → r • n ∈ p} p →
      x ∈ p
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
exact hx ⊥ (fun r _ hr ↦ hr.elim)

Premises used: False.elim, Bot.bot
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
⊢ 0 ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N

Tactic:
Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
⊢ 0 ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) s ⊥
smul₀ :
  ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → Membership.mem (γ := Submodule R M) ⊥ n → Membership.mem (γ := Submodule R M) ⊥ (r • n)
smul₁ :
  ∀ (r : R) ⦃m : M⦄,
    m ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
      Membership.mem (γ := Submodule R M) ⊥ m → Membership.mem (γ := Submodule R M) ⊥ (r • m)
add :
  ∀ ⦃m₁ m₂ : M⦄,
    m₁ ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
      m₂ ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
        Membership.mem (γ := Submodule R M) ⊥ m₁ →
          Membership.mem (γ := Submodule R M) ⊥ m₂ → Membership.mem (γ := Submodule R M) ⊥ (m₁ + m₂)
zero : Membership.mem (γ := Submodule R M) ⊥ 0
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
induction x, hx using set_smul_inductionOn
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x : M
r : S
n : M
mem₁ : r ∈ s
mem₂ : Membership.mem (γ := Submodule R M) ⊥ n
⊢ Membership.mem (γ := Submodule R M) ⊥ (r • n)

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x : M
r : R
m : M
mem : m ∈ HSMul.hSMul (β := Submodule R M) s ⊥
h : Membership.mem (γ := Submodule R M) ⊥ m
⊢ Membership.mem (γ := Submodule R M) ⊥ (r • m)

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x m₁ m₂ : M
mem₁ : m₁ ∈ HSMul.hSMul (β := Submodule R M) s ⊥
mem₂ : m₂ ∈ HSMul.hSMul (β := Submodule R M) s ⊥
h : Membership.mem (γ := Submodule R M) ⊥ m₁
h_1 : Membership.mem (γ := Submodule R M) ⊥ m₂
⊢ Membership.mem (γ := Submodule R M) ⊥ (m₁ + m₂)

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x : M
⊢ Membership.mem (γ := Submodule R M) ⊥ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
closed_under_smul : ∀ ⦃r_1 : S⦄ ⦃n : M⦄, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → r_1 • n ∈ r • N
le : r • N ≤ HSMul.hSMul (α := Set S) {r} N
⊢ HSMul.hSMul (α := Set S) {r} N = r • N

Tactic:
apply set_smul_eq_of_le

Premises used: Submodule.set_smul_eq_of_le
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
m : M
hm : m ∈ N
⊢ r • m ∈ r • N

Tactic:
⟨m, hm, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
m : M
hm : m ∈ N
⊢ r • m ∈ r • N

Tactic:
exact ⟨m, hm, rfl⟩
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
m : M
hm : m ∈ (↑N : Set M)
le :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        {p : Submodule R M | ∀ ⦃r_1 : S⦄ {n : M}, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → r_1 • n ∈ p} p →
      Membership.mem (α := M) p ((DistribSMul.toLinearMap R M r : (a : M) → M) m : M)
⊢ Membership.mem (α := M) (HSMul.hSMul (α := Set S) {r} N) ((DistribSMul.toLinearMap R M r : (a : M) → M) m : M)

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf]

Premises used: Submodule.mem_set_smul_def, Submodule.mem_sInf
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
m : M
hm : m ∈ (↑N : Set M)
p : Submodule R M
hp :
  Membership.mem (γ := Set (Submodule R M))
    {p : Submodule R M | ∀ ⦃r_1 : S⦄ {n : M}, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → r_1 • n ∈ p} p
⊢ Membership.mem (α := M) p ((DistribSMul.toLinearMap R M r : (a : M) → M) m : M)

Tactic:
hp rfl hm

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
m : M
hm : m ∈ (↑N : Set M)
p : Submodule R M
hp :
  Membership.mem (γ := Set (Submodule R M))
    {p : Submodule R M | ∀ ⦃r_1 : S⦄ {n : M}, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → r_1 • n ∈ p} p
⊢ Membership.mem (α := M) p ((DistribSMul.toLinearMap R M r : (a : M) → M) m : M)

Tactic:
exact hp rfl hm

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
mp : x ∈ HSMul.hSMul (α := Set S) {r} N → ∃ m ∈ N, x = r • m
mpr : (∃ m ∈ N, x = r • m) → x ∈ HSMul.hSMul (α := Set S) {r} N
⊢ x ∈ HSMul.hSMul (α := Set S) {r} N ↔ ∃ m ∈ N, x = r • m

Tactic:
fconstructor
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
r_1 : S
n : M
mem₁ : Membership.mem (γ := Set S) {r} r_1
mem₂ : n ∈ N
⊢ ∃ m ∈ N, r_1 • n = r • m

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
t : R
n : M
mem : n ∈ HSMul.hSMul (α := Set S) {r} N
h : ∃ m ∈ N, n = r • m
mp : ∀ (n : M) (hn : n ∈ N) (mem : r • n ∈ HSMul.hSMul (α := Set S) {r} N), ∃ m ∈ N, t • r • n = r • m
⊢ ∃ m ∈ N, t • n = r • m

Tactic:
rcases h with ⟨n, hn, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
t : R
n : M
hn : n ∈ N
mem : r • n ∈ HSMul.hSMul (α := Set S) {r} N
⊢ t • n ∈ N

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
t : R
n : M
hn : n ∈ N
mem : r • n ∈ HSMul.hSMul (α := Set S) {r} N
⊢ ∃ m ∈ N, t • r • n = r • m

Tactic:
exact ⟨t • n, by aesop, smul_comm _ _ _⟩
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x m₁ m₂ : M
mem₁ : m₁ ∈ HSMul.hSMul (α := Set S) {r} N
mem₂ : m₂ ∈ HSMul.hSMul (α := Set S) {r} N
h₁ : ∃ m ∈ N, m₁ = r • m
h₂ : ∃ m ∈ N, m₂ = r • m
mp : ∀ (m₁ : M) (h₁ : m₁ ∈ N) (mem₁ : r • m₁ ∈ HSMul.hSMul (α := Set S) {r} N), ∃ m ∈ N, r • m₁ + m₂ = r • m
⊢ ∃ m ∈ N, m₁ + m₂ = r • m

Tactic:
rcases h₁ with ⟨m₁, h₁, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x m₂ : M
mem₂ : m₂ ∈ HSMul.hSMul (α := Set S) {r} N
h₂ : ∃ m ∈ N, m₂ = r • m
m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ HSMul.hSMul (α := Set S) {r} N
mp : ∀ (m₂ : M) (h₂ : m₂ ∈ N) (mem₂ : r • m₂ ∈ HSMul.hSMul (α := Set S) {r} N), ∃ m ∈ N, r • m₁ + r • m₂ = r • m
⊢ ∃ m ∈ N, r • m₁ + m₂ = r • m

Tactic:
rcases h₂ with ⟨m₂, h₂, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ HSMul.hSMul (α := Set S) {r} N
m₂ : M
h₂ : m₂ ∈ N
mem₂ : r • m₂ ∈ HSMul.hSMul (α := Set S) {r} N
⊢ r • m₁ + r • m₂ = r • (m₁ + m₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ HSMul.hSMul (α := Set S) {r} N
m₂ : M
h₂ : m₂ ∈ N
mem₂ : r • m₂ ∈ HSMul.hSMul (α := Set S) {r} N
⊢ ∃ m ∈ N, r • m₁ + r • m₂ = r • m

Tactic:
exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
⊢ 0 = HSMul.hSMul (β := M) r 0

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
⊢ ∃ m ∈ N, 0 = r • m

Tactic:
exact ⟨0, Submodule.zero_mem _, by simp⟩
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
hx : x ∈ HSMul.hSMul (α := Set S) {r} N
mp : ∀ ⦃r_1 : S⦄ ⦃n : M⦄, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → ∃ m ∈ N, r_1 • n = r • m
mp₁ : ∀ (t : R) ⦃n : M⦄ (mem : n ∈ HSMul.hSMul (α := Set S) {r} N) (h : ∃ m ∈ N, n = r • m), ∃ m ∈ N, t • n = r • m
mp₂ :
  ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ HSMul.hSMul (α := Set S) {r} N) (mem₂ : m₂ ∈ HSMul.hSMul (α := Set S) {r} N)
    (h₁ : ∃ m ∈ N, m₁ = r • m) (h₂ : ∃ m ∈ N, m₂ = r • m), ∃ m ∈ N, m₁ + m₂ = r • m
mp₃ : ∃ m ∈ N, 0 = r • m
⊢ ∃ m ∈ N, x = r • m

Tactic:
induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩

Premises used: Submodule.zero, Submodule.add, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
⊢ (∃ m ∈ N, x = r • m) → x ∈ HSMul.hSMul (α := Set S) {r} N

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ a • N
⊢ ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯

Tactic:
simp_all only [← Submodule.singleton_set_smul]

Premises used: Submodule.singleton_set_smul
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ a • N
smul₂ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
⊢ ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯

Tactic:
simp_all only [← Submodule.singleton_set_smul]

Premises used: Submodule.singleton_set_smul
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ a • N
smul₂ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
add₁ :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
⊢ p 0 ⋯

Tactic:
simp_all only [← Submodule.singleton_set_smul]

Premises used: Submodule.singleton_set_smul
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x_1 : M
hx_1 : x_1 ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
add :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ HSMul.hSMul (α := Set S) {a} N
⊢ x ∈ a • N

Tactic:
rwa [← Submodule.singleton_set_smul]

Premises used: Submodule.singleton_set_smul
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
add :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
let : p x hx
⊢ p x hx

Tactic:
let p' (x : M) (hx : x ∈ ({a} : Set S) • N) : Prop :=
    p x (by rwa [← Submodule.singleton_set_smul])
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
add :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) → Prop :=
  fun (x : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) ↦ p x ⋯
⊢ p x hx

Tactic:
Submodule.set_smul_inductionOn (motive := p') _ (N.singleton_set_smul a ▸ hx)
      (fun r n hr hn ↦ ?_) smul₁ add zero

Premises used: Submodule.set_smul_inductionOn
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
add :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) → Prop :=
  fun (x : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) ↦ p x ⋯
refine : ∀ (r : S) (n : M) (hr : Membership.mem (γ := Set S) {a} r) (hn : n ∈ N), p' (r • n) ⋯
⊢ p x hx

Tactic:
refine Submodule.set_smul_inductionOn (motive := p') _ (N.singleton_set_smul a ▸ hx)
      (fun r n hr hn ↦ ?_) smul₁ add zero

Premises used: Submodule.set_smul_inductionOn