awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
hf :
  (transferSylow P hP).ker ⊓ (↑P : Subgroup G) = ⊥ ∧
    (↑(transferSylow P hP).ker : Set G) * (↑(↑P : Subgroup G) : Set G) = Set.univ
this : Function.Surjective (α := G) (β := ↥(↑P : Subgroup G)) (⇑(transferSylow P hP) : (a : G) → ↥(↑P : Subgroup G))
⊢ (transferSylow P hP).ker.IsComplement' (↑P : Subgroup G)

Tactic:
isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2

Premises used: Iff.mpr, Subgroup.isComplement'_of_disjoint_and_mul_eq_univ, disjoint_iff, And.right, And.left
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
hf :
  (transferSylow P hP).ker ⊓ (↑P : Subgroup G) = ⊥ ∧
    (↑(transferSylow P hP).ker : Set G) * (↑(↑P : Subgroup G) : Set G) = Set.univ
this : Function.Surjective (α := G) (β := ↥(↑P : Subgroup G)) (⇑(transferSylow P hP) : (a : G) → ↥(↑P : Subgroup G))
⊢ (transferSylow P hP).ker.IsComplement' (↑P : Subgroup G)

Tactic:
exact isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2

Premises used: Iff.mpr, Subgroup.isComplement'_of_disjoint_and_mul_eq_univ, disjoint_iff, And.right, And.left
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
⊢ ¬p ∣ Nat.card.{u_1} ↥(transferSylow P hP).ker

Tactic:
(ker_transferSylow_isComplement' P hP).index_eq_card ▸ P.not_dvd_index

Premises used: MonoidHom.ker_transferSylow_isComplement', Subgroup.IsComplement'.index_eq_card, Sylow.not_dvd_index, Eq.rec
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
Q : Subgroup G
hQ : IsPGroup.{u_1} p ↥Q
⊢ Disjoint (transferSylow P hP).ker Q

Tactic:
disjoint_iff.mpr <|
    card_eq_one.mp <|
      (hQ.to_le inf_le_right).card_eq_or_dvd.resolve_right fun h =>
        not_dvd_card_ker_transferSylow P hP <| h.trans <| card_dvd_of_le inf_le_left

Premises used: Iff.mpr, Subgroup.card_eq_one, MonoidHom.not_dvd_card_ker_transferSylow, disjoint_iff, inf_le_right, IsPGroup.to_le, Subgroup.card_dvd_of_le, Iff.mp, inf_le_left, Or.resolve_right, IsPGroup.card_eq_or_dvd, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
p : ℕ
hp : (Nat.card G).minFac = p
P : Sylow p G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
subst :
  ∀ {P : Sylow (Nat.card G).minFac G} (hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)),
    LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))

Tactic:
subst hp
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
pos : ∀ (hn : Nat.card G = 1), LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
neg : ∀ (hn : ¬Nat.card G = 1), LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))

Tactic:
by_cases hn : Nat.card G = 1

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : Nat.card G = 1
⊢ Subsingleton G

Tactic:
have := (Nat.card_eq_one_iff_unique.mp hn).1
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : Nat.card G = 1
this : Subsingleton G
pos pos₁ : LE.le (α := Subgroup G) (centralizer (↑P : Set G)) (centralizer (↑P : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))

Tactic:
rw [Subsingleton.elim (normalizer _) (centralizer P)]

Premises used: Subgroup.centralizer, Subgroup.normalizer, Subsingleton.elim
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
⊢ Fact (Nat.Prime (Nat.card G).minFac)

Tactic:
have := Fact.mk (Nat.minFac_prime hn)
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
⊢ Nat.card.{u_3} (↥(normalizer (↑(↑P : Subgroup G) : Set G)) ⧸ (↑P : Subgroup G).normalizerMonoidHom.ker) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))

