awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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 :
  Function.Injective (α := ↥(↑P : Subgroup G)) (β := ↥(↑P : Subgroup G))
      (⇑((transferSylow P hP).restrict (↑P : Subgroup G)) : (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G)) ∧
    map (transferSylow P hP) (↑P : Subgroup G) = ⊤
⊢ (transferSylow P hP).ker.IsComplement' (↑P : Subgroup G)
have this : Function.Surjective (α := G) (β := ↥(↑P : Subgroup G)) (⇑(transferSylow P hP) : (a : G) → ↥(↑P : Subgroup G))
Tactic: have := range_eq_top.mp (top_le_iff.mp (hf.2.ge.trans
    (map_le_range (transferSylow P hP) P)))
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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 :
  Function.Injective (α := ↥(↑P : Subgroup G)) (β := ↥(↑P : Subgroup G))
      (⇑((transferSylow P hP).restrict (↑P : Subgroup G)) : (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G)) ∧
    map (transferSylow P hP) (↑P : Subgroup G) = ⊤
this : Function.Surjective (α := G) (β := ↥(↑P : Subgroup G)) (⇑(transferSylow P hP) : (a : G) → ↥(↑P : Subgroup G))
⊢ (transferSylow P hP).ker.IsComplement' (↑P : Subgroup G)
have hf₁ : (transferSylow P hP).ker ⊓ (↑P : Subgroup G) = ⊥ ∧
  (↑(transferSylow P hP).ker : Set G) * (↑(↑P : Subgroup G) : Set G) = Set.univ
Tactic: rw [← (comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, SetLike.ext'_iff,
    normal_mul, ← ker_eq_bot_iff, ← map_subtype_inj,
    ker_restrict, subgroupOf_map_subtype, Subgroup.map_bot, coe_top] at hf
Cleared hypotheses: hf, this
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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)
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
have 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))
Tactic: subst hp
Cleared hypotheses: p, hp, P, hP
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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)
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
have pos : ∀ (hn : Nat.card G = 1), LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
Tactic: by_cases hn : Nat.card G = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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))
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
have neg : ∀ (hn : ¬Nat.card G = 1), LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
Tactic: by_cases hn : Nat.card G = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
have this : Subsingleton G
Tactic: have := (Nat.card_eq_one_iff_unique.mp hn).1
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
have pos : LE.le (α := Subgroup G) (centralizer (↑P : Set G)) (centralizer (↑P : Set G))
Tactic: rw [Subsingleton.elim (normalizer _) (centralizer P)]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
have this : Fact (Nat.Prime (Nat.card G).minFac)
Tactic: have := Fact.mk (Nat.minFac_prime hn)
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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)
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
have key : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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))
⊢ LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
have key₁ : 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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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))
have neg : (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
Tactic: refine relIndex_eq_one.mp (Nat.eq_one_of_dvd_coprimes ?_ dvd_rfl key)
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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))
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
have 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)))
Tactic: obtain ⟨k, hk⟩ := P.2.exists_card_eq
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
have neg : ∀ (h0 : k = 0),
  (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
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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)))
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
have neg₁ : ∀ (h0 : 0 < k),
  (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
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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 (Nat.card.{u_3} (MulAut ↥(↑P : Subgroup G)))
have neg : (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime 1
Tactic: rw [hP.card_mulAut, hk, h0, pow_zero, Nat.totient_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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.{u_3} (MulAut ↥(↑P : Subgroup G)))
have neg : (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime
  ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))
Tactic: rw [hP.card_mulAut, hk, Nat.totient_prime_pow Fact.out h0]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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))
have neg : (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime (Nat.card G).minFac
Tactic: refine (Nat.Coprime.pow_right _ ?_).mul_right ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime
    ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))
