awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H₁ H₂ : Subgroup G
simp_rw :
  (∀ ⦃x : MonoidHom.{u_1, u_2} G Mˣ⦄,
      (∀ x_1 ∈ H₂, Eq.{u_2 + 1} (α := Mˣ) ((x : (a : G) → Mˣ) x_1 : Mˣ) (1 : Mˣ)) →
        ∀ x_1 ∈ H₁, Eq.{u_2 + 1} (α := Mˣ) ((x : (a : G) → Mˣ) x_1 : Mˣ) (1 : Mˣ)) ↔
    ∀ ⦃x : G⦄, x ∈ H₁ → x ∈ H₂
⊢ LE.le (α := (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ)
      (({
              toFun := fun (H : Subgroup G) ↦
                (OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                  (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)),
              invFun := fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
                (MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
                  (ker (M :=
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)
                    (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                      (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                        ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                              Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                          Mˣ)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subgroup G) → (Subgroup (G →* Mˣ))ᵒᵈ)
          H₁ :
        (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ)
      (({
              toFun := fun (H : Subgroup G) ↦
                (OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                  (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)),
              invFun := fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
                (MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
                  (ker (M :=
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)
                    (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                      (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                        ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                              Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                          Mˣ)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subgroup G) → (Subgroup (G →* Mˣ))ᵒᵈ)
          H₂ :
        (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↔
    H₁ ≤ H₂

Tactic:
simp_rw [Equiv.coe_fn_mk, OrderDual.toDual_le_toDual,
      SetLike.le_def, mem_ker, restrictHom_apply, restrict_eq_one_iff]

Premises used: OrderDual.toDual_le_toDual, SetLike.le_def, MonoidHom.mem_ker, MonoidHom.restrict_eq_one_iff, MonoidHom.restrictHom_apply, Equiv.coe_fn_mk
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H₁ H₂ : Subgroup G
⊢ (∀ ⦃x : MonoidHom.{u_1, u_2} G Mˣ⦄,
      (∀ x_1 ∈ H₂, Eq.{u_2 + 1} (α := Mˣ) ((x : (a : G) → Mˣ) x_1 : Mˣ) (1 : Mˣ)) →
        ∀ x_1 ∈ H₁, Eq.{u_2 + 1} (α := Mˣ) ((x : (a : G) → Mˣ) x_1 : Mˣ) (1 : Mˣ)) ↔
    ∀ ⦃x : G⦄, x ∈ H₁ → x ∈ H₂

Tactic:
grind [forall_monoidHom_apply_eq_one_iff M H₂]

Premises used: CommGroup.forall_monoidHom_apply_eq_one_iff
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
φ : MonoidHom.{u_1, u_2} G Mˣ
⊢ Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
          ((subgroupOrderIsoSubgroupMonoidHom G M : (a : Subgroup G) → (Subgroup (G →* Mˣ))ᵒᵈ) H) :
        Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      φ ↔
    ∀ g ∈ H, Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) g : Mˣ) (1 : Mˣ)

Tactic:
simp [subgroupOrderIsoSubgroupMonoidHom]

Premises used: CommGroup.subgroupOrderIsoSubgroupMonoidHom
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
⊢ Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
            ((subgroupOrderIsoSubgroupMonoidHom G M : (a : Subgroup G) → (Subgroup (G →* Mˣ))ᵒᵈ) H) :
          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) =
    Nat.card.{u_1} (G ⧸ H)

Tactic:
card_restrictHom_ker _ _

Premises used: Set.Mem, CommGroup.card_restrictHom_ker
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
A B : FiniteIndexNormalSubgroup G
h :
  Eq.{u_1 + 1} (α := Subgroup G) ((fun (H : FiniteIndexNormalSubgroup G) ↦ H.toSubgroup) A)
    ((fun (H : FiniteIndexNormalSubgroup G) ↦ H.toSubgroup) B)
carrier : ∀ (x : G), x ∈ A.carrier ↔ x ∈ B.carrier
⊢ A = B

Tactic:
ext
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
A B : FiniteIndexNormalSubgroup G
h : A.toSubgroup = B.toSubgroup
x : G
carrier carrier₁ : x ∈ B.carrier ↔ x ∈ B.carrier
⊢ x ∈ A.carrier ↔ x ∈ B.carrier

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : FiniteIndexNormalSubgroup G
⊢ H.Normal

Tactic:
H.isNormal'

Premises used: FiniteIndexNormalSubgroup.isNormal'
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : FiniteIndexNormalSubgroup G
⊢ H.FiniteIndex

Tactic:
H.isFiniteIndex'

Premises used: FiniteIndexNormalSubgroup.isFiniteIndex'
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : FiniteIndexNormalSubgroup G
g : G
⊢ g ∈ H.toSubgroup ↔ g ∈ H

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
inst_2 : H.FiniteIndex
⊢ (ofSubgroup H).toSubgroup = H

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : Type u_2
N : Type u_3
inst_1 : Group H
inst_2 : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : MonoidHom.{u_1, u_2} G (H ⧸ K.toSubgroup) := MonoidHom.comp (QuotientGroup.mk' K.toSubgroup) f
⊢ Subgroup.comap f K.toSubgroup = g.ker

Tactic:
simpa using MonoidHom.comap_ker (g := QuotientGroup.mk' K.toSubgroup) (f := f)

Premises used: FiniteIndexNormalSubgroup.toSubgroup, QuotientGroup.mk', MonoidHom.comap_ker
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : Type u_2
N : Type u_3
inst_1 : Group H
inst_2 : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : MonoidHom.{u_1, u_2} G (H ⧸ K.toSubgroup) := MonoidHom.comp (QuotientGroup.mk' K.toSubgroup) f
⊢ Subgroup.comap f K.toSubgroup = g.ker

Tactic:
have hker : K.toSubgroup.comap f = g.ker := by
      simpa using MonoidHom.comap_ker (g := QuotientGroup.mk' K.toSubgroup) (f := f)
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : Type u_2
N : Type u_3
inst_1 : Group H
inst_2 : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : MonoidHom.{u_1, u_2} G (H ⧸ K.toSubgroup) := MonoidHom.comp (QuotientGroup.mk' K.toSubgroup) f
hker : Subgroup.comap f K.toSubgroup = g.ker
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex

Tactic:
simpa [hker] using (inferInstance : g.ker.FiniteIndex)

Premises used: inferInstance
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
K : FiniteIndexNormalSubgroup H
⊢ (comap f K).toSubgroup = Subgroup.comap f K.toSubgroup

Tactic:
rfl

Premises used: Subgroup.comap, rfl
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
K L : FiniteIndexNormalSubgroup H
h : K ≤ L
⊢ comap f K ≤ comap f L

Tactic:
fun _ hx ↦ h hx

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
K : FiniteIndexNormalSubgroup G
⊢ comap (MonoidHom.id G) K = K

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Goal:
G : Type u_1
inst : Group G
H : Type u_2
N : Type u_3
inst_1 : Group H
inst_2 : Group N
f : G →* H
g : H →* N
K : FiniteIndexNormalSubgroup N
⊢ comap (g.comp f) K = comap f (comap g K)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
hN : N.IsNormalClosureFG
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
obtain : ∀ (S : Set G) (hSfinite : S.Finite) (hSclosure : normalClosure S = N), (map f N).IsNormalClosureFG
⊢ (map f N).IsNormalClosureFG

Tactic:
obtain ⟨S, hSfinite, hSclosure⟩ := hN
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
⊢ (map f N).IsNormalClosureFG

Tactic:
⟨f '' S, hSfinite.image _, ?_⟩

Premises used: Set.Finite.image, And.intro, Exists.intro, Subgroup.IsNormalClosureFG, Set.image, DFunLike.coe
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
refine : normalClosure ((⇑f : (a : G) → H) '' S) = map f N
⊢ (map f N).IsNormalClosureFG

Tactic:
refine ⟨f '' S, hSfinite.image _, ?_⟩
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
rw : normalClosure ((⇑f : (a : G) → H) '' S) = map f (normalClosure S)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Subgroup H) (normalClosure ((⇑f : (a : G) → H) '' S)) (normalClosure ((⇑f : (a : G) → H) '' S))
⊢ normalClosure ((⇑f : (a : G) → H) '' S) = map f N

Tactic:
rw [← hSclosure, Subgroup.map_normalClosure _ _ hf]

Premises used: Subgroup.map_normalClosure
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
inst : Group G
⊢ IsNormalClosureFG.{u_1} (G := G) ⊥

Tactic:
⟨∅, Finite.of_subsingleton, normalClosure_empty⟩

Premises used: Finite.of_subsingleton, And.intro, Exists.intro, Subgroup.IsNormalClosureFG, Subgroup.normalClosure_empty, EmptyCollection.emptyCollection
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
iso : G ≃* H
h : IsFinitelyPresented G
obtain :
  ∀ (n : ℕ) (φ : FreeGroup (Fin n) →* G)
    (hφsurj : Function.Surjective (α := FreeGroup (Fin n)) (β := G) (⇑φ : (a : FreeGroup (Fin n)) → G))
    (hNC : φ.ker.IsNormalClosureFG), IsFinitelyPresented H
⊢ IsFinitelyPresented H

Tactic:
obtain ⟨n, φ, hφsurj, hNC⟩ := h
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
iso : G ≃* H
n : ℕ
φ : FreeGroup (Fin n) →* G
hφsurj : Function.Surjective (α := FreeGroup (Fin n)) (β := G) (⇑φ : (a : FreeGroup (Fin n)) → G)
hNC : φ.ker.IsNormalClosureFG
⊢ IsFinitelyPresented H

Tactic:
⟨n, (iso : G →* H).comp φ, iso.surjective.comp hφsurj, ?_⟩

Premises used: MonoidHomClass.toMonoidHom, MonoidHom.comp, MulEquiv.surjective, Group.IsFinitelyPresented.mk, And.intro, Exists.intro, Function.Surjective.comp
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
iso : G ≃* H
n : ℕ
φ : FreeGroup (Fin n) →* G
hφsurj : Function.Surjective (α := FreeGroup (Fin n)) (β := G) (⇑φ : (a : FreeGroup (Fin n)) → G)
hNC : φ.ker.IsNormalClosureFG
refine : (MonoidHom.ker (MonoidHom.comp (↑iso : G →* H) φ)).IsNormalClosureFG
⊢ IsFinitelyPresented H

Tactic:
refine ⟨n, (iso : G →* H).comp φ, iso.surjective.comp hφsurj, ?_⟩
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
iso : G ≃* H
n : ℕ
φ : FreeGroup (Fin n) →* G
hφsurj : Function.Surjective (α := FreeGroup (Fin n)) (β := G) (⇑φ : (a : FreeGroup (Fin n)) → G)
hNC rwa rwa₁ rwa₂ rwa₃ : φ.ker.IsNormalClosureFG
⊢ (MonoidHom.ker (MonoidHom.comp (↑iso : G →* H) φ)).IsNormalClosureFG

Tactic:
rwa [φ.ker_mulEquiv_comp iso]

Premises used: MonoidHom.ker_mulEquiv_comp
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
have :
  ∀ (n : ℕ) (toFun : α → Fin n) (f : Fin n → α) (hf_surj : Function.LeftInverse f toFun)
    (hf_inj : Function.RightInverse f toFun), IsFinitelyPresented.{u_3} (FreeGroup α)
⊢ IsFinitelyPresented.{u_3} (FreeGroup α)

Tactic:
have ⟨n, _, f, hf_surj, hf_inj⟩ := Finite.exists_equiv_fin α
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
n : ℕ
toFun : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun
hf_inj : Function.RightInverse f toFun
⊢ IsFinitelyPresented.{u_3} (FreeGroup α)

Tactic:
⟨n, FreeGroup.map f, FreeGroup.map_surjective hf_surj.surjective, ?_⟩

Premises used: FreeGroup.map, Group.IsFinitelyPresented.mk, And.intro, Exists.intro, FreeGroup.map_surjective, Function.LeftInverse.surjective
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
n : ℕ
toFun : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun
hf_inj : Function.RightInverse f toFun
refine : (FreeGroup.map f).ker.IsNormalClosureFG
⊢ IsFinitelyPresented.{u_3} (FreeGroup α)

Tactic:
refine ⟨n, FreeGroup.map f, FreeGroup.map_surjective hf_surj.surjective, ?_⟩
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
n : ℕ
toFun : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun
hf_inj : Function.RightInverse f toFun
rw : Subgroup.IsNormalClosureFG (G := FreeGroup (Fin n)) ⊥
⊢ (FreeGroup.map f).ker.IsNormalClosureFG

Tactic:
rw [(FreeGroup.map f).ker_eq_bot_iff.mpr (FreeGroup.map_injective hf_inj.injective)]

Premises used: FreeGroup.map_injective, Iff.mpr, FreeGroup.map, MonoidHom.ker_eq_bot_iff, Function.RightInverse.injective
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
n : ℕ
toFun : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun
hf_inj : Function.RightInverse f toFun
⊢ Subgroup.IsNormalClosureFG (G := FreeGroup (Fin n)) ⊥

Tactic:
.bot

Premises used: Subgroup.IsNormalClosureFG.bot
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
n : ℕ
toFun : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun
hf_inj : Function.RightInverse f toFun
⊢ Subgroup.IsNormalClosureFG (G := FreeGroup (Fin n)) ⊥

Tactic:
exact .bot
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
⊢ IsFinitelyPresented (Multiplicative ℤ)

Tactic:
equiv (FreeGroup.mulEquivIntOfUnique : FreeGroup Unit ≃* Multiplicative ℤ) inferInstance

Premises used: FreeGroup.mulEquivIntOfUnique, inferInstance, Group.IsFinitelyPresented.equiv
-- Module: Mathlib.GroupTheory.FinitelyPresentedGroup
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
⊢ AddGroup.IsFinitelyPresented ℤ

Tactic:
AddGroup.IsFinitelyPresented.equiv
    (FreeAddGroup.addEquivIntOfUnique : FreeAddGroup Unit ≃+ ℤ) inferInstance

Premises used: FreeAddGroup.addEquivIntOfUnique, inferInstance, AddGroup.IsFinitelyPresented.equiv
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
P : Submonoid M
h : ∃ (S : Set M), closure S = P ∧ S.Finite
S : Set M
hS : closure S = P
hf : S.Finite
⊢ closure (↑(hf.toFinset (s := S)) : Set M) = P

Tactic:
simp [hS]
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
P : Submonoid M
hP : P.FG
⊢ ∃ (S : Finset M), Minimal (fun (S : Finset M) ↦ closure (↑S : Set M) = P) S

Tactic:
exists_minimal_of_wellFoundedLT _ hP

Premises used: exists_minimal_of_wellFoundedLT
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
P : Submonoid M
h : P.FG
S : Set M
hS : closure S = P
hf : S.Finite
⊢ Eq (α := AddSubmonoid (Additive M)) (AddSubmonoid.closure ((⇑Additive.toMul : (a : Additive M) → M) ⁻¹' S))
    ((toAddSubmonoid : (a : Submonoid M) → AddSubmonoid (Additive M)) P)

Tactic:
simp [← Submonoid.toAddSubmonoid_closure, hS]

Premises used: Submonoid.toAddSubmonoid_closure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
P : Submonoid M
h : AddSubmonoid.FG.{u_1} (M := Additive M) ((toAddSubmonoid : (a : Submonoid M) → AddSubmonoid (Additive M)) P)
T : Set (Additive M)
hT :
  Eq (α := AddSubmonoid (Additive M)) (AddSubmonoid.closure T)
    ((toAddSubmonoid : (a : Submonoid M) → AddSubmonoid (Additive M)) P)
hf : T.Finite
⊢ closure ((⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' T) = P

Tactic:
simp [← AddSubmonoid.toSubmonoid'_closure, hT]

Premises used: AddSubmonoid.toSubmonoid'_closure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_3
inst : AddMonoid M
P : AddSubmonoid M
⊢ FG.{u_3} (M := Additive (Multiplicative M))
      ((Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative M)) → AddSubmonoid (Additive (Multiplicative M)))
        ((toSubmonoid : (a : AddSubmonoid M) → Submonoid (Multiplicative M)) P)) ↔
    Submonoid.FG.{u_3} (M := Multiplicative M) ((toSubmonoid : (a : AddSubmonoid M) → Submonoid (Multiplicative M)) P)

Tactic:
(Submonoid.fg_iff_add_fg (toSubmonoid P)).symm

Premises used: Submonoid.fg_iff_add_fg, AddSubmonoid.toSubmonoid, DFunLike.coe, Iff.symm
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_3
inst : AddMonoid M
P : AddSubmonoid M
⊢ P.FG ↔
    Submonoid.FG.{u_3} (M := Multiplicative M) ((toSubmonoid : (a : AddSubmonoid M) → Submonoid (Multiplicative M)) P)

Tactic:
convert! (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm

Premises used: Submonoid.fg_iff_add_fg, AddSubmonoid.toSubmonoid, DFunLike.coe, Iff.symm
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq (α := Submonoid M) (closure (↑∅ : Set M)) ⊥

Tactic:
simp
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
P Q : Submonoid M
hP : P.FG
hQ : Q.FG
rcases : ∀ (s : Finset M), (closure (↑s : Set M) ⊔ Q).FG
⊢ (P ⊔ Q).FG

Tactic:
rcases hP with ⟨s, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
Q : Submonoid M
hQ : Q.FG
s : Finset M
rcases : ∀ (t : Finset M), FG (closure (↑s : Set M) ⊔ closure (↑t : Set M))
⊢ (closure (↑s : Set M) ⊔ Q).FG

Tactic:
rcases hQ with ⟨t, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
s t : Finset M
⊢ Eq (α := Submonoid M) (closure (↑(s ∪ t) : Set M)) (closure (↑s : Set M) ⊔ closure (↑t : Set M))

Tactic:
simp [closure_union]

Premises used: Submonoid.closure_union
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
s t : Finset M
⊢ FG (closure (↑s : Set M) ⊔ closure (↑t : Set M))

Tactic:
exact ⟨s ∪ t, by simp [closure_union]⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
P Q : Submonoid M
hP : P.FG
hQ : Q.FG
rcases : ∀ (s : Finset M), (closure (↑s : Set M) ⊔ Q).FG
rcases₁ : ∀ (s t : Finset M), FG (closure (↑s : Set M) ⊔ closure (↑t : Set M))
⊢ (P ⊔ Q).FG

Tactic:
classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_3
s : Finset ι
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ (s.sup P).FG

Tactic:
Finset.sup_induction bot (fun _ ha _ hb => ha.sup hb) hP

Premises used: Finset.sup_induction, Submonoid.FG.sup, Submonoid.FG.bot
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_3
s : Finset ι
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ FG.{u_1} (M := M) (⨆ i ∈ s, P i)

Tactic:
simpa only [Finset.sup_eq_iSup] using finset_sup s P hP

Premises used: Submonoid.FG.finset_sup, Finset.sup_eq_iSup
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_3
s : Set ι
hs : s.Finite
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ ∀ i ∈ hs.toFinset (s := s), (P i).FG

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_3
s : Set ι
hs : s.Finite
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ FG.{u_1} (M := M) (⨆ i ∈ s, P i)

Tactic:
simpa using biSup_finset hs.toFinset P (by simpa)

Premises used: Set.Finite.toFinset, Submonoid.FG.biSup_finset
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
ι : Sort u_3
inst_1 : Finite ι
P : ι → Submonoid M
hP : ∀ (i : ι), (P i).FG
⊢ (_root_.iSup P).FG

Tactic:
simpa [iSup_plift_down] using biSup Set.finite_univ (P ∘ PLift.down) fun i _ => hP i.down

Premises used: iSup_plift_down, Function.comp, PLift.down, Set.finite_univ, Submonoid.FG.biSup
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
P : Submonoid M
Q : Submonoid N
hP : P.FG
hQ : Q.FG
obtain : ∀ (bM : Finset M) (hbM : closure (↑bM : Set M) = P), (P.prod Q).FG (M := M × N)
⊢ (P.prod Q).FG (M := M × N)

Tactic:
obtain ⟨bM, hbM⟩ := hP
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
P : Submonoid M
Q : Submonoid N
hQ : Q.FG
bM : Finset M
hbM : closure (↑bM : Set M) = P
obtain : ∀ (bN : Finset N) (hbN : closure (↑bN : Set N) = Q), (P.prod Q).FG (M := M × N)
⊢ (P.prod Q).FG (M := M × N)

Tactic:
obtain ⟨bN, hbN⟩ := hQ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
P : Submonoid M
Q : Submonoid N
bM : Finset M
hbM : closure (↑bM : Set M) = P
bN : Finset N
hbN : closure (↑bN : Set N) = Q
⊢ (P.prod Q).FG (M := M × N)

Tactic:
⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩

Premises used: SProd.sprod, Exists.intro, Union.union, Submonoid.FG, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
P : Submonoid M
Q : Submonoid N
bM : Finset M
hbM : closure (↑bM : Set M) = P
bN : Finset N
hbN : closure (↑bN : Set N) = Q
refine : closure (↑(SProd.sprod (β := Finset N) bM {1} ∪ SProd.sprod (α := Finset M) {1} bN) : Set (M × N)) = P.prod Q
⊢ (P.prod Q).FG (M := M × N)

Tactic:
refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
P : Submonoid M
Q : Submonoid N
bM : Finset M
hbM : closure (↑bM : Set M) = P
bN : Finset N
hbN : closure (↑bN : Set N) = Q
push_cast : closure (SProd.sprod (β := Set N) (↑bM : Set M) {1} ∪ SProd.sprod (α := Set M) {1} (↑bN : Set N)) = P.prod Q
⊢ closure (↑(SProd.sprod (β := Finset N) bM {1} ∪ SProd.sprod (α := Finset M) {1} bN) : Set (M × N)) = P.prod Q

Tactic:
push_cast