awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i
simp_rw :
  closure
      (⋃ x ∈ (↑Finset.univ : Set ι),
        (↑(Finset.image (⇑(MonoidHom.mulSingle M x : M x →* (i : ι) → M i) : (a : M x) → (i : ι) → M i) (s x)) :
          Set ((i : ι) → M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₁ :
  closure
      (⋃ (x : ι),
        ⋃ (_ : Membership.mem (γ := Set ι) Set.univ x),
          (↑(Finset.image (⇑(MonoidHom.mulSingle M x : M x →* (i : ι) → M i) : (a : M x) → (i : ι) → M i) (s x)) :
            Set ((i : ι) → M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₂ :
  closure
      (⋃ (x : ι),
        (↑(Finset.image (⇑(MonoidHom.mulSingle M x : M x →* (i : ι) → M i) : (a : M x) → (i : ι) → M i) (s x)) :
          Set ((i : ι) → M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₃ :
  ⨆ (i : ι),
      closure
        (↑(Finset.image (⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (s i)) :
          Set ((i : ι) → M i)) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₄ :
  ⨆ (i : ι),
      closure
        ((⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) '' (↑(s i) : Set (M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₅ :
  ⨆ (i : ι),
      map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (closure (↑(s i) : Set (M i))) =
    Submonoid.pi (M := M) Set.univ P
⊢ closure
      (↑(Finset.biUnion Finset.univ fun (i : ι) ↦
            Finset.image (⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (s i)) :
        Set ((i : ι) → M i)) =
    Submonoid.pi (M := M) Set.univ P
have simp_rw₆ : ⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i) =
  Submonoid.pi (M := M) Set.univ P
Tactic: simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
have haveI : ∀ (this : Fintype ι), (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
Tactic: classical
  haveI := Fintype.ofFinite ι
  choose s hs using hP
  refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
  simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
have haveI₃ : ∀ (this : Fintype ι) (s : (i : ι) → Finset (M i)) (hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i),
  (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
Tactic: classical
  haveI := Fintype.ofFinite ι
  choose s hs using hP
  refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
  simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
haveI₃ :
  ∀ (this : Fintype ι) (s : (i : ι) → Finset (M i)) (hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i),
    (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
have haveI₄ : ∀ (this : Fintype ι) (s : (i : ι) → Finset (M i)) (hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i),
  closure
      (↑(Finset.biUnion Finset.univ fun (i : ι) ↦
            Finset.image (⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (s i)) :
        Set ((i : ι) → M i)) =
    Submonoid.pi (M := M) Set.univ P
Tactic: classical
  haveI := Fintype.ofFinite ι
  choose s hs using hP
  refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
  simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
⊢ FG M
have intro : ∀ (val : Fintype M), FG M
Tactic: cases nonempty_fintype M
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
val : Fintype M
⊢ Eq (α := Submonoid M) (Submonoid.closure (↑Finset.univ : Set M)) ⊤
have rw : Eq.{u_1 + 1} (α := Submonoid M) (Submonoid.closure Set.univ) ⊤
Tactic: rw [Finset.coe_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
h : P.FG
e : M →* M'
⊢ FG (Submonoid.map e P)
have obtain : ∀ (s : Finset M), FG (Submonoid.map e (closure (↑s : Set M)))
Tactic: obtain ⟨s, rfl⟩ := h
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
e : M →* M'
s : Finset M
⊢ Eq (α := Submonoid M') (closure (↑(Finset.image (⇑e : (a : M) → M') s) : Set M'))
    (Submonoid.map e (closure (↑s : Set M)))
have rw : Eq (α := Submonoid M') (closure ((⇑e : (a : M) → M') '' (↑s : Set M))) (Submonoid.map e (closure (↑s : Set M)))
Tactic: rw [Finset.coe_image, MonoidHom.map_mclosure]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
e : M →* M'
s : Finset M
rw : Eq (α := Submonoid M') (closure ((⇑e : (a : M) → M') '' (↑s : Set M))) (Submonoid.map e (closure (↑s : Set M)))
⊢ Eq (α := Submonoid M') (closure (↑(Finset.image (⇑e : (a : M) → M') s) : Set M'))
    (Submonoid.map e (closure (↑s : Set M)))
have rw₁ : Eq.{u_3 + 1} (α := Submonoid M') (closure ((⇑e : (a : M) → M') '' (↑s : Set M)))
  (closure ((⇑e : (a : M) → M') '' (↑s : Set M)))
Tactic: rw [Finset.coe_image, MonoidHom.map_mclosure]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
h : P.FG
e : M →* M'
⊢ FG (Submonoid.map e P)
have obtain : ∀ (s : Finset M), FG (Submonoid.map e (closure (↑s : Set M)))
Tactic: classical
    obtain ⟨s, rfl⟩ := h
    exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
h : FG (Submonoid.map e P)
⊢ P.FG
have obtain : ∀ (s : Finset M') (hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)), P.FG
Tactic: obtain ⟨s, hs⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
⊢ P.FG
have h : closure (↑(s.preimage (⇑e : (a : M) → M') sorry) : Set M) = P
Tactic: use s.preimage e he.injOn
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
⊢ closure (↑(s.preimage (⇑e : (a : M) → M') ⋯) : Set M) = P
have h : Eq (α := Submonoid M') (Submonoid.map e (closure (↑(s.preimage (⇑e : (a : M) → M') sorry) : Set M))) (Submonoid.map e P)
Tactic: apply Submonoid.map_injective_of_injective he
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
⊢ Eq (α := Submonoid M') (Submonoid.map e (closure (↑(s.preimage (⇑e : (a : M) → M') ⋯) : Set M))) (Submonoid.map e P)
have h : Eq (α := Submonoid M')
  (closure (Set.image.{u_1, u_3} (α := M) (⇑e : (a : M) → M') ((⇑e : (a : M) → M') ⁻¹' (↑s : Set M'))))
  (closure (↑s : Set M'))
Tactic: rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
⊢ Eq (α := Submonoid M')
    (closure (Set.image.{u_1, u_3} (α := M) (⇑e : (a : M) → M') ((⇑e : (a : M) → M') ⁻¹' (↑s : Set M'))))
    (closure (↑s : Set M'))
have h : Set.image.{u_1, u_3} (α := M) (⇑e : (a : M) → M') ((⇑e : (a : M) → M') ⁻¹' (↑s : Set M')) = (↑s : Set M')
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
⊢ Set.image.{u_1, u_3} (α := M) (⇑e : (a : M) → M') ((⇑e : (a : M) → M') ⁻¹' (↑s : Set M')) = (↑s : Set M')
have h : LE.le (α := Submonoid M') (Submonoid.map e P) (Submonoid.map e ⊤)
Tactic: rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
      MonoidHom.mrange_eq_map e]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
N : Submonoid M
| N.FG
have rw : Submonoid.FG (Submonoid.map N.subtype ⊤)
Tactic: rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
N : Submonoid M
⊢ FG.{u_1} ↥N ↔ N.FG
have conv_rhs : FG.{u_1} ↥N ↔ Submonoid.FG (Submonoid.map N.subtype ⊤)
Tactic: conv_rhs => rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ FG M'
have obtain : ∀ (s : Finset M) (hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤), FG M'
Tactic: obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
s : Finset M
hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤
⊢ FG M'
have h : Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤
Tactic: use s.image f
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
s : Finset M
hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤
⊢ Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤
have h : Eq.{u_3 + 1} (α := Submonoid M') (Submonoid.closure ((⇑f : (a : M) → M') '' (↑s : Set M))) ⊤
Tactic: rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
s : Finset M
hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤
h : Eq.{u_3 + 1} (α := Submonoid M') (Submonoid.closure ((⇑f : (a : M) → M') '' (↑s : Set M))) ⊤
⊢ Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤
have h₁ : Eq (α := Submonoid M') (Submonoid.map f (Submonoid.closure (↑s : Set M))) ⊤
Tactic: rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
s : Finset M
hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤
h : Eq.{u_3 + 1} (α := Submonoid M') (Submonoid.closure ((⇑f : (a : M) → M') '' (↑s : Set M))) ⊤
h₁ : Eq (α := Submonoid M') (Submonoid.map f (Submonoid.closure (↑s : Set M))) ⊤
⊢ Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤
have h₂ : Eq (α := Submonoid M') (Submonoid.map f ⊤) ⊤
Tactic: rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
s : Finset M
hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤
h : Eq.{u_3 + 1} (α := Submonoid M') (Submonoid.closure ((⇑f : (a : M) → M') '' (↑s : Set M))) ⊤
h₁ : Eq (α := Submonoid M') (Submonoid.map f (Submonoid.closure (↑s : Set M))) ⊤
h₂ : Eq (α := Submonoid M') (Submonoid.map f ⊤) ⊤
⊢ Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤
have h₃ : Eq (α := Submonoid M') (MonoidHom.mrange f) ⊤
Tactic: rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ FG M'
have obtain : ∀ (s : Finset M) (hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤), FG M'
Tactic: classical
    obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
    use s.image f
    rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
obtain : ∀ (s : Finset M) (hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤), FG M'
⊢ FG M'
have h : ∀ (s : Finset M) (hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤),
  Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤
Tactic: classical
    obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
    use s.image f
    rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
⊢ FG M ↔
    ∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid (↑S : Type u_1) →* M),
      Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
have refine_1 : FG M →
  ∀ (S : Finset M) (hS : Eq (α := Submonoid M) (Submonoid.closure (↑S : Set M)) ⊤),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := FreeMonoid (↑(↑S : Set M) : Type u_1)) (β := M)
      (⇑((FreeMonoid.lift : (a : (↑(↑S : Set M) : Type u_1) → M) → FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ (↑S : Set M))) :
            FreeMonoid (↑(↑S : Set M) : Type u_1) →* M) :
        (a : FreeMonoid (↑(↑S : Set M) : Type u_1)) → M)
Tactic: refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeMonoid.lift Subtype.val, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
refine_1 :
  FG M →
    ∀ (S : Finset M) (hS : Eq (α := Submonoid M) (Submonoid.closure (↑S : Set M)) ⊤),
      Function.Surjective.{u_1 + 1, u_1 + 1} (α := FreeMonoid (↑(↑S : Set M) : Type u_1)) (β := M)
        (⇑((FreeMonoid.lift : (a : (↑(↑S : Set M) : Type u_1) → M) → FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
                (Subtype.val (p := fun (x : M) ↦ x ∈ (↑S : Set M))) :
              FreeMonoid (↑(↑S : Set M) : Type u_1) →* M) :
          (a : FreeMonoid (↑(↑S : Set M) : Type u_1)) → M)
⊢ FG M ↔
    ∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid (↑S : Type u_1) →* M),
      Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
have refine_2 : (∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid (↑S : Type u_1) →* M),
    Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)) →
  FG M
Tactic: refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeMonoid.lift Subtype.val, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
h : FG M
S : Finset M
hS : Eq (α := Submonoid M) (Submonoid.closure (↑S : Set M)) ⊤
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := FreeMonoid (↑(↑S : Set M) : Type u_1)) (β := M)
    (⇑((FreeMonoid.lift : (a : (↑(↑S : Set M) : Type u_1) → M) → FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ (↑S : Set M))) :
          FreeMonoid (↑(↑S : Set M) : Type u_1) →* M) :
      (a : FreeMonoid (↑(↑S : Set M) : Type u_1)) → M)
have refine_1 : Eq (α := Submonoid M)
  (MonoidHom.mrange (F := FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
    ((FreeMonoid.lift : (a : (↑(↑S : Set M) : Type u_1) → M) → FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
        (Subtype.val (p := fun (x : M) ↦ x ∈ (↑S : Set M))) :
      FreeMonoid (↑(↑S : Set M) : Type u_1) →* M))
  ⊤
Tactic: rwa [← MonoidHom.mrange_eq_top, ← Submonoid.closure_eq_mrange]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Set M
hfin : Finite.{u_1 + 1} (↑S : Type u_1)
φ : FreeMonoid (↑S : Type u_1) →* M
hφ : Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
⊢ FG M
have refine_2 : Eq (α := Submonoid M)
  (Submonoid.closure
    (Set.image (α := FreeMonoid (↑S : Type u_1)) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M) (Set.range FreeMonoid.of)))
  ⊤
Tactic: refine fg_iff.mpr ⟨φ '' Set.range FreeMonoid.of, ?_, Set.toFinite _⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
⊢ FG M ↔
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
have mp : FG M →
  ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
    Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
mp :
  FG M →
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
⊢ FG M ↔
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
have mpr : (∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
    Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)) →
  FG M
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
⊢ FG M →
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
have mp : (∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid (↑S : Type u_1) →* M),
    Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)) →
  ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
    Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
Tactic: rw [fg_iff_exists_freeMonoid_hom_surjective]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Set M
hS : S.Finite
φ : FreeMonoid (↑S : Type u_1) →* M
hφ : Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
⊢ ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
    Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
have mp : ∀ (n : ℕ) (e : (↑S : Type u_1) ≃ Fin n),
  ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
    Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
Tactic: obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
s : Finset M
⊢ FG.{u_1} ↥(Submonoid.closure (↑s : Set M))
have refine : Eq (α := Submonoid ↥(Submonoid.closure (↑s : Set M)))
  (Submonoid.closure
    (↑(s.preimage
          (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (Submonoid.closure (↑s : Set M)) x)) sorry) :
      Set ↥(Submonoid.closure (↑s : Set M))))
  ⊤
