awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
have refine : ∀ (hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x) (x y : M)
  (hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x)
  (hy : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y),
  (∃ (i : ι), x ∈ S i) → (∃ (i : ι), y ∈ S i) → ∃ (i : ι), x * y ∈ S i
Tactic: refine fun hx ↦ closure_induction (by simp) (by simp) ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x_1 : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
x y : M
hx_1 : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
hy : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ (i : ι), x * y ∈ S i
have obtain : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), ∃ (i : ι), x * y ∈ S i
Tactic: obtain ⟨k, hik, hjk⟩ := hS i j
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : ∃ (i : ι), p i
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i
have rw : ∀ (hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)) {S : ι → Submonoid M}
  (hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}) {x : M},
  Membership.mem (γ := Submonoid M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i
Tactic: rw [← nonempty_subtype] at hp
Cleared hypotheses: hp, S, hS, x
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i
have rw : (∃ (i : Subtype p), x ∈ S (↑i : ι)) ↔ ∃ (i : ι), p i ∧ x ∈ S i
Tactic: rw [iSup_subtype', mem_iSup_of_directed]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
rw : (∃ (i : Subtype p), x ∈ S (↑i : ι)) ↔ ∃ (i : ι), p i ∧ x ∈ S i
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i
have hS₁ : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) fun (x : Subtype p) ↦ S (↑x : ι)
Tactic: rw [iSup_subtype', mem_iSup_of_directed]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) fun (x : Subtype p) ↦ S (↑x : ι)
have hS₁ : Directed (ι := Subtype p) (S ⁻¹'o fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) (Subtype.val (p := p))
Tactic: rw [← Function.comp_def, directed_comp]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
⊢ Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
have pos : ∀ (h : p), Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
pos : ∀ (h : p), Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
⊢ Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
have neg : ∀ (h : ¬p), Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (hypothesis)
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
have this : Nonempty.{u_1 + 1} (↑S : Type u_1)
Tactic: haveI : Nonempty S := Sne.to_subtype
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u_1} ↥(⨆ (i : ι), S i)
have refine : ∀ (a : M),
  Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) a →
    ∀ (b : M), Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) b → a * b = b * a
Tactic: refine .of_setLike_mul_comm ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
⊢ ∀ (a : M),
    Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) a →
      ∀ (b : M), Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) b → a * b = b * a
have simp_rw : ∀ (a : M) (x : ι) (h : a ∈ S x) (b : M) (x : ι) (h : b ∈ S x), a * b = b * a
Tactic: simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
⊢ a * b = b * a
have obtain : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), a * b = b * a
Tactic: obtain ⟨k, hik, hjk⟩ := dir i j
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (hypothesis)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
⊢ motive x
have hx₁ : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
Tactic: rw [iSup_eq_closure] at hx
Cleared hypotheses: hx, mem, one, mul
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
⊢ motive x
have refine : ∀ (x : M) (hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x), motive x
Tactic: refine closure_induction (fun x hx => ?_) one (fun _ _ _ _ ↦ mul _ _) hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x_1 : M
hx_1 : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x
⊢ motive x
have obtain : ∀ (i : ι) (hi : x ∈ (↑(S i) : Set M)), motive x
Tactic: obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
⊢ motive x hx
have refine : ∃ (Hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x), motive x Hx
Tactic: refine Exists.elim (?_ : ∃ Hx, motive x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) => hc
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
⊢ ∃ (Hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x), motive x Hx
have refine_1 : ∀ (i : ι) (x : M) (hx : x ∈ S i),
  (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) x
Tactic: refine @iSup_induction _ _ ι S (fun m => ∃ hm, motive m hm) _ hx (fun i x hx => ?_) ?_
      fun x y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
refine_1 :
  ∀ (i : ι) (x : M) (hx : x ∈ S i),
    (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) x
