awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
inst_5 : Monoid N
inst_6 : IsCancelMul N
f g : M →* N
⊢ ∀ x ∈ f.eqLocusM g, ∀ (y : M), x * y ∈ f.eqLocusM g → y ∈ f.eqLocusM g

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
G : Type u_2
φ : G → G
inst : Div G
g : G
⊢ commutatorMap φ g = g / φ g

Tactic:
rfl

Premises used: MonoidHom.commutatorMap, rfl
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := G) (commutatorMap (⇑φ : (a : G) → G))

Tactic:
fun x y h ↦ inv_mul_eq_one.mp <| hφ _ ?_

Premises used: HMul.hMul, Inv.inv, Iff.mp, Function.Injective, inv_mul_eq_one
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
refine :
  ∀ (x y : G) (h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y),
    (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := G) (commutatorMap (⇑φ : (a : G) → G))

Tactic:
refine fun x y h ↦ inv_mul_eq_one.mp <| hφ _ ?_

Premises used: HMul.hMul, Inv.inv, Iff.mp, inv_mul_eq_one
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
x y : G
h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y
rwa : HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) x⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₁ : HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₂ : x * HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = y
rwa₃ : HMul.hMul (β := G) (HMul.hMul (β := G) x (((φ : (a : G) → G) x)⁻¹ : G)) ((φ : (a : G) → G) y : G) = y
rwa₄ : HMul.hMul (β := G) x (((φ : (a : G) → G) x)⁻¹ : G) = HDiv.hDiv (β := G) y ((φ : (a : G) → G) y : G)
rwa₅ rwa₆ rwa₇ rwa₈ : HDiv.hDiv (β := G) x ((φ : (a : G) → G) x : G) = HDiv.hDiv (β := G) y ((φ : (a : G) → G) y : G)
⊢ (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y

Tactic:
rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]

Premises used: map_inv, mul_assoc, division_def, eq_inv_mul_iff_mul_eq, map_mul, eq_div_iff_mul_eq'
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
⊢ Function.Surjective.{u_2 + 1, u_2 + 1} (α := G) (commutatorMap (⇑φ : (a : G) → G))

Tactic:
Finite.surjective_of_injective hφ.commutatorMap_injective

Premises used: Finite.surjective_of_injective, MonoidHom.FixedPointFree.commutatorMap_injective
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
obtain :
  ∀ (g : G),
    Eq.{u_2 + 1} (α := G)
      (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] (commutatorMap (⇑φ : (a : G) → G) g)) (List.range n)))
      1
⊢ Eq.{u_2 + 1} (α := G) (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g) (List.range n))) 1

Tactic:
obtain ⟨g, rfl⟩ := commutatorMap_surjective hφ g

Premises used: MonoidHom.FixedPointFree.commutatorMap_surjective, rfl
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
simp :
  Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g / (⇑φ : (a : G) → G)^[k.succ] g) (List.range n))) 1
⊢ Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] (commutatorMap (⇑φ : (a : G) → G) g)) (List.range n))) 1

Tactic:
simp only [commutatorMap_apply, iterate_map_div, ← Function.iterate_succ_apply]

Premises used: iterate_map_div, MonoidHom.commutatorMap_apply, Function.iterate_succ_apply
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
rw : (⇑φ : (a : G) → G)^[0] g / (⇑φ : (a : G) → G)^[n] g = 1
rw₁ : g / (⇑φ : (a : G) → G)^[n] g = 1
rw₂ : g / _root_.id g = 1
rw₃ : g / (fun (x : G) ↦ x) g = 1
rw₄ rw₅ : Eq.{u_2 + 1} (α := G) 1 1
⊢ Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g / (⇑φ : (a : G) → G)^[k.succ] g) (List.range n))) 1

Tactic:
rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']

Premises used: Function.id_def, div_self', List.prod_range_div', Function.iterate_zero_apply
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[2] _root_.id
h : ∀ (g : G), (φ : (a : G) → G) g = g⁻¹
⊢ Eq.{u_2 + 1} (α := (a : G) → G) (⇑φ : (a : G) → G) fun (x : G) ↦ x⁻¹

Tactic:
ext g
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[2] _root_.id
g : G
⊢ HMul.hMul (β := G) g ((φ : (a : G) → G) g : G) = 1

