awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Basic (goal)
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
hb : b ∈ S
mem : ∀ (r : R) (hr : r ∈ (↑S : Set R)), Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b)
zero : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (0 * b)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)
have add : ∀ (r s : R),
  Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) r →
    Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) s →
      ∀ (hr : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b))
        (hs : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (s * b)),
        Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) ((r + s) * b)
Tactic: induction ha using closure_induction with
  | mem r hr => exact mem_closure.mpr fun y hy => hy (mul_mem hr hb)
  | zero => simp only [zero_mul, zero_mem _]
  | add r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Basic (goal)
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
hb : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) b
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)
have mem : ∀ (r : R) (hr : r ∈ (↑S : Set R)), Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r)
Tactic: induction hb using closure_induction with
  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
  | zero => simp only [mul_zero, zero_mem _]
  | add r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Basic (goal)
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
hb : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) b
mem : ∀ (r : R) (hr : r ∈ (↑S : Set R)), Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)
have zero : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * 0)
Tactic: induction hb using closure_induction with
  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
  | zero => simp only [mul_zero, zero_mem _]
  | add r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Basic (goal)
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
hb : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) b
mem : ∀ (r : R) (hr : r ∈ (↑S : Set R)), Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r)
zero : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * 0)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)
have add : ∀ (r s : R),
  Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) r →
    Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) s →
      ∀ (hr : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r))
        (hs : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * s)),
        Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * (r + s))
Tactic: induction hb using closure_induction with
  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
  | zero => simp only [mul_zero, zero_mem _]
  | add r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : AddMonoidWithOne R
⊢ Eq (α := AddSubmonoid R) 1 (closure {1})
have rw : Eq (α := AddSubmonoid R) (AddMonoidHom.mrange (F := ℕ →+ R) (Nat.castAddMonoidHom R))
  (AddMonoidHom.mrange (F := ℕ →+ R) ((multiplesHom R : (a : R) → ℕ →+ R) 1))
Tactic: rw [closure_singleton_eq, one_eq_mrange]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : AddMonoidWithOne R
⊢ Eq (α := AddSubmonoid R) (AddMonoidHom.mrange (F := ℕ →+ R) (Nat.castAddMonoidHom R))
    (AddMonoidHom.mrange (F := ℕ →+ R) ((multiplesHom R : (a : R) → ℕ →+ R) 1))
