awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (hypothesis)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx : x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
hy : hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
hx₁ : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
⊢ x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
have hy₁ : hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
Tactic: push _ ∈ _ at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hy : hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
⊢ x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
have a : ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
  (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
  (hy : Membership.mem (γ := Submonoid M) (closure s) 1)
  (hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1),
  HMul.hMul (α := M) 1 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
Tactic: obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
Cleared hypotheses: x, hx_1, y, hy_1, hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hy : hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
a :
  ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
    (hy : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1),
    HMul.hMul (α := M) 1 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
⊢ x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
have a₁ : ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
  (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
  (hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1),
  1 * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
Tactic: obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
Cleared hypotheses: x, y, hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hy : hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
a :
  ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
    (hy : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1),
    HMul.hMul (α := M) 1 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₁ :
  ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
    (hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1),
    1 * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
⊢ x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
have a₂ : ∀ (hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x)
  (hy : Membership.mem (γ := Submonoid M) (closure s) 1)
  (hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1),
  x * 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
Tactic: obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
Cleared hypotheses: hx_1, hy_1, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hy : hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
a :
  ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
    (hy : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1),
    HMul.hMul (α := M) 1 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₁ :
  ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
    (hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1),
    1 * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₂ :
  ∀ (hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1),
    x * 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
⊢ x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
have a₃ : ∀ (hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x)
  (hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1),
  x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
Tactic: obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : x ∈ (↑(closure s) : Set M)
⊢ x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
have a : ∀ (x : M) (hx : x ∈ s), x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
Tactic: induction hx using closure_induction with
    | mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | one => exact Or.inl <| by simp
    | mul x hx y hy hx hy =>
      push _ ∈ _ at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all [mul_mem]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : x ∈ (↑(closure s) : Set M)
a : ∀ (x : M) (hx : x ∈ s), x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
⊢ x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
have a₁ : 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
Tactic: induction hx using closure_induction with
    | mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | one => exact Or.inl <| by simp
    | mul x hx y hy hx hy =>
      push _ ∈ _ at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all [mul_mem]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : x ∈ (↑(closure s) : Set M)
a : ∀ (x : M) (hx : x ∈ s), x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₁ : 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
⊢ x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
have a₂ : ∀ (x hx : M) (y : Membership.mem (γ := Submonoid M) (closure s) x)
  (hy : Membership.mem (γ := Submonoid M) (closure s) hx) (hx_1 : x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M))
  (hy : hx ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)), x * hx ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
Tactic: induction hx using closure_induction with
    | mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | one => exact Or.inl <| by simp
    | mul x hx y hy hx hy =>
      push _ ∈ _ at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all [mul_mem]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
