awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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

Tactic:
⟨fun {B} hB ↦ B.subsingleton_or_nontrivial.imp id fun hB' ↦ ?_⟩

Premises used: Set.subsingleton_or_nontrivial, id, Or.imp, MulAction.IsPreprimitive.mk
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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)
refine : ∀ {B : Set X} (hB : IsBlock G B) (hB' : B.Nontrivial), B = Set.univ
⊢ IsPreprimitive G X

Tactic:
refine ⟨fun {B} hB ↦ B.subsingleton_or_nontrivial.imp id fun hB' ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
⊢ Finite X

Tactic:
have : Finite X := (Nat.card_ne_zero.mp hp.ne_zero).2
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
rw : B.ncard ∣ Nat.card X
⊢ B = Set.univ

Tactic:
rw [Set.eq_univ_iff_ncard, eq_comm, ← hp.dvd_iff_eq ((Set.one_lt_ncard).mpr hB').ne']

Premises used: Iff.mpr, Set.one_lt_ncard, Nat.Prime.dvd_iff_eq, eq_comm, LT.lt.ne', Set.eq_univ_iff_ncard
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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.ncard ∣ Nat.card X

Tactic:
hB.ncard_dvd_card hB'.nonempty

Premises used: MulAction.IsBlock.ncard_dvd_card, Set.Nontrivial.nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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.ncard ∣ Nat.card X

Tactic:
exact hB.ncard_dvd_card hB'.nonempty

Premises used: MulAction.IsBlock.ncard_dvd_card, Set.Nontrivial.nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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

Tactic:
⟨fun {B} hB ↦ ?_⟩

Premises used: MulAction.IsPreprimitive.mk
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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))
refine : ∀ {B : Set Y} (hB : IsBlock H B), IsTrivialBlock B
⊢ IsPreprimitive H Y

