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

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
hX : Finite X
hB : IsBlock G B
hB' : (orbit G B).ncard < 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B = Set.univ

Tactic:
interval_cases (orbit G B).ncard

Result:
case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : B.ncard * 0 = Nat.card X
⊢ B = Set.univ

case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard * 1 = Nat.card X
⊢ B = Set.univ

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
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B = Set.univ

Tactic:
rw [← key, mul_lt_mul_iff_of_pos_left (by rwa [Set.ncard_pos])] 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
hX : Finite X
hB : IsBlock G B
hB' : (orbit G B).ncard < 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B = Set.univ

Proof state:
case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : IsEmpty X
⊢ B = Set.univ

Tactic:
exact (IsEmpty.exists_iff.mp hB_ne).elim

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
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
hB_ne : B.Nonempty
⊢ B = Set.univ

Tactic:
have key := hB.ncard_block_mul_ncard_orbit_eq hB_ne

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
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B = Set.univ

Proof state:
case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard * 1 = Nat.card X
⊢ B = Set.univ

Tactic:
rw [mul_one, ← Set.ncard_univ] at key

Result:
case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard = Set.univ.ncard
⊢ B = Set.univ

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

Tactic:
rwa [Set.ncard_pos]

Result:
no goals

Proof state:
case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : B.ncard * 0 = Nat.card X
⊢ B = Set.univ

Tactic:
rw [mul_zero, eq_comm, Nat.card_eq_zero, or_iff_left hX.not_infinite] at key

Result:
case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : IsEmpty X
⊢ B = Set.univ

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

Tactic:
simp only [Set.ncard_empty, zero_mul, not_lt_zero'] at hB'

Result:
no goals

Proof state:
case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard = Set.univ.ncard
⊢ B = Set.univ

Tactic:
rw [Set.eq_of_subset_of_ncard_le (Set.subset_univ B) key.ge]

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
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
⊢ B = Set.univ

Tactic:
rcases Set.eq_empty_or_nonempty B with rfl | hB_ne

Result:
case inl
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
hX : Finite X
hB : IsBlock G ∅
hB' : Nat.card X < ∅.ncard * 2
⊢ ∅ = Set.univ

case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
hB_ne : B.Nonempty
⊢ B = Set.univ