Tactic: refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
s : Finset M
⊢ Eq (α := Submonoid ↥(Submonoid.closure (↑s : Set M)))
    (Submonoid.closure
      (↑(s.preimage
            (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (Submonoid.closure (↑s : Set M)) x)) ⋯) :
        Set ↥(Submonoid.closure (↑s : Set M))))
    ⊤
have rw : Eq (α := Submonoid ↥(Submonoid.closure (↑s : Set M)))
  (Submonoid.closure
    (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (Submonoid.closure (↑s : Set M)) x) ⁻¹'
      (↑s : Set M)))
  ⊤
Tactic: rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
s : Finset M
rw :
  Eq (α := Submonoid ↥(Submonoid.closure (↑s : Set M)))
    (Submonoid.closure
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (Submonoid.closure (↑s : Set M)) x) ⁻¹'
        (↑s : Set M)))
    ⊤
⊢ Eq (α := Submonoid ↥(Submonoid.closure (↑s : Set M)))
    (Submonoid.closure
      (↑(s.preimage
            (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (Submonoid.closure (↑s : Set M)) x)) ⋯) :
        Set ↥(Submonoid.closure (↑s : Set M))))
    ⊤
have rw₁ : Eq.{u_1 + 1} (α := Submonoid ↥(Submonoid.closure (↑s : Set M))) ⊤ ⊤
Tactic: rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
⊢ P.FG ↔ P.FG
have mp : P.FG → P.FG
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
mp : P.FG → P.FG
⊢ P.FG ↔ P.FG
have mpr : P.FG → P.FG
Tactic: constructor