awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : AddMonoidWithOne R
⊢ Eq.{u_2 + 1} (α := AddSubmonoid R) 1 (closure 1)

Tactic:
one_eq_closure

Premises used: AddSubmonoid.one_eq_closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N : AddSubmonoid A
m : R
n : A
hm : m ∈ M
hn : n ∈ N
⊢ (DistribSMul.toAddMonoidHom A (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) : (a : A) → A) n = m • n

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
⊢ M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P

Tactic:
⟨fun H _m hm _n hn => H <| smul_mem_smul hm hn, fun H =>
    iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩

Premises used: Iff.mpr, _private.0.AddSubmonoid.smul_le.match_1, AddSubmonoid.smul_mem_smul, LE.le, AddSubmonoid.map, Iff.intro, iSup_le, Subtype.val, DistribSMul.toAddMonoidHom, AddSubmonoid.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N : AddSubmonoid A
C : A → Prop
a : A
ha : a ∈ M • N
hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)
hadd : ∀ (x y : A), C x → C y → C (x + y)
⊢ 0 ∈ AddSubsemigroup.carrier { carrier := setOf C, add_mem' := ⋯ : AddSubsemigroup A }

Tactic:
simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)

Premises used: smul_zero, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
S : AddSubmonoid R
m : R
h : m ∈ S
n : A
hn : Membership.mem (γ := AddSubmonoid A) ⊥ n
⊢ n = 0

Tactic:
rw [AddSubmonoid.mem_bot] at hn ⊢

Premises used: AddSubmonoid.mem_bot
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
S : AddSubmonoid R
m : R
h : m ∈ S
n : A
hn : n = 0
rw : HSMul.hSMul (β := A) m 0 = 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := A) 0 0
⊢ m • n = 0

Tactic:
rw [hn, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M M' : AddSubmonoid R
N P : AddSubmonoid A
h : M ≤ M'
hnp : N ≤ P
⊢ M • N ≤ M' • P

Tactic:
smul_le.2 fun _m hm _n hn => smul_mem_smul (h hm) (hnp hn)

Premises used: Iff.mpr, AddSubmonoid.smul_mem_smul, AddSubmonoid.smul_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M M' : AddSubmonoid R
P : AddSubmonoid A
h : M ≤ M'
⊢ M • P ≤ M' • P

Tactic:
smul_le_smul h le_rfl

Premises used: le_rfl, AddSubmonoid.smul_le_smul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
h : N ≤ P
⊢ M • N ≤ M • P

Tactic:
smul_le_smul le_rfl h

Premises used: le_rfl, AddSubmonoid.smul_le_smul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N : AddSubmonoid A
⊢ (↑M : Set R) • (↑N : Set A) ⊆ (↑(M • N) : Set A)

Tactic:
smul_subset_iff.2 fun _i hi _j hj ↦ smul_mem_smul hi hj

Premises used: Iff.mpr, AddSubmonoid.smul_mem_smul, Set.smul_subset_iff
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ m • np ∈ M • N ⊔ M • P

Tactic:
closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)

Premises used: AddSubmonoid.closure_induction
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
refine_1 :
  ∀ (x : A) (h : x ∈ (↑N : Set A) ∪ (↑P : Set A)),
    (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
        m • x ∈ M • N ⊔ M • P)
      x ⋯
refine_2 : HSMul.hSMul (β := A) m 0 ∈ M • N ⊔ M • P
refine_3 :
  ∀ (x y : A) (hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x)
    (hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y),
    (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
          m • x ∈ M • N ⊔ M • P)
        x hx →
      (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          y hy →
        (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          (x + y) ⋯
⊢ m • np ∈ M • N ⊔ M • P

Tactic:
refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)

Premises used: AddSubmonoid.closure_induction
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x : A
hx : x ∈ (↑N : Set A)
⊢ m • x ∈ M • N ⊔ M • P

Tactic:
le_sup_left (a := M • N) (smul_mem_smul hm hx)

Premises used: AddSubmonoid.smul_mem_smul, le_sup_left
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x : A
hx : x ∈ (↑P : Set A)
⊢ m • x ∈ M • N ⊔ M • P

Tactic:
le_sup_right (a := M • N) (smul_mem_smul hm hx)

Premises used: AddSubmonoid.smul_mem_smul, le_sup_right
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x : A
hx : x ∈ (↑N : Set A)
⊢ m • x ∈ M • N ⊔ M • P

Tactic:
exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx),
        le_sup_right (a := M • N) (smul_mem_smul hm hx)]

Premises used: AddSubmonoid.smul_mem_smul, le_sup_left, le_sup_right
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
      m • x ∈ M • N ⊔ M • P)
    0 ⋯