⊢ ∃ (Hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x), motive x Hx
have refine_2 : (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) 1
Tactic: refine @iSup_induction _ _ ι S (fun m => ∃ hm, motive m hm) _ hx (fun i x hx => ?_) ?_
      fun x y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x
refine_1 :
  ∀ (i : ι) (x : M) (hx : x ∈ S i),
    (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) x
refine_2 : ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) 1), motive 1 hm
⊢ ∃ (Hx : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x), motive x Hx
have refine_3 : ∀ (x y : M),
  (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) x →
    (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) y →
      (fun (m : M) ↦ ∃ (hm : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) m), motive m hm) (x * y)
Tactic: refine @iSup_induction _ _ ι S (fun m => ∃ hm, motive m hm) _ hx (fun i x hx => ?_) ?_
      fun x y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
x y : M
⊢ Membership.mem (γ := Submonoid M) (closure {x}) y ↔ ∃ (n : ℕ), x ^ n = y
have rw : (∃ (x_1 : Multiplicative ℕ),
    (((powersHom M : (a : M) → Multiplicative ℕ →* M) x : Multiplicative ℕ →* M) : (a : Multiplicative ℕ) → M) x_1 =
      y) ↔
  ∃ (n : ℕ), x ^ n = y
Tactic: rw [closure_singleton_eq, mem_mrange]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
α : Type u_4
f : α → M
⊢ Eq (α := Submonoid M)
    (mrange (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M))
    (closure (Set.range f))
have rw : Eq (α := Submonoid M)
  (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
    ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) ⊤)
  (closure (Set.range f))
Tactic: rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
α : Type u_4
f : α → M
rw :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) ⊤)
    (closure (Set.range f))
⊢ Eq (α := Submonoid M)
    (mrange (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M))
    (closure (Set.range f))
have rw₁ : Eq (α := Submonoid M)
  (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
    ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M)
    (closure (Set.range FreeMonoid.of)))
  (closure (Set.range f))
Tactic: rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
α : Type u_4
f : α → M
rw :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) ⊤)
    (closure (Set.range f))
rw₁ :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      (closure (Set.range FreeMonoid.of)))
    (closure (Set.range f))
⊢ Eq (α := Submonoid M)
    (mrange (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M))
    (closure (Set.range f))
have rw₂ : Eq (α := Submonoid M)
  (closure
    (Set.image.{u_4, u_1} (α := FreeMonoid α)
      (⇑((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) :
        (a : FreeMonoid α) → M)
      (Set.range FreeMonoid.of)))
  (closure (Set.range f))
Tactic: rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
α : Type u_4
f : α → M
rw :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) ⊤)
    (closure (Set.range f))
rw₁ :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      (closure (Set.range FreeMonoid.of)))
    (closure (Set.range f))
rw₂ :
  Eq (α := Submonoid M)
    (closure
      (Set.image.{u_4, u_1} (α := FreeMonoid α)
        (⇑((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) :
          (a : FreeMonoid α) → M)
        (Set.range FreeMonoid.of)))
    (closure (Set.range f))
⊢ Eq (α := Submonoid M)
    (mrange (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M))
    (closure (Set.range f))
have rw₃ : Eq (α := Submonoid M)
  (closure
    (Set.range.{u_1, u_4 + 1} (ι := α)
      ((⇑((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) :
          (a : FreeMonoid α) → M) ∘
        FreeMonoid.of)))
  (closure (Set.range f))
Tactic: rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
α : Type u_4
f : α → M
rw :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) ⊤)
    (closure (Set.range f))