have neg₁ : (relIndex (centralizer (↑P : Set G)) (normalizer (↑P : Set G))).Coprime ((Nat.card G).minFac - 1)
Tactic: refine (Nat.Coprime.pow_right _ ?_).mul_right ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
have neg : ((↑P : Subgroup G).relIndex (normalizer (↑P : Set G))).Coprime (Nat.card G).minFac
Tactic: apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_of_le_left _ P.le_centralizer)
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ ((↑P : Subgroup G).relIndex (normalizer (↑P : Set G))).Coprime (Nat.card G).minFac
have neg : (↑P : Subgroup G).index.Coprime (Nat.card G).minFac
Tactic: apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_index_of_le P.le_normalizer)
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ (↑P : Subgroup G).index.Coprime (Nat.card G).minFac
have neg : ¬(Nat.card G).minFac ∣ (↑P : Subgroup G).index
Tactic: rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd Fact.out]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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 - 1)
have neg : (Nat.card.{u_3} ↥(normalizer (↑P : Set G))).Coprime ((Nat.card G).minFac - 1)
Tactic: apply Nat.Coprime.coprime_dvd_left <| relIndex_dvd_card ..
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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.{u_3} ↥(normalizer (↑P : Set G))).Coprime ((Nat.card G).minFac - 1)
have neg : (Nat.card G).Coprime ((Nat.card G).minFac - 1)
Tactic: apply Nat.Coprime.coprime_dvd_left <| card_subgroup_dvd_card _
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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).Coprime ((Nat.card G).minFac - 1)
have h1 : (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)
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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).Coprime ((Nat.card G).minFac - 1)
have h2 : (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)
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ (Nat.card G).Coprime ((Nat.card G).minFac - 1)
have 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)
Tactic: contrapose! h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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)
have neg : 2 ≤ (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)
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
have subst : ∀ {P : Sylow (Nat.card G).minFac G} (hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)),
  (MonoidHom.transferSylow P sorry).ker.IsComplement' (↑P : Subgroup G)
Tactic: subst hp
Cleared hypotheses: p, hp, P, hP
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
have pos : ∀ (hn : Nat.card G = 1), (MonoidHom.transferSylow P sorry).ker.IsComplement' (↑P : Subgroup G)
Tactic: by_cases hn : Nat.card G = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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), (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
have neg : ∀ (hn : ¬Nat.card G = 1), (MonoidHom.transferSylow P sorry).ker.IsComplement' (↑P : Subgroup G)
Tactic: by_cases hn : Nat.card G = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
have this : Subsingleton G
Tactic: have := (Nat.card_eq_one_iff_unique.mp hn).1
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
have pos : IsComplement'.{u_3} (G := G) ⊥ ⊤
Tactic: rw [Subsingleton.elim (MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)).ker ⊥,
      Subsingleton.elim P.1 ⊤]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (hypothesis)
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
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
have this : Fact (Nat.Prime (Nat.card G).minFac)
Tactic: have := Fact.mk (Nat.minFac_prime hn)
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.UniquelyDecodable (goal)
Goal:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }
hflat :
  Eq.{u_1 + 1} (α := List α)
    ((fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) ↦ (↑L : List (List α)).flatten) L₁)
    ((fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) ↦ (↑L : List (List α)).flatten) L₂)
⊢ L₁ = L₂
have a : (↑L₁ : List (List α)) = (↑L₂ : List (List α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ hammingDist (β := β) x x = 0
have rw : ∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ x x_1
Tactic: rw [hammingDist, card_eq_zero, filter_eq_empty_iff]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ card.{u_2} (α := ι) {i : ι | x i ≠ z i} ≤
    card.{u_2} (α := ι) {i : ι | x i ≠ y i} + card.{u_2} (α := ι) {i : ι | y i ≠ z i}
have refine : LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} ({i : ι | x i ≠ y i} ∪ {i : ι | y i ≠ z i})
Tactic: refine le_trans (card_mono ?_) (card_union_le _ _)
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} ({i : ι | x i ≠ y i} ∪ {i : ι | y i ≠ z i})
have rw : LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} {a : ι | x a ≠ y a ∨ y a ≠ z a}
Tactic: rw [← filter_or]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist (β := β) x z ≤ hammingDist (β := β) x y + hammingDist (β := β) y z
have unfold : card.{u_2} (α := ι) {i : ι | x i ≠ z i} ≤
  card.{u_2} (α := ι) {i : ι | x i ≠ y i} + card.{u_2} (α := ι) {i : ι | y i ≠ z i}
Tactic: classical
    unfold hammingDist
    refine le_trans (card_mono ?_) (card_union_le _ _)
    rw [← filter_or]
    exact monotone_filter_right _ fun i _ h ↦ (h.ne_or_ne _).imp_right Ne.symm