Tactic:
simpa [List.range_succ] using hφ.prod_pow_eq_one h2 g

Premises used: MonoidHom.FixedPointFree.prod_pow_eq_one, List.range_succ
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[2] _root_.id
g : G
⊢ HMul.hMul (β := G) g ((φ : (a : G) → G) g : G) = 1

Tactic:
have key : g * φ g = 1 := by simpa [List.range_succ] using hφ.prod_pow_eq_one h2 g
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[2] _root_.id
g : G
key : HMul.hMul (β := G) g ((φ : (a : G) → G) g : G) = 1
h : ∀ (key : g⁻¹ = (φ : (a : G) → G) g), (φ : (a : G) → G) g = g⁻¹
h₁ h₂ h₃ h₄ : ∀ (key : (φ : (a : G) → G) g = g⁻¹), (φ : (a : G) → G) g = g⁻¹
⊢ (φ : (a : G) → G) g = g⁻¹

Tactic:
rwa [← inv_eq_iff_mul_eq_one, eq_comm] at key

Premises used: eq_comm, inv_eq_iff_mul_eq_one
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
⊢ Eq.{u_2 + 1} (α := (a : G) → G) (⇑φ : (a : G) → G) fun (x : G) ↦ x⁻¹

Tactic:
coe_eq_inv_of_sq_eq_one hφ (funext h2)

Premises used: MonoidHom.FixedPointFree.coe_eq_inv_of_sq_eq_one, funext
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g h : G
⊢ (φ : (a : G) → G) (g * h) = HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) g : G) ((φ : (a : G) → G) h : G)

Tactic:
have key := map_mul φ g h
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g h : G
key : (φ : (a : G) → G) (g * h) = HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) g : G) ((φ : (a : G) → G) h : G)
rwa :
  ∀ (key : (fun (x : G) ↦ x⁻¹) (g * h) = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h)),
    Commute g h
rwa₁ : ∀ (key : g * h = (HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h))⁻¹), Commute g h
rwa₂ : ∀ (key : g * h = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) h)⁻¹ ((fun (x : G) ↦ x⁻¹) g)⁻¹), Commute g h
rwa₃ : ∀ (key : g * h = h * ((fun (x : G) ↦ x⁻¹) g)⁻¹), Commute g h
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (key : g * h = h * g), Commute g h
⊢ Commute g h

Tactic:
rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key

Premises used: MonoidHom.FixedPointFree.coe_eq_inv_of_involutive, inv_inv, mul_inv_rev, inv_eq_iff_eq_inv
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
rw : (fun (x : G) ↦ x⁻¹) g = g
rw₁ : g * g = 1
rw₂ : HPow.hPow (β := ℕ) g 2 = 1
rw₃ : g ^ orderOf g = 1
rw₄ rw₅ : Eq.{u_2 + 1} (α := G) 1 1
⊢ (φ : (a : G) → G) g = g

Tactic:
rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]

Premises used: MonoidHom.FixedPointFree.coe_eq_inv_of_involutive, sq, pow_orderOf_eq_one, inv_eq_iff_mul_eq_one
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
⊢ (φ : (a : G) → G) g = g

Tactic:
have key : φ g = g := by
    rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
key : (φ : (a : G) → G) g = g
⊢ Eq (α := ℕ) 1 2

Tactic:
rw [hφ g key, orderOf_one] at hg

Premises used: orderOf_one
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
key : (φ : (a : G) → G) g = g
hg₁ : Eq (α := ℕ) 1 2
⊢ (φ : (a : G) → G) g = g

Tactic:
rw [hφ g key, orderOf_one] at hg

Premises used: orderOf_one
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : Eq (α := ℕ) 1 2
key : (φ : (a : G) → G) g = g
⊢ False

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
have : ∀ (this : Fintype G), Odd (Nat.card G)
⊢ Odd (Nat.card G)

Tactic:
have := Fintype.ofFinite G
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
this : Fintype G
by_contra : ∀ (h : ¬Odd (Nat.card G)), False
⊢ Odd (Nat.card G)

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
this : Fintype G
h : ¬Odd (Nat.card G)
⊢ 2 ∣ Fintype.card G