have e_f : Eq (α := ℕ →+ R) (Nat.castAddMonoidHom R) ((multiplesHom R : (a : R) → ℕ →+ R) 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : AddMonoidWithOne R
⊢ Eq (α := ℕ →+ R) (Nat.castAddMonoidHom R) ((multiplesHom R : (a : R) → ℕ →+ R) 1)
have e_f : Eq (α := R) ((Nat.castAddMonoidHom R : (a : ℕ) → R) 1 : R) (((multiplesHom R : (a : R) → ℕ →+ R) 1 : (a : ℕ) → R) 1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (hypothesis)
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
⊢ Membership.mem (γ := AddSubmonoid A) ⊥ (m • n)
have hn₁ : n = 0
Tactic: rw [AddSubmonoid.mem_bot] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
⊢ m • n = 0
have rw : HSMul.hSMul (β := A) m 0 = 0
Tactic: rw [hn, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
⊢ m • n = 0
have rw₁ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [hn, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
have 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 sorry
Tactic: refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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 ⋯
⊢ m • np ∈ M • N ⊔ M • P
have refine_2 : (fun (x : A) (x_1 : Membership.mem (γ := AddSubmonoid A) (closure ((↑N : Set A) ∪ (↑P : Set A))) x) ↦
    m • x ∈ M • N ⊔ M • P)
  0 sorry
Tactic: refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
⊢ m • np ∈ M • N ⊔ M • P
have 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) sorry
Tactic: refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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 + y) ∈ M • N ⊔ M • P
have refine_3 : m • x + m • y ∈ M • N ⊔ M • P
Tactic: rw [smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
⊢ (fun (x : A) ↦ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) (t • x)) 0
have simp_rw : Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), T • S i) 0
Tactic: simp_rw [smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
⊢ (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)
have 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)
Tactic: simp_rw [smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
⊢ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) = closure (S * T)
have a : HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) ≤ closure (S * T)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
a : HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) ≤ closure (S * T)
⊢ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) = closure (S * T)
have a₁ : closure (S * T) ≤ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
⊢ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T) ≤ closure (S * T)
have 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)
Tactic: refine mul_le.2 fun a ha b hb => ?_
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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) (closure (S * T)) (a * b)
have a₁ : Membership.mem (γ := AddSubmonoid R) (comap (F := R →+ R) (AddMonoidHom.mulRight b) (closure (S * T))) a
Tactic: rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
have a₁ : ∀ (a' : R) (ha' : a' ∈ S), a' ∈ (↑(comap (F := R →+ R) (AddMonoidHom.mulRight b) (closure (S * T))) : Set R)
Tactic: refine (closure_le.2 fun a' ha' => ?_) ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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' ∈ (↑(comap (F := R →+ R) (AddMonoidHom.mulRight b) (closure (S * T))) : Set R)
have a₁ : Membership.mem (γ := AddSubmonoid R) (comap (F := R →+ R) (AddMonoidHom.mulLeft a') (closure (S * T))) b
Tactic: change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
have a₁ : ∀ (b' : R) (hb' : b' ∈ T), b' ∈ (↑(comap (F := R →+ R) (AddMonoidHom.mulLeft a') (closure (S * T))) : Set R)
Tactic: refine (closure_le.2 fun b' hb' => ?_) hb
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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
⊢ b' ∈ (↑(comap (F := R →+ R) (AddMonoidHom.mulLeft a') (closure (S * T))) : Set R)
have a₁ : Membership.mem (γ := AddSubmonoid R) (closure (S * T)) (a' * b')
Tactic: change a' * b' ∈ closure (S * T)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ HMul.hMul (α := AddSubmonoid R) (closure S) (closure T)
have a : S * T ⊆ (↑(HMul.hMul (α := AddSubmonoid R) (closure S) (closure T)) : Set R)
Tactic: rw [closure_le]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = closure ((↑M : Set R) * (↑N : Set R))
have rw : M * N = HMul.hMul (α := AddSubmonoid R) (closure (↑M : Set R)) (closure (↑N : Set R))
Tactic: rw [← closure_mul_closure, closure_eq, closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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))
⊢ M * N = closure ((↑M : Set R) * (↑N : Set R))
have rw₁ : M * N = M * closure (↑N : Set R)
Tactic: rw [← closure_mul_closure, closure_eq, closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
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)
⊢ M * N = closure ((↑M : Set R) * (↑N : Set R))
have rw₂ : M * N = M * N
Tactic: rw [← closure_mul_closure, closure_eq, closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : Membership.mem (γ := AddSubmonoid R) ⊥ m
n : R
h : n ∈ S
⊢ Membership.mem (γ := AddSubmonoid R) ⊥ (m * n)
have rw : ∀ (hm : m = 0), ∀ n ∈ S, m * n = 0
Tactic: rw [AddSubmonoid.mem_bot] at hm ⊢
Cleared hypotheses: hm, n, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
h : n ∈ S
⊢ m * n = 0
have rw : 0 * n = 0
Tactic: rw [hm, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
h : n ∈ S
rw : 0 * n = 0
⊢ m * n = 0
have rw₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [hm, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
mn : R
hmn : mn ∈ M ⊔ N
p : R
hp : p ∈ P
⊢ mn * p ∈ M * P ⊔ N * P
have obtain : ∀ (m : R) (hm : m ∈ M) (n : R) (hn : n ∈ N) (hmn : m + n ∈ M ⊔ N), (m + n) * p ∈ M * P ⊔ N * P
Tactic: obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
Cleared hypotheses: mn, hmn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ (m + n) * p ∈ M * P ⊔ N * P
have rw : m * p + n * p ∈ M * P ⊔ N * P
Tactic: rw [right_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i) s
t : R
ht : t ∈ T
⊢ (fun (x : R) ↦ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t)) 0
have simp_rw : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) 0
Tactic: simp_rw [zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i) s
t : R
ht : t ∈ T
x x_1 : R
⊢ (fun (x : R) ↦ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t)) x →
    (fun (x : R) ↦ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t)) x_1 →
      (fun (x : R) ↦ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t)) (x + x_1)
have simp_rw : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t) →
  Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x_1 * t) →
    Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t + x_1 * t)