rw₁ :
  Eq (α := Submonoid M)
    (map (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      (closure (Set.range FreeMonoid.of)))
    (closure (Set.range f))
rw₂ :
  Eq (α := Submonoid M)
    (closure
      (Set.image.{u_4, u_1} (α := FreeMonoid α)
        (⇑((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) :
          (a : FreeMonoid α) → M)
        (Set.range FreeMonoid.of)))
    (closure (Set.range f))
rw₃ :
  Eq (α := Submonoid M)
    (closure
      (Set.range.{u_1, u_4 + 1} (ι := α)
        ((⇑((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M) :
            (a : FreeMonoid α) → M) ∘
          FreeMonoid.of)))
    (closure (Set.range f))
⊢ Eq (α := Submonoid M)
    (mrange (F := MonoidHom.{u_4, u_1} (FreeMonoid α) M)
      ((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_4, u_1} (FreeMonoid α) M))
    (closure (Set.range f))
have rw₄ : Eq (α := Submonoid M) (closure (Set.range f)) (closure (Set.range f))
Tactic: rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ Eq (α := Submonoid M) (closure s)
    (mrange (F := FreeMonoid { x : M // x ∈ s } →* M)
      ((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
          (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
        FreeMonoid { x : M // x ∈ s } →* M))
have rw : Eq (α := Submonoid M) (closure s)
  (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
Tactic: rw [FreeMonoid.mrange_lift, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
rw :
  Eq (α := Submonoid M) (closure s)
    (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
⊢ Eq (α := Submonoid M) (closure s)
    (mrange (F := FreeMonoid { x : M // x ∈ s } →* M)
      ((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
          (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
        FreeMonoid { x : M // x ∈ s } →* M))
have rw₁ : Eq (α := Submonoid M) (closure s) (closure s)
Tactic: rw [FreeMonoid.mrange_lift, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ (↑(closure s) : Set M) = List.prod '' {l : List M | ∀ x ∈ l, x ∈ s}
have rw : Eq.{u_1 + 1} (α := Set M)
  (Set.range (ι := FreeMonoid { x : M // x ∈ s })
    (⇑((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
          FreeMonoid { x : M // x ∈ s } →* M) :
      (a : FreeMonoid { x : M // x ∈ s }) → M))
  (Set.range (ι := List { x : M // x ∈ s }) (List.prod ∘ List.map (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
Tactic: rw [closure_eq_mrange, coe_mrange, ← Set.range_list_map_coe, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
⊢ ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
have rwa : ∀ (hx : x ∈ (↑(closure s) : Set M)), ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
Tactic: rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
rwa : ∀ (hx : x ∈ (↑(closure s) : Set M)), ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
⊢ ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
have rwa₁ : ∀ (hx : Membership.mem (γ := Set M) (List.prod '' {l : List M | ∀ x ∈ l, x ∈ s}) x),
  ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
Tactic: rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
rwa : ∀ (hx : x ∈ (↑(closure s) : Set M)), ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
rwa₁ :
  ∀ (hx : Membership.mem (γ := Set M) (List.prod '' {l : List M | ∀ x ∈ l, x ∈ s}) x),
    ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
⊢ ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
have rwa₂ : ∀ (hx : ∃ (x_1 : List M), Membership.mem (γ := Set (List M)) {l : List M | ∀ x ∈ l, x ∈ s} x_1 ∧ x_1.prod = x),
  ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
Tactic: rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_4
inst : CommMonoid M
s : Set M
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
⊢ ∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
have obtain : ∀ (l : List M) (h1 : ∀ y ∈ l, y ∈ s) (h2 : l.prod = x), ∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
Tactic: obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (hypothesis)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : (m : M) → Membership.mem (γ := Submonoid M) (closure s) m → Prop
one : motive 1 ⋯
mul_left :
  ∀ (x : M) (hx : x ∈ s) (y : M) (hy : Membership.mem (γ := Submonoid M) (closure s) y), motive y hy → motive (x * y) ⋯
x : M
h : Membership.mem (γ := Submonoid M) (closure s) x
⊢ motive x h
have h₁ : Membership.mem (γ := Submonoid M)
  (mrange (F := FreeMonoid { x : M // x ∈ s } →* M)
    ((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
        (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
      FreeMonoid { x : M // x ∈ s } →* M))
  x
Tactic: simp_rw [closure_eq_mrange] at h