Tactic:
apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x : A
refine_3 :
  ∀ (y : A) (hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x)
    (hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y),
    (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
          m • x ∈ M • N ⊔ M • P)
        x hx →
      (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          y hy →
        (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          (x + y) ⋯
⊢ ∀ (y : A) (hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x)
    (hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y),
    (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
          m • x ∈ M • N ⊔ M • P)
        x hx →
      (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          y hy →
        (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          (x + y) ⋯

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x y : A
refine_3 :
  ∀ (hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x)
    (hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y),
    (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
          m • x ∈ M • N ⊔ M • P)
        x hx →
      (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          y hy →
        (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          (x + y) ⋯
⊢ ∀ (hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x)
    (hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y),
    (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
          m • x ∈ M • N ⊔ M • P)
        x hx →
      (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          y hy →
        (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          (x + y) ⋯

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x y : A
hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x
refine_3 :
  ∀ (hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y),
    (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
          m • x ∈ M • N ⊔ M • P)
        x hx →
      (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          y hy →
        (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          (x + y) ⋯
⊢ ∀ (hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y),
    (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
          m • x ∈ M • N ⊔ M • P)
        x hx →
      (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          y hy →
        (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
            m • x ∈ M • N ⊔ M • P)
          (x + y) ⋯

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x y : A
hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x
hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y
h1 : m • x ∈ M • N ⊔ M • P
h2 : m • y ∈ M • N ⊔ M • P
refine_3 : m • x + m • y ∈ M • N ⊔ M • P
⊢ m • (x + y) ∈ M • N ⊔ M • P

Tactic:
rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x y : A
hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x
hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y
h1 : m • x ∈ M • N ⊔ M • P
h2 : m • y ∈ M • N ⊔ M • P
⊢ m • x + m • y ∈ M • N ⊔ M • P

Tactic:
add_mem h1 h2

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x y : A
hx : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x
hy : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) y
h1 : m • x ∈ M • N ⊔ M • P
h2 : m • y ∈ M • N ⊔ M • P
⊢ m • x + m • y ∈ M • N ⊔ M • P

Tactic:
exact add_mem h1 h2

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), S i) s
simp_rw : Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) 0
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (HSMul.hSMul (β := A) t 0)

Tactic:
simp_rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), S i) s
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) 0

Tactic:
apply zero_mem

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), S i) s
x y : A
simp_rw :
  Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • x) →
    Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • y) →
      Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • x + t • y)
⊢ (fun (x : A) ↦ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • x)) x →
    (fun (x : A) ↦ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • x)) y →
      (fun (x : A) ↦ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • x)) (x + y)

Tactic:
simp_rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
A : Type u_3
inst : AddMonoid R
inst_1 : AddMonoid A
inst_2 : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), S i) s
x y : A
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • x) →
    Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • y) →
      Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • x + t • y)

Tactic:
apply add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
m n : R
hm : m ∈ M
hn : n ∈ N
⊢ m * n ∈ M * N

Tactic:
smul_mem_smul hm hn

Premises used: AddSubmonoid.smul_mem_smul, Set.Mem, AddMonoidHom.mulLeft, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
⊢ M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P

Tactic:
smul_le

Premises used: Set.Mem, AddSubmonoid.smul_le, AddMonoidHom.mulLeft, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
C : R → Prop
r : R
hr : r ∈ M * N
hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)
ha : ∀ (x y : R), C x → C y → C (x + y)
⊢ C r

Tactic:
AddSubmonoid.smul_induction_on hr hm ha

Premises used: AddSubmonoid.smul_induction_on
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) ≤ closure (S * T)
a₁ : closure (S * T) ≤ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T)
⊢ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) = closure (S * T)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
⊢ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) ≤ closure (S * T)

Tactic:
mul_le.2 fun a ha b hb => ?_

Premises used: Iff.mpr, AddSubmonoid.mul_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a :
  ∀ (a : R) (ha : Membership.mem (γ := AddSubmonoid R) (closure S) a) (b : R)
    (hb : Membership.mem (γ := AddSubmonoid R) (closure T) b),
    Membership.mem (γ := AddSubmonoid R) (closure (S * T)) (a * b)
⊢ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) ≤ closure (S * T)

Tactic:
refine mul_le.2 fun a ha b hb => ?_

Premises used: Iff.mpr, AddSubmonoid.mul_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
a₁ : Membership.mem (γ := AddSubmonoid R) (comap (F := R →+ R) (AddMonoidHom.mulRight b) (closure (S * T))) a
⊢ Membership.mem (γ := AddSubmonoid R) (closure (S * T)) (a * b)

Tactic:
rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]

Premises used: AddMonoidHom.mulRight_apply, AddSubmonoid.mem_comap
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
⊢ Membership.mem (γ := AddSubmonoid R) (comap (F := R →+ R) (AddMonoidHom.mulRight b) (closure (S * T))) a