Tactic: simp_rw [right_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
⊢ -x * y = -(x * y)
have refine_1 : ∀ (m : R) (hm : m ∈ -x) (n : R) (hn : n ∈ y), m * n ∈ -(x * y)
Tactic: refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
refine_1 : ∀ (m : R) (hm : m ∈ -x) (n : R) (hn : n ∈ y), m * n ∈ -(x * y)
⊢ -x * y = -(x * y)
have refine_2 : ∀ (m : R) (hm : m ∈ x) (n : R) (hn : n ∈ y), m * n ∈ -(-x * y)
Tactic: refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ -x
n : R
hn : n ∈ y
⊢ m * n ∈ -(x * y)
have refine_1 : ∀ (hm : -m ∈ x), -m * n ∈ x * y
Tactic: simp only [AddSubmonoid.mem_neg, ← neg_mul] at *
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * n ∈ -(-x * y)
have refine_2 : -m * n ∈ -x * y
Tactic: simp only [AddSubmonoid.mem_neg, ← neg_mul] at *
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
⊢ x * -y = -(x * y)
have refine_1 : ∀ (m : R) (hm : m ∈ x) (n : R) (hn : n ∈ -y), m * n ∈ -(x * y)
Tactic: refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
refine_1 : ∀ (m : R) (hm : m ∈ x) (n : R) (hn : n ∈ -y), m * n ∈ -(x * y)
⊢ x * -y = -(x * y)
have refine_2 : ∀ (m : R) (hm : m ∈ x) (n : R) (hn : n ∈ y), m * n ∈ -(x * -y)
Tactic: refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ -y
⊢ m * n ∈ -(x * y)
have refine_1 : ∀ (hn : -n ∈ y), m * -n ∈ x * y
Tactic: simp only [AddSubmonoid.mem_neg, ← mul_neg] at *
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * n ∈ -(x * -y)
have refine_2 : m * -n ∈ x * -y
Tactic: simp only [AddSubmonoid.mem_neg, ← mul_neg] at *
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M_1 : Type u_1
R : Type u_2
A : Type u_3
inst : NonAssocSemiring R
M : AddSubmonoid R
⊢ 1 * M = M
have rw : closure 1 * M = M
Tactic: rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M_1 : Type u_1
R : Type u_2
A : Type u_3
inst : NonAssocSemiring R
M : AddSubmonoid R
rw : closure 1 * M = M
⊢ 1 * M = M
have rw₁ : HMul.hMul (α := AddSubmonoid R) (closure 1) (closure (↑M : Set R)) = closure (↑M : Set R)
Tactic: rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M_1 : Type u_1
R : Type u_2
A : Type u_3
inst : NonAssocSemiring R
M : AddSubmonoid R
rw : closure 1 * M = M
rw₁ : HMul.hMul (α := AddSubmonoid R) (closure 1) (closure (↑M : Set R)) = closure (↑M : Set R)
⊢ 1 * M = M
have rw₂ : Eq (α := AddSubmonoid R) (closure (1 * (↑M : Set R))) (closure (↑M : Set R))
Tactic: rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M_1 : Type u_1
R : Type u_2
A : Type u_3
inst : NonAssocSemiring R
M : AddSubmonoid R
rw : closure 1 * M = M
rw₁ : HMul.hMul (α := AddSubmonoid R) (closure 1) (closure (↑M : Set R)) = closure (↑M : Set R)
rw₂ : Eq (α := AddSubmonoid R) (closure (1 * (↑M : Set R))) (closure (↑M : Set R))
⊢ 1 * M = M
have rw₃ : Eq (α := AddSubmonoid R) (closure (↑M : Set R)) (closure (↑M : Set R))
Tactic: rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M_1 : Type u_1
R : Type u_2
A : Type u_3
inst : NonAssocSemiring R
M : AddSubmonoid R
⊢ M * 1 = M
have rw : M * closure 1 = M
Tactic: rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Pointwise (goal)
Goal:
M_1 : Type u_1
R : Type u_2
A : Type u_3
inst : NonAssocSemiring R
M : AddSubmonoid R
rw : M * closure 1 = M
⊢ M * 1 = M
have rw₁ : HMul.hMul (α := AddSubmonoid R) (closure (↑M : Set R)) (closure 1) = closure (↑M : Set R)
Tactic: rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, mul_one]