-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem subsingleton_of_card_lt [Finite X] (hB : IsBlock G B)
    (hB' : Nat.card X < 2 * Set.ncard (orbit G B)) :
    B.Subsingleton

Proof state:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬B.ncard * (orbit G B).ncard ≥ 2 * (orbit G B).ncard
h : B.Nonempty
⊢ ¬2 ≤ B.ncard

Tactic:
exact fun hb ↦ hB' (Nat.mul_le_mul_right _ hb)

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ ∅.Subsingleton

Tactic:
exact Set.subsingleton_empty

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
⊢ B.ncard < 2

Tactic:
cases Set.eq_empty_or_nonempty B with
| inl h => rw [h, Set.ncard_empty]; norm_num
| inr h =>
  rw [← hB.ncard_block_mul_ncard_orbit_eq h, lt_iff_not_ge] at hB'
  rw [← not_le]
  exact fun hb ↦ hB' (Nat.mul_le_mul_right _ hb)

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2

Tactic:
rw [← hB.ncard_block_mul_ncard_orbit_eq h, lt_iff_not_ge] at hB'

Result:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬B.ncard * (orbit G B).ncard ≥ 2 * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2

Proof state:
case inl
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ B.Subsingleton

Tactic:
rw [h]

Result:
case inl
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ ∅.Subsingleton

Proof state:
case inl
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ B.ncard < 2

Tactic:
rw [h, Set.ncard_empty]

Result:
case inl
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ 0 < 2

Proof state:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : ∃ a, B = {a}
⊢ B.Subsingleton

Tactic:
obtain ⟨a, ha⟩ := h

Result:
case inr.intro
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
a : X
ha : B = {a}
⊢ B.Subsingleton

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
⊢ B.Subsingleton

Tactic:
suffices Set.ncard B < 2 by
  rw [Nat.lt_succ_iff, Set.ncard_le_one_iff_eq] at this
  cases this with
  | inl h => rw [h]; exact Set.subsingleton_empty
  | inr h =>
    obtain ⟨a, ha⟩ := h; rw [ha]; exact Set.subsingleton_singleton

Result:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
⊢ B.ncard < 2

Proof state:
case inr.intro
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
a : X
ha : B = {a}
⊢ {a}.Subsingleton

Tactic:
exact Set.subsingleton_singleton

Result:
no goals

Proof state:
case inr.intro
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
a : X
ha : B = {a}
⊢ B.Subsingleton

Tactic:
rw [ha]

Result:
case inr.intro
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
a : X
ha : B = {a}
⊢ {a}.Subsingleton

Proof state:
case inl
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
this : B = ∅ ∨ ∃ a, B = {a}
⊢ B.Subsingleton

Tactic:
cases this with
| inl h => rw [h]; exact Set.subsingleton_empty
| inr h =>
  obtain ⟨a, ha⟩ := h; rw [ha]; exact Set.subsingleton_singleton

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬B.ncard * (orbit G B).ncard ≥ 2 * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2

Tactic:
rw [← not_le]

Result:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬B.ncard * (orbit G B).ncard ≥ 2 * (orbit G B).ncard
h : B.Nonempty
⊢ ¬2 ≤ B.ncard

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
this : B.ncard < 2
⊢ B.Subsingleton

Tactic:
rw [Nat.lt_succ_iff, Set.ncard_le_one_iff_eq] at this

Result:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
this : B = ∅ ∨ ∃ a, B = {a}
⊢ B.Subsingleton