awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
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))))
⊢ (↑(closure s) : Set M) = List.prod '' {l : List M | ∀ x ∈ l, x ∈ s}

Tactic:
rw [closure_eq_mrange, coe_mrange, ← Set.range_list_map_coe, ← Set.range_comp]

Premises used: MonoidHom.coe_mrange, Set.range_comp, Set.range_list_map_coe, Submonoid.closure_eq_mrange
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ 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:
congrArg _ (funext <| FreeMonoid.lift_apply _)

Premises used: FreeMonoid, congrArg, funext, FreeMonoid.lift_apply
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ 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:
exact congrArg _ (funext <| FreeMonoid.lift_apply _)

Premises used: congrArg, funext, FreeMonoid.lift_apply
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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
rwa₂ rwa₃ rwa₄ 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
⊢ ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx

Premises used: Set.mem_image, SetLike.mem_coe, Submonoid.closure_eq_image_prod
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_4
inst : CommMonoid M
s : Set M
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
obtain : ∀ (l : List M) (h1 : ∀ y ∈ l, y ∈ s) (h2 : l.prod = x), ∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x
⊢ ∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx

Premises used: Submonoid.exists_list_of_mem_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_4
inst : CommMonoid M
s : Set M
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
l : List M
h1 : ∀ y ∈ l, y ∈ s
h2 : l.prod = x
⊢ ∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
⟨l, h1, (Multiset.prod_coe l).trans h2⟩

Premises used: Multiset.ofList, And.intro, Exists.intro, Multiset.prod_coe, Eq.trans
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_4
inst : CommMonoid M
s : Set M
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
l : List M
h1 : ∀ y ∈ l, y ∈ s
h2 : l.prod = x
⊢ ∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
exact ⟨l, h1, (Multiset.prod_coe l).trans h2⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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
⊢ 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

Premises used: Submonoid.closure_eq_mrange
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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_1 : Membership.mem (γ := Submonoid M) (closure s) x
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
obtain :
  ∀ (l : FreeMonoid { x : M // x ∈ s })
    (h :
      Membership.mem (α := M) (γ := Submonoid M) (closure 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)
            l :
          M)),
    motive
      ((((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)
        l)
      h
⊢ motive x h_1

Tactic:
obtain ⟨l, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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) ⋯
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure 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)
        1 :
      M)
⊢ motive
    ((((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)
      1)
    h

Tactic:
one

Premises used: FreeMonoid.prodAux
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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) ⋯
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure 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)
        1 :
      M)