Tactic:
(closure_le.2 fun a' ha' => ?_) ha

Premises used: Iff.mpr, AddSubmonoid.closure_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
a₁ : ∀ (a' : R) (ha' : a' ∈ S), a' ∈ (↑(comap (F := R →+ R) (AddMonoidHom.mulRight b) (closure (S * T))) : Set R)
⊢ Membership.mem (γ := AddSubmonoid R) (comap (F := R →+ R) (AddMonoidHom.mulRight b) (closure (S * T))) a

Tactic:
refine (closure_le.2 fun a' ha' => ?_) ha

Premises used: Iff.mpr, AddSubmonoid.closure_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
a' : R
ha' : a' ∈ S
a₁ : Membership.mem (γ := AddSubmonoid R) (comap (F := R →+ R) (AddMonoidHom.mulLeft a') (closure (S * T))) b
⊢ a' ∈ (↑(comap (F := R →+ R) (AddMonoidHom.mulRight b) (closure (S * T))) : Set R)

Tactic:
change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')

Premises used: HMul.hMul, AddSubmonoid.comap, AddSubmonoid.closure, AddMonoidHom.mulLeft
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
a' : R
ha' : a' ∈ S
⊢ Membership.mem (γ := AddSubmonoid R) (comap (F := R →+ R) (AddMonoidHom.mulLeft a') (closure (S * T))) b

Tactic:
(closure_le.2 fun b' hb' => ?_) hb

Premises used: Iff.mpr, AddSubmonoid.closure_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
a' : R
ha' : a' ∈ S
a₁ : ∀ (b' : R) (hb' : b' ∈ T), b' ∈ (↑(comap (F := R →+ R) (AddMonoidHom.mulLeft a') (closure (S * T))) : Set R)
⊢ Membership.mem (γ := AddSubmonoid R) (comap (F := R →+ R) (AddMonoidHom.mulLeft a') (closure (S * T))) b

Tactic:
refine (closure_le.2 fun b' hb' => ?_) hb

Premises used: Iff.mpr, AddSubmonoid.closure_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
a₁ : Membership.mem (γ := AddSubmonoid R) (closure (S * T)) (a' * b')
⊢ b' ∈ (↑(comap (F := R →+ R) (AddMonoidHom.mulLeft a') (closure (S * T))) : Set R)

Tactic:
change a' * b' ∈ closure (S * T)

Premises used: HMul.hMul, AddSubmonoid.closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ Membership.mem (γ := AddSubmonoid R) (closure (S * T)) (a' * b')

Tactic:
subset_closure (Set.mul_mem_mul ha' hb')

Premises used: AddSubmonoid.subset_closure, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (closure S) a
b : R
hb : Membership.mem (γ := AddSubmonoid R) (closure T) b
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ Membership.mem (γ := AddSubmonoid R) (closure (S * T)) (a' * b')

Tactic:
exact subset_closure (Set.mul_mem_mul ha' hb')

Premises used: AddSubmonoid.subset_closure, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : S * T ⊆ (↑(HMul.hMul (α := AddSubmonoid R) (closure S) (closure T)) : Set R)
⊢ closure (S * T) ≤ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T)

Tactic:
rw [closure_le]

Premises used: AddSubmonoid.closure_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ S
b : R
hb : b ∈ T
⊢ (fun (x1 x2 : R) ↦ x1 * x2) a b ∈ (↑(HMul.hMul (α := AddSubmonoid R) (closure S) (closure T)) : Set R)

Tactic:
mul_mem_mul (subset_closure ha) (subset_closure hb)

Premises used: Set.Mem, AddSubmonoid.subset_closure, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ S
b : R
hb : b ∈ T
⊢ (fun (x1 x2 : R) ↦ x1 * x2) a b ∈ (↑(HMul.hMul (α := AddSubmonoid R) (closure S) (closure T)) : Set R)

Tactic:
exact mul_mem_mul (subset_closure ha) (subset_closure hb)

Premises used: AddSubmonoid.subset_closure, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
rw : M * N = HMul.hMul (α := AddSubmonoid R) (closure (↑M : Set R)) (closure (↑N : Set R))
rw₁ : M * N = M * closure (↑N : Set R)
rw₂ rw₃ : M * N = M * N
⊢ M * N = closure ((↑M : Set R) * (↑N : Set R))

Tactic:
rw [← closure_mul_closure, closure_eq, closure_eq]

Premises used: AddSubmonoid.closure_eq, AddSubmonoid.closure_mul_closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
⊢ S * ⊥ = ⊥

Tactic:
addSubmonoid_smul_bot S

Premises used: AddMonoidHom.mulLeft, AddSubmonoid.addSubmonoid_smul_bot, DistribSMul.toAddMonoidHom