Tactic:
have key := card_dvd_of_injective _ (QuotientGroup.kerLift_injective P.normalizerMonoidHom)
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  Nat.card.{u_3} (↥(normalizer (↑(↑P : Subgroup G) : Set G)) ⧸ (↑P : Subgroup G).normalizerMonoidHom.ker) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
⊢ relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))

Tactic:
rw [normalizerMonoidHom_ker, ← index, ← relIndex] at key

Premises used: Subgroup.normalizerMonoidHom_ker, Subgroup.relIndex, Subgroup.index
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))

Tactic:
relIndex_eq_one.mp (Nat.eq_one_of_dvd_coprimes ?_ dvd_rfl key)

Premises used: Nat.eq_one_of_dvd_coprimes, Subgroup.relIndex_eq_one, Iff.mp, dvd_rfl
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
neg :
  (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))

Tactic:
refine relIndex_eq_one.mp (Nat.eq_one_of_dvd_coprimes ?_ dvd_rfl key)

Premises used: Nat.eq_one_of_dvd_coprimes, Subgroup.relIndex_eq_one, Iff.mp, dvd_rfl
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
neg :
  ∀ (k : ℕ) (hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k),
    (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))

Tactic:
obtain ⟨k, hk⟩ := P.2.exists_card_eq

Premises used: Sylow.isPGroup', IsPGroup.exists_card_eq
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
neg :
  ∀ (h0 : k = 0),
    (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
neg₁ :
  ∀ (h0 : 0 < k),
    (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))

Tactic:
rcases eq_zero_or_pos k with h0 | h0

Premises used: eq_zero_or_pos
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : k = 0
neg : (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime 1
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))

Tactic:
rw [hP.card_mulAut, hk, h0, pow_zero, Nat.totient_one]

Premises used: pow_zero, IsCyclic.card_mulAut, Nat.totient_one
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : k = 0
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime 1

Tactic:
apply Nat.coprime_one_right

Premises used: Nat.coprime_one_right
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
neg :
  (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime
    ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))

Tactic:
rw [hP.card_mulAut, hk, Nat.totient_prime_pow Fact.out h0]

Premises used: Nat.totient_prime_pow, IsCyclic.card_mulAut, Fact.out
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime
    ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))

Tactic:
(Nat.Coprime.pow_right _ ?_).mul_right ?_

Premises used: Nat.Coprime.pow_right, Nat.Coprime.mul_right
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
neg : (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card G).minFac
neg₁ : (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime ((Nat.card G).minFac - 1)
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime
    ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))

Tactic:
refine (Nat.Coprime.pow_right _ ?_).mul_right ?_

Premises used: Nat.Coprime.pow_right, Nat.Coprime.mul_right
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
neg : ((↑P : Subgroup G).relIndex (normalizer (↑P : Set G))).Coprime (Nat.card G).minFac
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card G).minFac

Tactic:
apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_of_le_left _ P.le_centralizer)

Premises used: Sylow.toSubgroup, Nat.Coprime.coprime_dvd_left, Subgroup.le_centralizer, Subgroup.relIndex_dvd_of_le_left
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
neg : (↑P : Subgroup G).index.Coprime (Nat.card G).minFac
⊢ ((↑P : Subgroup G).relIndex (normalizer (↑P : Set G))).Coprime (Nat.card G).minFac

Tactic:
apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_index_of_le P.le_normalizer)

Premises used: Subgroup.relIndex_dvd_index_of_le, Nat.Coprime.coprime_dvd_left, Subgroup.le_normalizer
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
neg : ¬(Nat.card G).minFac ∣ (↑P : Subgroup G).index
⊢ (↑P : Subgroup G).index.Coprime (Nat.card G).minFac

Tactic:
rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd Fact.out]

Premises used: Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ¬(Nat.card G).minFac ∣ (↑P : Subgroup G).index

Tactic:
P.not_dvd_index

Premises used: Sylow.not_dvd_index
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ¬(Nat.card G).minFac ∣ (↑P : Subgroup G).index

Tactic:
exact P.not_dvd_index