N N' : Submonoid M
⊢ N ⊔ N' = closure ((↑N : Set M) ∪ (↑N' : Set M))
have simp_rw : N ⊔ N' = closure (↑N : Set M) ⊔ closure (↑N' : Set M)
Tactic: simp_rw [closure_union, closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
m : M
p : Submonoid M
⊢ closure {m} ≤ p ↔ m ∈ p
have rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
Tactic: rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
m : M
p : Submonoid M
rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
⊢ closure {m} ≤ p ↔ m ∈ p
have rw₁ : m ∈ (↑p : Set M) ↔ m ∈ p
Tactic: rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
m : M
p : Submonoid M
rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
rw₁ : m ∈ (↑p : Set M) ↔ m ∈ p
⊢ closure {m} ≤ p ↔ m ∈ p
have rw₂ : m ∈ p ↔ m ∈ p
Tactic: rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
⊢ Eq (α := Submonoid M) (closure (insert 1 s)) (closure s)
have rw : Membership.mem (γ := Submonoid M) (closure s) 1
Tactic: rw [insert_eq, closure_union, sup_eq_right, closure_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), p i) m ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
have rw : (∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
Tactic: rw [← closure_singleton_le_iff_mem, le_iSup_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
⊢ Eq.{u_1 + 1} (α := Submonoid M) (⨆ (i : ι), p i) (closure (⋃ (i : ι), (↑(p i) : Set M)))
have simp_rw : Eq.{u_1 + 1} (α := Submonoid M) (⨆ (i : ι), p i) (⨆ (i : ι), closure (↑(p i) : Set M))
Tactic: simp_rw [Submonoid.closure_iUnion, Submonoid.closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
have simp_rw : p₁ ⊓ p₂ ≤ ⊥ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
Tactic: simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
p₁ p₂ : Submonoid M
simp_rw : p₁ ⊓ p₂ ≤ ⊥ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
have simp_rw₁ : (∀ ⦃x : M⦄, x ∈ p₁ ⊓ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
Tactic: simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
p₁ p₂ : Submonoid M
simp_rw : p₁ ⊓ p₂ ≤ ⊥ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
simp_rw₁ : (∀ ⦃x : M⦄, x ∈ p₁ ⊓ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
have simp_rw₂ : (∀ ⦃x : M⦄, x ∈ p₁ ∧ x ∈ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
Tactic: simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
p₁ p₂ : Submonoid M
simp_rw : p₁ ⊓ p₂ ≤ ⊥ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
simp_rw₁ : (∀ ⦃x : M⦄, x ∈ p₁ ⊓ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
simp_rw₂ : (∀ ⦃x : M⦄, x ∈ p₁ ∧ x ∈ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
have simp_rw₃ : (∀ ⦃x : M⦄, x ∈ p₁ → x ∈ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
Tactic: simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
⊢ Eq (α := Submonoid M) (closure (s \ t)) (closure s)
have refine : ∀ (x : M) (hxs : x ∈ s), x ∈ (↑(closure (s \ t)) : Set M)
Tactic: refine (closure_mono Set.diff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
⊢ x ∈ (↑(closure (s \ t)) : Set M)
have pos : ∀ (hxt : x ∈ t), x ∈ (↑(closure (s \ t)) : Set M)
Tactic: by_cases hxt : x ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
pos : ∀ (hxt : x ∈ t), x ∈ (↑(closure (s \ t)) : Set M)
⊢ x ∈ (↑(closure (s \ t)) : Set M)
have neg : ∀ (hxt : x ∉ t), x ∈ (↑(closure (s \ t)) : Set M)
Tactic: by_cases hxt : x ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ (↑(closure (s \ t)) : Set M)
have neg : ∀ (S : Submonoid M), s \ t ⊆ (↑S : Set M) → x ∈ S
Tactic: rw [SetLike.mem_coe, Submonoid.mem_closure]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (hypothesis)
Goal:
M_1 : Type u_1
N : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N
s : Set M_1
M : Type u_4
inst_2 : Monoid M
a b : M
ha : Membership.mem (γ := Set M) (setOf IsUnit) a
hb : Membership.mem (γ := Set M) (setOf IsUnit) b
⊢ Membership.mem (γ := Set M) (setOf IsUnit) (a * b)
have ha₁ : IsUnit a
Tactic: rw [Set.mem_setOf_eq] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (hypothesis)
Goal:
M_1 : Type u_1
N : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N
s : Set M_1
M : Type u_4
inst_2 : Monoid M
a b : M
ha : Membership.mem (γ := Set M) (setOf IsUnit) a
hb : Membership.mem (γ := Set M) (setOf IsUnit) b
ha₁ : IsUnit a
⊢ Membership.mem (γ := Set M) (setOf IsUnit) (a * b)
have hb₁ : IsUnit b
Tactic: rw [Set.mem_setOf_eq] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
a : M
⊢ Membership.mem (γ := Set M) (setOf IsUnit) a ↔ IsUnit a
have rw : IsUnit a ↔ IsUnit a
Tactic: rw [Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f (1 * y) = f 1 * f y
have rw : f y = f 1 * f y
Tactic: rw [one_mul, h1, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
rw : f y = f 1 * f y
⊢ f (1 * y) = f 1 * f y
have rw₁ : f y = 1 * f y
Tactic: rw [one_mul, h1, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
rw : f y = f 1 * f y
rw₁ : f y = 1 * f y
⊢ f (1 * y) = f 1 * f y
have rw₂ : f y = f y
Tactic: rw [one_mul, h1, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f (a * b * y) = f (a * b) * f y
have rw : f (a * (b * y)) = f (a * b) * f y
Tactic: rw [mul_assoc, ha, ha, hb, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
rw : f (a * (b * y)) = f (a * b) * f y
⊢ f (a * b * y) = f (a * b) * f y
have rw₁ : f a * f (b * y) = f (a * b) * f y
Tactic: rw [mul_assoc, ha, ha, hb, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
rw : f (a * (b * y)) = f (a * b) * f y
rw₁ : f a * f (b * y) = f (a * b) * f y
⊢ f (a * b * y) = f (a * b) * f y
have rw₂ : f a * f (b * y) = f a * f b * f y
Tactic: rw [mul_assoc, ha, ha, hb, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
rw : f (a * (b * y)) = f (a * b) * f y
rw₁ : f a * f (b * y) = f (a * b) * f y
rw₂ : f a * f (b * y) = f a * f b * f y
⊢ f (a * b * y) = f (a * b) * f y
have rw₃ : f a * (f b * f y) = f a * f b * f y
Tactic: rw [mul_assoc, ha, ha, hb, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Basic (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
rw : f (a * (b * y)) = f (a * b) * f y
rw₁ : f a * f (b * y) = f (a * b) * f y
rw₂ : f a * f (b * y) = f a * f b * f y
rw₃ : f a * (f b * f y) = f a * f b * f y
⊢ f (a * b * y) = f (a * b) * f y
have rw₄ : f a * (f b * f y) = f a * (f b * f y)
Tactic: rw [mul_assoc, ha, ha, hb, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
B : Type u_3
inst : Monoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
S : B
l : List M
hl : ∀ x ∈ l, x ∈ S
⊢ l.prod ∈ S
have lift : ∀ (l : List ↥S), (List.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) l).prod ∈ S
Tactic: lift l to List S using hl
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
B : Type u_3
inst : Monoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
S : B
l : List ↥S
⊢ (List.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) l).prod ∈ S
have rw : (↑l.prod : M) ∈ S
Tactic: rw [← coe_list_prod]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
m : Multiset M
hm : ∀ a ∈ m, a ∈ S
⊢ m.prod ∈ S
have lift : ∀ (m : Multiset ↥S), (Multiset.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) m).prod ∈ S
Tactic: lift m to Multiset S using hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
m : Multiset ↥S
⊢ (Multiset.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) m).prod ∈ S
have rw : (↑m.prod : M) ∈ S
Tactic: rw [← coe_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
m : Multiset M
comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ m} Commute
h : ∀ x ∈ m, x ∈ S
⊢ m.noncommProd comm ∈ S
have h₁ : ∀ (l : List M) (comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ ⟦l⟧} Commute) (h : ∀ x ∈ ⟦l⟧, x ∈ S),
  Multiset.noncommProd ⟦l⟧ comm ∈ S
Tactic: induction m using Quotient.inductionOn with | h l => ?_
Cleared hypotheses: m, comm, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
l : List M
comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ ⟦l⟧} Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ Multiset.noncommProd ⟦l⟧ comm ∈ S
have h₁ : l.prod ∈ S
Tactic: simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t : Set ι).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
⊢ t.noncommProd f comm ∈ S
have h₁ : ∀ x ∈ Multiset.map f t.val, x ∈ S
Tactic: apply multiset_noncommProd_mem
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t : Set ι).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ y ∈ Multiset.map f t.val → y ∈ S
have h₁ : (∃ a ∈ t.val, f a = y) → y ∈ S
Tactic: rw [Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x_1 : M
s : Set M
x y : M
hx_1 : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) y
hx : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
hy : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = y
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x * y
have mul : ∀ (f : M → ℕ) (t : Finset M) (hts : (↑t : Set M) ⊆ s) (hf : Function.support f ⊆ (↑t : Set M)),
  Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a) →
    ∃ (f_1 : M → ℕ) (t_1 : Finset M),
      (↑t_1 : Set M) ⊆ s ∧ Function.support f_1 ⊆ (↑t_1 : Set M) ∧ ∏ a ∈ t_1, a ^ f_1 a = (∏ a ∈ t, a ^ f a) * y
Tactic: obtain ⟨f, t, hts, hf, rfl⟩ := hx
Cleared hypotheses: x, hx_1, hx