Tactic:
rw [Nat.not_odd_iff_even, even_iff_two_dvd, Nat.card_eq_fintype_card] at h

Premises used: Nat.not_odd_iff_even, even_iff_two_dvd, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
this : Fintype G
h : 2 ∣ Fintype.card G
obtain : ∀ (g : G) (hg : orderOf g = 2), False
⊢ False

Tactic:
obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card 2 h

Premises used: exists_prime_orderOf_dvd_card, OfNat.ofNat
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
this : Fintype G
h : 2 ∣ Fintype.card G
g : G
hg : orderOf g = 2
⊢ False

Tactic:
hφ.orderOf_ne_two_of_involutive h2 g hg

Premises used: MonoidHom.FixedPointFree.orderOf_ne_two_of_involutive
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
this : Fintype G
h : 2 ∣ Fintype.card G
g : G
hg : orderOf g = 2
⊢ False

Tactic:
exact hφ.orderOf_ne_two_of_involutive h2 g hg

Premises used: MonoidHom.FixedPointFree.orderOf_ne_two_of_involutive
-- Module: Mathlib.GroupTheory.FixedPointFree
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
⊢ Odd (orderOf g)

Tactic:
Odd.of_dvd_nat (hφ.odd_card_of_involutive h2) (orderOf_dvd_natCard g)

Premises used: orderOf_dvd_natCard, Odd.of_dvd_nat, MonoidHom.FixedPointFree.odd_card_of_involutive
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.focalSubgroup = closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}

Tactic:
rfl

Premises used: Subgroup.focalSubgroup, rfl
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.focalSubgroupOf = H.focalSubgroup.subgroupOf H

Tactic:
rfl

Premises used: Subgroup.focalSubgroupOf, rfl
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} ⊆ (↑H : Set G)
⊢ H.focalSubgroup ≤ H

Tactic:
rw [focalSubgroup_def, closure_le]

Premises used: Subgroup.closure_le, Subgroup.focalSubgroup_def
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
h : g ∈ H
⊢ g ∈ (↑H : Set G)

Tactic:
h
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
h : g ∈ H
⊢ g ∈ (↑H : Set G)

Tactic:
exact h
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ map H.subtype H.focalSubgroupOf = H.focalSubgroup

Tactic:
map_subgroupOf_eq_of_le H.focalSubgroup_le

Premises used: Subgroup.map_subgroupOf_eq_of_le, Subgroup.focalSubgroupOf, Subgroup.focalSubgroup_le
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : ∀ (h k : G), h ∈ H.focalSubgroup → k ∈ H → k * h * k⁻¹ ∈ H.focalSubgroup
⊢ H.focalSubgroupOf.Normal

Tactic:
rw [focalSubgroupOf_def, normal_subgroupOf_iff (focalSubgroup_le H)]

Premises used: Subgroup.normal_subgroupOf_iff, Subgroup.focalSubgroupOf_def, Subgroup.focalSubgroup_le
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
z : G
hz : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} z
mem : ∀ (x : G) (hxP : x ∈ H) (u : G) (hzH : ⁅x, u⁆ ∈ H), g * ⁅x, u⁆ * g⁻¹ ∈ H.focalSubgroup
⊢ g * z * g⁻¹ ∈ H.focalSubgroup

Tactic:
obtain ⟨hzH, x, hxP, u, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x : G
hxP : x ∈ H
u : G
hzH : ⁅x, u⁆ ∈ H
⊢ g * ⁅x, u⁆ * g⁻¹ ∈ H

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x : G
hxP : x ∈ H
u : G
hzH : ⁅x, u⁆ ∈ H
⊢ g * x * g⁻¹ ∈ H

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x : G
hxP : x ∈ H
u : G
hzH : ⁅x, u⁆ ∈ H
⊢ g * ⁅x, u⁆ * g⁻¹ = ⁅g * x * g⁻¹, g * u * g⁻¹⁆

Tactic:
group
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x : G
hxP : x ∈ H
u : G
hzH : ⁅x, u⁆ ∈ H
⊢ g * ⁅x, u⁆ * g⁻¹ ∈ H.focalSubgroup

Tactic:
exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
⊢ g * 1 * g⁻¹ ∈ H.focalSubgroup

