awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
rw :
  IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔
    IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3))
      (((block_stabilizerOrderIso G a :
            OrderIso.{u_4, u_3} { B : Set X // a ∈ B ∧ IsBlock G B } (↑(Set.Ici (stabilizer G a)) : Type u_3)) :
          (a_1 : { B : Set X // a ∈ B ∧ IsBlock G B }) → (↑(Set.Ici (stabilizer G a)) : Type u_3))
        ⊥)
⊢ IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔ IsCoatom.{u_4} (α := BlockMem G a) ⊥
have rw₁ : IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔
  IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥
Tactic: rw [← OrderIso.isCoatom_iff (block_stabilizerOrderIso G a), OrderIso.map_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h : N.Normal
hNX : fixedPoints.{u_3, u_4} (↥N) α ≠ Set.univ
⊢ IsPretransitive.{u_3, u_4} (↥N) α
have hNX₁ : ∃ (a : α), a ∉ fixedPoints.{u_3, u_4} (↥N) α
Tactic: rw [Set.ne_univ_iff_exists_notMem] at hNX
Cleared hypotheses: hNX
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h : N.Normal
hNX : ∃ (a : α), a ∉ fixedPoints.{u_3, u_4} (↥N) α
⊢ IsPretransitive.{u_3, u_4} (↥N) α
have obtain : ∀ (a : α) (ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α), IsPretransitive.{u_3, u_4} (↥N) α
Tactic: obtain ⟨a, ha⟩ := hNX
Cleared hypotheses: hNX
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
⊢ IsPretransitive.{u_3, u_4} (↥N) α
have rw : orbit.{u_3, u_4} (↥N) a = Set.univ
Tactic: rw [isPretransitive_iff_orbit_eq_univ a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
⊢ orbit.{u_3, u_4} (↥N) a = Set.univ
have apply : ¬(orbit.{u_3, u_4} (↥N) a).Subsingleton
Tactic: apply Or.resolve_left (isTrivialBlock_of_isBlock (IsBlock.orbit_of_normal a))
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
⊢ False
have apply : a ∈ fixedPoints.{u_3, u_4} (↥N) α
Tactic: apply ha
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
this : orbit.{u_3, u_4} (↥N) a = {a}
⊢ Membership.mem (γ := Set α) {a} (n • a)
have rw : n • a ∈ orbit.{u_3, u_4} (↥N) a
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
this : orbit.{u_3, u_4} (↥N) a = {a}
w : ↥N
⊢ n • a ∈ orbit.{u_3, u_4} (↥N) a
have h₁ : (fun (m : ↥N) ↦ m • a) n = n • a
Tactic: use n
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
⊢ Membership.mem (γ := Set α) {a} (n • a)
have suffices : orbit.{u_3, u_4} (↥N) a = {a}
Tactic: suffices orbit N a = {a} by rw [← this]; use n
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
⊢ orbit.{u_3, u_4} (↥N) a = {a}
have h₁ : ∀ (b : α), b ∈ orbit.{u_3, u_4} (↥N) a ↔ Membership.mem (γ := Set α) {a} b
Tactic: ext b
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
b : α
⊢ b ∈ orbit.{u_3, u_4} (↥N) a ↔ Membership.mem (γ := Set α) {a} b
have h₁ : Membership.mem (γ := Set α) {a} b ↔ Membership.mem (γ := Set α) {a} b
Tactic: rw [Set.Subsingleton.eq_singleton_of_mem h (MulAction.mem_orbit_self a)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
⊢ IsPreprimitive G X
have refine : ∀ {B : Set X} (hB : IsBlock G B) (hB' : B.Nontrivial), B = Set.univ
Tactic: refine ⟨fun {B} hB ↦ B.subsingleton_or_nontrivial.imp id fun hB' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
⊢ B = Set.univ
have this : Finite X
Tactic: have : Finite X := (Nat.card_ne_zero.mp hp.ne_zero).2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B = Set.univ
have rw : B.ncard ∣ Nat.card X
Tactic: rw [Set.eq_univ_iff_ncard, eq_comm, ← hp.dvd_iff_eq ((Set.one_lt_ncard).mpr hB').ne']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
⊢ IsPreprimitive H Y
have refine : ∀ {B : Set Y} (hB : IsBlock H B), IsTrivialBlock B
Tactic: refine ⟨fun {B} hB ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
⊢ IsTrivialBlock B
have inl : ∀ (hB' : B = ∅), IsTrivialBlock B
Tactic: rcases B.eq_empty_or_nonempty with hB' | hB'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
inl : ∀ (hB' : B = ∅), IsTrivialBlock B
⊢ IsTrivialBlock B
have inr : ∀ (hB' : B.Nonempty), IsTrivialBlock B
Tactic: rcases B.eq_empty_or_nonempty with hB' | hB'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
⊢ IsTrivialBlock B
have inr : ¬B = Set.univ → B.Subsingleton
Tactic: rw [IsTrivialBlock, or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
⊢ B.Subsingleton
have inr : B.ncard < 2
Tactic: suffices Set.ncard B < 2 by simpa [Nat.lt_succ_iff] using this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
⊢ B.ncard < 2
have apply : B.ncard * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ Nat.card Y
Tactic: apply lt_of_mul_lt_mul_right' (hf'.trans_le' _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
⊢ B.ncard * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ Nat.card Y
have simp : B.ncard * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ B.ncard * (orbit H B).ncard
Tactic: simp only [← hB.ncard_block_mul_ncard_orbit_eq hB']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
⊢ B.ncard * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤
    B.ncard * (orbit H B).ncard
have h : Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ (orbit H B).ncard
Tactic: apply Nat.mul_le_mul_left
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
⊢ Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ (orbit H B).ncard
have h : ∀ (hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)),
  Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ (orbit H B).ncard
Tactic: have hfin := Fintype.ofFinite (Set.range fun g : H ↦ g • B)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
⊢ Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ (orbit H B).ncard
have h : ∑ i : (↑(Set.range fun (g : H) ↦ g • B) : Type u_4),
    (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ (↑i : Set Y)).ncard ≤
  (orbit H B).ncard
Tactic: rw [(hB.isBlockSystem hB').left.ncard_eq_finsum, finsum_eq_sum_of_fintype]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
⊢ ∑ i : (↑(Set.range fun (g : H) ↦ g • B) : Type u_4),
      (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ (↑i : Set Y)).ncard ≤
    (orbit H B).ncard
have h : HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
  (orbit H B).ncard
Tactic: apply le_trans (Finset.sum_le_card_nsmul _ _ 1 _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
h :
  HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
    (orbit H B).ncard
⊢ ∑ i : (↑(Set.range fun (g : H) ↦ g • B) : Type u_4),
      (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ (↑i : Set Y)).ncard ≤
    (orbit H B).ncard
have apply : ∀ (x : (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)),
  Membership.mem (γ := Finset (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ x →
    (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ (↑x : Set Y)).ncard ≤ 1
Tactic: apply le_trans (Finset.sum_le_card_nsmul _ _ 1 _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
⊢ HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
    (orbit H B).ncard
have h : (↑(Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) : ℕ) ≤ (orbit H B).ncard
Tactic: rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
h : (↑(Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) : ℕ) ≤ (orbit H B).ncard
⊢ HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
    (orbit H B).ncard
have h₁ : (↑(Fintype.card.{u_4} (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) : ℕ) ≤ (orbit H B).ncard
Tactic: rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
h : (↑(Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) : ℕ) ≤ (orbit H B).ncard
h₁ : (↑(Fintype.card.{u_4} (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) : ℕ) ≤ (orbit H B).ncard
⊢ HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
    (orbit H B).ncard
have h₂ : (↑(Finset.card.{u_4} (α := Set Y) (Set.toFinset (Set.range fun (g : H) ↦ g • B))) : ℕ) ≤ (orbit H B).ncard
Tactic: rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
h : (↑(Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) : ℕ) ≤ (orbit H B).ncard
h₁ : (↑(Fintype.card.{u_4} (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) : ℕ) ≤ (orbit H B).ncard
h₂ : (↑(Finset.card.{u_4} (α := Set Y) (Set.toFinset (Set.range fun (g : H) ↦ g • B))) : ℕ) ≤ (orbit H B).ncard
⊢ HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
    (orbit H B).ncard
have h₃ : (↑(Set.ncard.{u_4} (α := Set Y) (Set.range fun (g : H) ↦ g • B)) : ℕ) ≤ (orbit H B).ncard
Tactic: rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
h : (↑(Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) : ℕ) ≤ (orbit H B).ncard
h₁ : (↑(Fintype.card.{u_4} (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) : ℕ) ≤ (orbit H B).ncard
h₂ : (↑(Finset.card.{u_4} (α := Set Y) (Set.toFinset (Set.range fun (g : H) ↦ g • B))) : ℕ) ≤ (orbit H B).ncard
h₃ : (↑(Set.ncard.{u_4} (α := Set Y) (Set.range fun (g : H) ↦ g • B)) : ℕ) ≤ (orbit H B).ncard
⊢ HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
    (orbit H B).ncard
have h₄ : (↑(Set.ncard.{u_4} (α := Set Y) (Set.range fun (g : H) ↦ g • B)) : ℕ) ≤
  Set.ncard.{u_4} (α := Set Y) (Set.range fun (m : H) ↦ m • B)
Tactic: rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
h : (↑(Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) : ℕ) ≤ (orbit H B).ncard
h₁ : (↑(Fintype.card.{u_4} (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) : ℕ) ≤ (orbit H B).ncard
h₂ : (↑(Finset.card.{u_4} (α := Set Y) (Set.toFinset (Set.range fun (g : H) ↦ g • B))) : ℕ) ≤ (orbit H B).ncard
h₃ : (↑(Set.ncard.{u_4} (α := Set Y) (Set.range fun (g : H) ↦ g • B)) : ℕ) ≤ (orbit H B).ncard
h₄ :
  (↑(Set.ncard.{u_4} (α := Set Y) (Set.range fun (g : H) ↦ g • B)) : ℕ) ≤
    Set.ncard.{u_4} (α := Set Y) (Set.range fun (m : H) ↦ m • B)
⊢ HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
    (orbit H B).ncard
have h₅ : Set.ncard.{u_4} (α := Set Y) (Set.range fun (g : H) ↦ g • B) ≤
  Set.ncard.{u_4} (α := Set Y) (Set.range fun (g : H) ↦ g • B)
Tactic: rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
⊢ (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩
        (↑(Subtype.mk (p := fun (x : Set Y) ↦ Membership.mem (γ := Set (Set Y)) (Set.range fun (g : H) ↦ g • B) x)
              ((fun (g : H) ↦ g • B) g) ⋯) :
          Set Y)).ncard ≤
    1
have suffices : (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ g • B).Subsingleton
Tactic: suffices Set.Subsingleton (Set.range f ∩ g • B) by simpa