Premises used: Sylow.not_dvd_index
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
neg : (Nat.card.{u_3} ↥(normalizer (↑P : Set G))).Coprime ((Nat.card G).minFac - 1)
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime ((Nat.card G).minFac - 1)

Tactic:
apply Nat.Coprime.coprime_dvd_left <| relIndex_dvd_card ..

Premises used: Nat.Coprime.coprime_dvd_left, Subgroup.relIndex_dvd_card
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
neg : (Nat.card G).Coprime ((Nat.card G).minFac - 1)
⊢ (Nat.card.{u_3} ↥(normalizer (↑P : Set G))).Coprime ((Nat.card G).minFac - 1)

Tactic:
apply Nat.Coprime.coprime_dvd_left <| card_subgroup_dvd_card _

Premises used: Nat.Coprime.coprime_dvd_left, Subgroup.card_subgroup_dvd_card
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G

Tactic:
have h1 := Nat.gcd_dvd_left (Nat.card G) ((Nat.card G).minFac - 1)
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
⊢ (Nat.card G).gcd ((Nat.card G).minFac - 1) ≤ (Nat.card G).minFac - 1

Tactic:
have h2 := Nat.gcd_le_right (n := (Nat.card G).minFac - 1) (Nat.card G)
      (tsub_pos_iff_lt.mpr (Nat.minFac_prime hn).one_lt)
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≤ (Nat.card G).minFac - 1
neg :
  ∀ (h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≠ 1),
    (Nat.card G).minFac - 1 < (Nat.card G).gcd ((Nat.card G).minFac - 1)
⊢ (Nat.card G).Coprime ((Nat.card G).minFac - 1)

Tactic:
contrapose! h2
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≠ 1
⊢ (Nat.card G).minFac - 1 < (Nat.card G).gcd ((Nat.card G).minFac - 1)

Tactic:
Nat.sub_one_lt_of_le (Nat.card G).minFac_pos (Nat.minFac_le_of_dvd ?_ h1)

Premises used: Nat.minFac_le_of_dvd, Nat.card, Nat.minFac_pos, Nat.sub_one_lt_of_le
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≠ 1
neg : 2 ≤ (Nat.card G).gcd ((Nat.card G).minFac - 1)
⊢ (Nat.card G).minFac - 1 < (Nat.card G).gcd ((Nat.card G).minFac - 1)

Tactic:
refine Nat.sub_one_lt_of_le (Nat.card G).minFac_pos (Nat.minFac_le_of_dvd ?_ h1)

Premises used: Nat.minFac_le_of_dvd, Nat.card, Nat.minFac_pos, Nat.sub_one_lt_of_le
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≠ 1
⊢ 2 ≤ (Nat.card G).gcd ((Nat.card G).minFac - 1)

Tactic:
(Nat.two_le_iff _).mpr ⟨ne_zero_of_dvd_ne_zero Nat.card_pos.ne' h1, h2⟩

Premises used: Iff.mpr, Nat.two_le_iff, Nat.card_pos, LT.lt.ne', And.intro, ne_zero_of_dvd_ne_zero
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key :
  relIndex (centralizer (↑(↑P : Subgroup G) : Set G)) (normalizer (↑(↑P : Subgroup G) : Set G)) ∣
    Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G))
k : ℕ
hk : Nat.card.{u_3} ↥(↑P : Subgroup G) = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≠ 1
⊢ 2 ≤ (Nat.card G).gcd ((Nat.card G).minFac - 1)

Tactic:
exact (Nat.two_le_iff _).mpr ⟨ne_zero_of_dvd_ne_zero Nat.card_pos.ne' h1, h2⟩

Premises used: Iff.mpr, Nat.two_le_iff, Nat.card_pos, LT.lt.ne', And.intro, ne_zero_of_dvd_ne_zero
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
p : ℕ
hp : (Nat.card G).minFac = p
P : Sylow p G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
subst :
  ∀ {P : Sylow (Nat.card G).minFac G} (hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)),
    (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)

Tactic:
subst hp