⊢ motive
    ((((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)
      1)
    h

Tactic:
exact one
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : { x : M // x ∈ s }
y : FreeMonoid { x : M // x ∈ s }
ih :
  ∀
    (h :
      Membership.mem (α := M) (γ := Submonoid M) (closure 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)
            y :
          M)),
    motive
      ((((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)
        y)
      h
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure 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)
        (FreeMonoid.of x * y) :
      M)
mul_of :
  motive
    (HMul.hMul (β := M) (↑x : 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) :
            (a : FreeMonoid { x : M // x ∈ s }) → M)
          y :
        M))
    ⋯
⊢ motive
    ((((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)
      (FreeMonoid.of x * y))
    h

Tactic:
simp only [map_mul, FreeMonoid.lift_eval_of]

Premises used: FreeMonoid.lift_eval_of, map_mul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : { x : M // x ∈ s }
y : FreeMonoid { x : M // x ∈ s }
ih :
  ∀
    (h :
      Membership.mem (α := M) (γ := Submonoid M) (closure 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)
            y :
          M)),
    motive
      ((((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)
        y)
      h
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure 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)
        (FreeMonoid.of x * y) :
      M)
⊢ motive
    (HMul.hMul (β := M) (↑x : 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) :
            (a : FreeMonoid { x : M // x ∈ s }) → M)
          y :
        M))
    ⋯

Tactic:
mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)

Premises used: FreeMonoid.lift, Subtype.prop, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : { x : M // x ∈ s }
y : FreeMonoid { x : M // x ∈ s }
ih :
  ∀
    (h :
      Membership.mem (α := M) (γ := Submonoid M) (closure 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)
            y :
          M)),
    motive
      ((((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)
        y)
      h
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure 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)
        (FreeMonoid.of x * y) :
      M)
mul_of :
  Membership.mem (α := M) (γ := Submonoid M) (closure 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)
        y :
      M)
⊢ motive
    (HMul.hMul (β := M) (↑x : 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) :
            (a : FreeMonoid { x : M // x ∈ s }) → M)
          y :
        M))
    ⋯

Tactic:
refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)

Premises used: FreeMonoid.lift, Subtype.prop, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : { x : M // x ∈ s }
y : FreeMonoid { x : M // x ∈ s }
ih :
  ∀
    (h :
      Membership.mem (α := M) (γ := Submonoid M) (closure 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)
            y :
          M)),
    motive
      ((((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)
        y)
      h
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure 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)
        (FreeMonoid.of x * y) :
      M)
⊢ Membership.mem (α := M) (γ := Submonoid M) (closure 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)
        y :
      M)

Tactic:
simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

Premises used: Submonoid.closure_eq_mrange, MonoidHom.mem_mrange, exists_apply_eq_apply
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
⊢ Membership.mem (γ := Submonoid M) (closure s) x

Tactic:
simp [hs]
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
have : ∀ (this : Membership.mem (γ := Submonoid M) (closure s) x), motive x
⊢ motive x

Tactic:
have : x ∈ closure s := by simp [hs]
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
⊢ motive 1

Tactic:
one
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
⊢ motive 1

Tactic:
exact one
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x_1 : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
x : M
hx : x ∈ s
y : M
hy : Membership.mem (γ := Submonoid M) (closure s) y
ih : motive y
⊢ motive (x * y)

Tactic:
mul_left x hx y ih
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x_1 : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
x : M
hx : x ∈ s
y : M
hy : Membership.mem (γ := Submonoid M) (closure s) y
ih : motive y
⊢ motive (x * y)

Tactic:
exact mul_left x hx y ih
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
this : Membership.mem (γ := Submonoid M) (closure s) x
one₁ : motive 1
mul_left₁ :
  ∀ (x : M) (hx : x ∈ s) (y : M), Membership.mem (γ := Submonoid M) (closure s) y → ∀ (ih : motive y), motive (x * y)
⊢ motive x

Tactic:
induction this using closure_induction_left with
  | one => exact one
  | mul_left x hx y _ ih => exact mul_left x hx y ih
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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_right :
  ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : Membership.mem (γ := Submonoid M) (closure s) x
m : Mᵐᵒᵖ
hm : Membership.mem (γ := Submonoid Mᵐᵒᵖ) (closure (MulOpposite.unop ⁻¹' s)) m
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hm : Membership.mem (γ := Submonoid Mᵐᵒᵖ) (Submonoid.op (closure s)) m),
    Membership.mem (γ := Submonoid M) (closure s) (MulOpposite.unop m)
⊢ Membership.mem (γ := Submonoid M) (closure s) (MulOpposite.unop m)

Tactic:
rwa [← op_closure] at hm

Premises used: Submonoid.op_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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_right :
  ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : Membership.mem (γ := Submonoid M) (closure s) x
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Submonoid Mᵐᵒᵖ) (Submonoid.op (closure s)) { unop' := x : PreOpposite M }
⊢ Membership.mem (γ := Submonoid Mᵐᵒᵖ) (closure (MulOpposite.unop ⁻¹' s)) { unop' := x : PreOpposite M }

Tactic:
rwa [← op_closure]

Premises used: Submonoid.op_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
⊢ Membership.mem (γ := Submonoid M) (closure s) x

Tactic:
simp [hs]
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
have : ∀ (this : Membership.mem (γ := Submonoid M) (closure s) x), motive x
⊢ motive x

Tactic:
have : x ∈ closure s := by simp [hs]
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
⊢ motive 1

Tactic:
one
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
⊢ motive 1

Tactic:
exact one
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x_1 : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
y : M
hy : y ∈ s
ih : motive x
⊢ motive (x * y)

Tactic:
mul_right x y hy ih
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x_1 : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
y : M
hy : y ∈ s
ih : motive x
⊢ motive (x * y)

Tactic:
exact mul_right x y hy ih
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
this : Membership.mem (γ := Submonoid M) (closure s) x
one₁ : motive 1
mul_right₁ :
  ∀ (x : M), Membership.mem (γ := Submonoid M) (closure s) x → ∀ (y : M) (hy : y ∈ s) (ih : motive x), motive (x * y)
⊢ motive x

Tactic:
induction this using closure_induction_right with
  | one => exact one
  | mul_right x _ y hy ih => exact mul_right x y hy ih
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a n_1 n : M
i : ℕ
simp : n_1 ^ i = n ↔ HPow.hPow (β := ℕ) n_1 ((Multiplicative.toAdd : (a : Multiplicative ℕ) → ℕ) i : ℕ) = n
⊢ (fun (x : ℕ) ↦ n_1 ^ x) i = n ↔
    (((powersHom M : (a : M) → Multiplicative ℕ →* M) n_1 : Multiplicative ℕ →* M) : (a : Multiplicative ℕ) → M) i = n

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a n_1 n : M
i : ℕ
⊢ n_1 ^ i = n ↔ HPow.hPow (β := ℕ) n_1 ((Multiplicative.toAdd : (a : Multiplicative ℕ) → ℕ) i : ℕ) = n

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
n : M
⊢ Membership.mem (γ := Submonoid M) (powers n) n

Tactic:
⟨1, pow_one _⟩

Premises used: Set.Mem, setOf, pow_one, Exists.intro, Set.range, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x : M
⊢ (↑(powers x) : Set M) = Set.range fun (n : ℕ) ↦ x ^ n

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x z : M
⊢ Membership.mem (γ := Submonoid M) (powers z) x ↔ ∃ (n : ℕ), z ^ n = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
n : M
h : ∀ (x : M), Membership.mem (γ := Submonoid M) (powers n) x ↔ Membership.mem (γ := Submonoid M) (closure {n}) x
⊢ Eq (α := Submonoid M) (powers n) (closure {n})

Tactic:
ext