Tactic:
simp
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x y : G
hx : Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) x
hy : Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) y
IHa : g * x * g⁻¹ ∈ H.focalSubgroup
IHb : g * y * g⁻¹ ∈ H.focalSubgroup
⊢ g * (x * y) * g⁻¹ ∈ H.focalSubgroup

Tactic:
simpa using mul_mem IHa IHb

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x : G
hx : Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) x
IH : g * x * g⁻¹ ∈ H.focalSubgroup
⊢ g * x⁻¹ * g⁻¹ ∈ H.focalSubgroup

Tactic:
simpa [mul_assoc] using inv_mem IH

Premises used: mul_assoc, InvMemClass.inv_mem
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hn : n ∈ H.focalSubgroup
hg : g ∈ H
mem :
  ∀ (z : G) (hz : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} z),
    g * z * g⁻¹ ∈ H.focalSubgroup
one : g * 1 * g⁻¹ ∈ H.focalSubgroup
mul :
  ∀ (x y : G),
    Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) x →
      Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) y →
        ∀ (IHa : g * x * g⁻¹ ∈ H.focalSubgroup) (IHb : g * y * g⁻¹ ∈ H.focalSubgroup),
          g * (x * y) * g⁻¹ ∈ H.focalSubgroup
inv :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) x →
      ∀ (IH : g * x * g⁻¹ ∈ H.focalSubgroup), g * x⁻¹ * g⁻¹ ∈ H.focalSubgroup
⊢ g * n * g⁻¹ ∈ H.focalSubgroup

Tactic:
induction hn using closure_induction with
  | mem z hz =>
    obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
    exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩
  | one => simp
  | mul _ _ _ _ IHa IHb => simpa using mul_mem IHa IHb
  | inv _ _ IH => simpa [mul_assoc] using inv_mem IH

Premises used: mul_assoc, Subgroup.mul, Subgroup.one, Subgroup.inv, rfl
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} ⊆ (↑(_root_.commutator G) : Set G)
⊢ H.focalSubgroup ≤ _root_.commutator G

Tactic:
rw [focalSubgroup_def, closure_le]

Premises used: Subgroup.closure_le, Subgroup.focalSubgroup_def
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
left : x ∈ H
u : G
left_1 : ⁅x, u⁆ ∈ H
⊢ ⁅x, u⁆ ∈ (↑(_root_.commutator G) : Set G)

Tactic:
commutator_mem_commutator (mem_top x) (mem_top u)

Premises used: Set.Mem, Subgroup.commutator_mem_commutator, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
left : x ∈ H
u : G
left_1 : ⁅x, u⁆ ∈ H
⊢ ⁅x, u⁆ ∈ (↑(_root_.commutator G) : Set G)

Tactic:
exact commutator_mem_commutator (mem_top x) (mem_top u)

Premises used: Subgroup.commutator_mem_commutator, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
apply :
  (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh ∈
    H.focalSubgroupOf
⊢ Eq (α := ↥H ⧸ H.focalSubgroupOf)
    ((QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj) :
      ↥H ⧸ H.focalSubgroupOf)
    ((QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) :
      ↥H ⧸ H.focalSubgroupOf)

Tactic:
apply QuotientGroup.eq.mpr

Premises used: Iff.mpr, QuotientGroup.eq
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
rw :
  (↑((Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) : G) ∈
    H.focalSubgroup
⊢ (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh ∈
    H.focalSubgroupOf

Tactic:
rw [focalSubgroupOf_def, mem_subgroupOf]

Premises used: Subgroup.focalSubgroupOf_def, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
a :
  Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}
    (↑((Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) : G)
⊢ (↑((Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) : G) ∈
    H.focalSubgroup

Tactic:
apply subset_closure

Premises used: Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
a : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} ((g⁻¹ * h * g)⁻¹ * h)
⊢ Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}
    (↑((Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) : G)

Tactic:
simp only [coe_mul, coe_inv]

Premises used: Subgroup.coe_inv, Subgroup.coe_mul
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ (g⁻¹ * h * g)⁻¹ * h = ⁅(g⁻¹ * h * g)⁻¹, g⁆

Tactic:
group
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} ((g⁻¹ * h * g)⁻¹ * h)

Tactic:
exact ⟨H.mul_mem (H.inv_mem hconj) hh, _, H.inv_mem hconj, g, by group⟩