Theorem: MulAction.IsBlock.is_subsingleton (Jordan/Blocks.lean)

State before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
⊢ Set.Subsingleton B
Tactic:
have := Fintype.ofFinite X
State after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
⊢ Set.Subsingleton B

State before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
⊢ Set.Subsingleton B
Tactic:
suffices Set.ncard B ≤ 1 by
  rw [Set.ncard_le_one_iff_eq] at this
  cases' this with h h
  rw [h]; exact Set.subsingleton_empty
  obtain ⟨a, ha⟩ := h; rw [ha]; exact Set.subsingleton_singleton
State after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
⊢ Set.ncard B ≤ 1

State before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this✝ : Fintype X
this : Set.ncard B ≤ 1
⊢ Set.Subsingleton B
Tactic:
rw [Set.ncard_le_one_iff_eq] at this
State after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this✝ : Fintype X
this : B = ∅ ∨ ∃ a, B = {a}
⊢ Set.Subsingleton B

State before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this✝ : Fintype X
this : B = ∅ ∨ ∃ a, B = {a}
⊢ Set.Subsingleton B
Tactic:
cases' this with h h
State after:
case inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : B = ∅
⊢ Set.Subsingleton B

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

State before:
case inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : B = ∅
⊢ Set.Subsingleton B

case inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : ∃ a, B = {a}
⊢ Set.Subsingleton B
Tactic:
rw [h]
State after:
case inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : B = ∅
⊢ Set.Subsingleton ∅

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

State before:
case inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : B = ∅
⊢ Set.Subsingleton ∅

case inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : ∃ a, B = {a}
⊢ Set.Subsingleton B
Tactic:
exact Set.subsingleton_empty
State after:
case inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : ∃ a, B = {a}
⊢ Set.Subsingleton B

State before:
case inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : ∃ a, B = {a}
⊢ Set.Subsingleton B
Tactic:
obtain ⟨a, ha⟩ := h
State after:
case inr.intro
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
a : X
ha : B = {a}
⊢ Set.Subsingleton B

State before:
case inr.intro
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
a : X
ha : B = {a}
⊢ Set.Subsingleton B
Tactic:
rw [ha]
State after:
case inr.intro
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
a : X
ha : B = {a}
⊢ Set.Subsingleton {a}

State before:
case inr.intro
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
a : X
ha : B = {a}
⊢ Set.Subsingleton {a}
Tactic:
exact Set.subsingleton_singleton
State after:
no goals

State before:
case inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : B = ∅
⊢ Set.ncard B ≤ 1
Tactic:
rw [h, Set.ncard_empty]
State after:
case inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : B = ∅
⊢ 0 ≤ 1

State before:
case inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : B = ∅
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
case inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
⊢ Set.ncard B ≤ 1
Tactic:
let hk := ncard_block_mul_ncard_orbit_eq hB h
State after:
case inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
⊢ Set.ncard B ≤ 1

State before:
case inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
⊢ Set.ncard B ≤ 1
Tactic:
cases' Nat.lt_or_ge (Set.ncard B) 2 with hb hb
State after:
case inr.inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B < 2
⊢ Set.ncard B ≤ 1

case inr.inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B ≥ 2
⊢ Set.ncard B ≤ 1

State before:
case inr.inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B < 2
⊢ Set.ncard B ≤ 1
Tactic:
rw [← Nat.lt_succ_iff]
State after:
case inr.inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B < 2
⊢ Set.ncard B < Nat.succ 1

State before:
case inr.inl
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B < 2
⊢ Set.ncard B < Nat.succ 1
Tactic:
exact hb
State after:
no goals

State before:
case inr.inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B ≥ 2
⊢ Set.ncard B ≤ 1
Tactic:
exfalso
State after:
case inr.inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B ≥ 2
⊢ False

State before:
case inr.inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B ≥ 2
⊢ False
Tactic:
rw [← hk, lt_iff_not_ge] at hB'
State after:
case inr.inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : ¬Set.ncard B * Set.ncard (Set.range fun g => g • B) ≥ 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B ≥ 2
⊢ False

State before:
case inr.inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : ¬Set.ncard B * Set.ncard (Set.range fun g => g • B) ≥ 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B ≥ 2
⊢ False
Tactic:
apply hB'
State after:
case inr.inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : ¬Set.ncard B * Set.ncard (Set.range fun g => g • B) ≥ 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B ≥ 2
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) ≥ 2 * Set.ncard (Set.range fun g => g • B)

State before:
case inr.inr
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : ¬Set.ncard B * Set.ncard (Set.range fun g => g • B) ≥ 2 * Set.ncard (Set.range fun g => g • B)
this : Fintype X
h : Set.Nonempty B
hk : Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X := ncard_block_mul_ncard_orbit_eq hB h
hb : Set.ncard B ≥ 2
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) ≥ 2 * Set.ncard (Set.range fun g => g • B)
Tactic:
refine' Nat.mul_le_mul_right _ hb
State after:
no goals