Tactic:
refine ⟨fun {B} hB ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
inr : ∀ (hB' : B.Nonempty), IsTrivialBlock B
⊢ IsTrivialBlock B

Tactic:
rcases B.eq_empty_or_nonempty with hB' | hB'

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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 = ∅
⊢ IsTrivialBlock B

Tactic:
simp [IsTrivialBlock, hB']

Premises used: MulAction.IsTrivialBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
inr : ¬B = Set.univ → B.Subsingleton
⊢ IsTrivialBlock B

Tactic:
rw [IsTrivialBlock, or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right, MulAction.IsTrivialBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
this : B.ncard < 2
⊢ B.Subsingleton

Tactic:
simpa [Nat.lt_succ_iff] using this

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
inr : B.ncard < 2
⊢ B.Subsingleton

Tactic:
suffices Set.ncard B < 2 by simpa [Nat.lt_succ_iff] using this
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
apply : B.ncard * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ Nat.card Y
⊢ B.ncard < 2

Tactic:
apply lt_of_mul_lt_mul_right' (hf'.trans_le' _)

Premises used: lt_of_mul_lt_mul_right', LT.lt.trans_le'
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
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
⊢ B.ncard * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ Nat.card Y

Tactic:
simp only [← hB.ncard_block_mul_ncard_orbit_eq hB']

Premises used: MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
h : Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ (orbit H B).ncard
⊢ 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:
apply Nat.mul_le_mul_left

Premises used: Nat.mul_le_mul_left
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
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
⊢ 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)
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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 :
  ∑ 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
⊢ Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ (orbit H B).ncard

Tactic:
rw [(hB.isBlockSystem hB').left.ncard_eq_finsum, finsum_eq_sum_of_fintype]

Premises used: Setoid.IsPartition.ncard_eq_finsum, MulAction.IsBlock.isBlockSystem, finsum_eq_sum_of_fintype, And.left
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
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
⊢ ∑ 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:
apply le_trans (Finset.sum_le_card_nsmul _ _ 1 _)

Premises used: Finset.sum_le_card_nsmul, OfNat.ofNat, le_trans
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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)
h₅ 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)
⊢ HSMul.hSMul (β := ℕ) (Finset.card.{u_4} (α := (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)) Finset.univ) 1 ≤
    (orbit H B).ncard

Tactic:
rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]

Premises used: Finset.card_univ, Nat.cast_id, Set.toFinset_card, Set.ncard_eq_toFinset_card', MulAction.orbit, nsmul_one
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
this : (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ g • B).Subsingleton
⊢ (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

Tactic:
simpa
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
suffices : (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ g • B).Subsingleton
⊢ (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

Tactic:
suffices Set.Subsingleton (Set.range f ∩ g • B) by simpa
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
rw : Set.Subsingleton.{u_4} (α := Y) (Set.image.{u_2, u_4} (α := X) (⇑f : (a : X) → Y) ((⇑f : (a : X) → Y) ⁻¹' (g • B)))
⊢ (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ g • B).Subsingleton

Tactic:
rw [← Set.image_preimage_eq_range_inter]

Premises used: Set.image_preimage_eq_range_inter
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
hs : Set.Subsingleton.{u_2} (α := X) ((⇑f : (a : X) → Y) ⁻¹' (g • B))
⊢ Set.Subsingleton.{u_4} (α := Y) (Set.image.{u_2, u_4} (α := X) (⇑f : (a : X) → Y) ((⇑f : (a : X) → Y) ⁻¹' (g • B)))

Tactic:
apply Set.Subsingleton.image

Premises used: Set.Subsingleton.image
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
hs : ¬Eq.{u_2 + 1} (α := Set X) ((⇑f : (a : X) → Y) ⁻¹' (g • B)) Set.univ
⊢ Set.Subsingleton.{u_2} (α := X) ((⇑f : (a : X) → Y) ⁻¹' (g • B))

Tactic:
apply Or.resolve_right (isTrivialBlock_of_isBlock ((hB.translate g).preimage f))

Premises used: MulAction.IsBlock.preimage, MulAction.IsBlock.translate, MulAction.IsPreprimitive.isTrivialBlock_of_isBlock, Or.resolve_right
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
h : Eq.{u_2 + 1} (α := Set X) ((⇑f : (a : X) → Y) ⁻¹' (g • B)) Set.univ
⊢ Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B

Tactic:
simp only [Set.preimage_eq_univ_iff] at h

Premises used: Set.preimage_eq_univ_iff
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
hs : B = Set.univ
⊢ False

Tactic:
apply hB_ne_top
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
hs : Nat.card Y < B.ncard * 2
⊢ B = Set.univ

Tactic:
apply hB.eq_univ_of_card_lt

Premises used: MulAction.IsBlock.eq_univ_of_card_lt
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
hs : 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ B.ncard * 2
⊢ Nat.card Y < B.ncard * 2

Tactic:
apply lt_of_lt_of_le hf'

Premises used: lt_of_lt_of_le
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
hs : Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ B.ncard
⊢ 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ B.ncard * 2

Tactic:
rw [mul_comm, mul_le_mul_iff_left₀ Nat.succ_pos']

Premises used: Nat.succ_pos', mul_comm, mul_le_mul_iff_left₀
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
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
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
⊢ Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ B.ncard

Tactic:
apply le_trans (Set.ncard_le_ncard h) (Set.ncard_image_le B.toFinite)

Premises used: Set.ncard_image_le, Set.toFinite, Set.ncard_le_ncard, le_trans
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
this : b ∉ B
⊢ ¬∀ (i : G), Membership.mem (γ := Set X) (⋂ (_ : a ∈ i • A), i • A) b

Tactic:
rw [Set.mem_iInter] at this

Premises used: Set.mem_iInter
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
this : ¬∀ (i : G), Membership.mem (γ := Set X) (⋂ (_ : a ∈ i • A), i • A) b
⊢ ∃ (g : G), a ∈ g • A ∧ b ∉ g • A

Tactic:
simpa only [Set.mem_iInter, not_forall, exists_prop] using this

Premises used: exists_prop, Set.mem_iInter, Classical.not_forall
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
suffices : b ∉ B
⊢ ∃ (g : G), a ∈ g • A ∧ b ∉ g • A

Tactic:
suffices b ∉ B by
    rw [Set.mem_iInter] at this
    simpa only [Set.mem_iInter, not_forall, exists_prop] using this
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
rw : b ∉ {a}
⊢ b ∉ B

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ ¬b = a

Tactic:
Ne.symm h

Premises used: Ne.symm
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ ¬b = a

Tactic:
exact Ne.symm h

Premises used: Ne.symm