Theorem: MulAction.is_top_of_large_block (Jordan/Blocks.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
⊢ B = ⊤
Tactic:
letI := Fintype.ofFinite X
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
⊢ B = ⊤

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
⊢ B = ⊤
Tactic:
cases' Set.eq_empty_or_nonempty B with hB_e hB_ne
State after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_e : B = ∅
⊢ B = ⊤

case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
⊢ B = ⊤

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
⊢ B = ⊤
Tactic:
rw [Set.top_eq_univ, ← Set.toFinset_inj, Set.toFinset_univ, ← Finset.card_eq_iff_eq_univ, ← Set.ncard_eq_toFinset_card']
State after:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
⊢ Set.ncard B = Fintype.card X

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
⊢ Set.ncard B = Fintype.card X
Tactic:
obtain ⟨k, h⟩ := ncard_of_block_divides hB hB_ne
State after:
case inr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
h : Nat.card X = Set.ncard B * k
⊢ Set.ncard B = Fintype.card X

State before:
case inr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
h : Nat.card X = Set.ncard B * k
⊢ Set.ncard B = Fintype.card X
Tactic:
simp only [← Nat.card_eq_fintype_card]
State after:
case inr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
h : Nat.card X = Set.ncard B * k
⊢ Set.ncard B = Nat.card X

State before:
case inr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
h : Nat.card X = Set.ncard B * k
⊢ Set.ncard B = Nat.card X
Tactic:
rw [h] at hB' ⊢
State after:
case inr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ Set.ncard B = Set.ncard B * k

State before:
case inr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ Set.ncard B = Set.ncard B * k
Tactic:
suffices k = 1 by
  simp only [this, mul_one]
State after:
case inr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ k = 1

State before:
case inr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ k = 1
Tactic:
apply le_antisymm
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ k ≤ 1

case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ 1 ≤ k

State before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_e : B = ∅
⊢ B = ⊤
Tactic:
exfalso
State after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_e : B = ∅
⊢ False

State before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard B
this : Fintype X := Fintype.ofFinite X
hB_e : B = ∅
⊢ False
Tactic:
rw [hB_e] at hB'
State after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard ∅
this : Fintype X := Fintype.ofFinite X
hB_e : B = ∅
⊢ False

State before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB' : Nat.card X < 2 * Set.ncard ∅
this : Fintype X := Fintype.ofFinite X
hB_e : B = ∅
⊢ False
Tactic:
simp only [Set.ncard_empty, mul_zero, gt_iff_lt, not_lt_zero'] at hB'
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this✝ : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
this : k = 1
⊢ Set.ncard B = Set.ncard B * k
Tactic:
simp only [this, mul_one]
State after:
no goals

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ k ≤ 1
Tactic:
rw [← not_lt, ← Nat.succ_le_iff]
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ ¬Nat.succ 1 ≤ k

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ ¬Nat.succ 1 ≤ k
Tactic:
intro hk
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
hk : Nat.succ 1 ≤ k
⊢ False

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
hk : Nat.succ 1 ≤ k
⊢ False
Tactic:
rw [← not_le] at hB'
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : ¬2 * Set.ncard B ≤ Set.ncard B * k
h : Nat.card X = Set.ncard B * k
hk : Nat.succ 1 ≤ k
⊢ False

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : ¬2 * Set.ncard B ≤ Set.ncard B * k
h : Nat.card X = Set.ncard B * k
hk : Nat.succ 1 ≤ k
⊢ False
Tactic:
apply hB'
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : ¬2 * Set.ncard B ≤ Set.ncard B * k
h : Nat.card X = Set.ncard B * k
hk : Nat.succ 1 ≤ k
⊢ 2 * Set.ncard B ≤ Set.ncard B * k

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : ¬2 * Set.ncard B ≤ Set.ncard B * k
h : Nat.card X = Set.ncard B * k
hk : Nat.succ 1 ≤ k
⊢ 2 * Set.ncard B ≤ Set.ncard B * k
Tactic:
rw [mul_comm]
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : ¬2 * Set.ncard B ≤ Set.ncard B * k
h : Nat.card X = Set.ncard B * k
hk : Nat.succ 1 ≤ k
⊢ Set.ncard B * 2 ≤ Set.ncard B * k

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : ¬2 * Set.ncard B ≤ Set.ncard B * k
h : Nat.card X = Set.ncard B * k
hk : Nat.succ 1 ≤ k
⊢ Set.ncard B * 2 ≤ Set.ncard B * k
Tactic:
apply Nat.mul_le_mul_left _ hk
State after:
no goals

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ 1 ≤ k
Tactic:
rw [← not_lt, Nat.lt_one_iff]
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ ¬k = 0

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
⊢ ¬k = 0
Tactic:
intro hk
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
hk : k = 0
⊢ False

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
h : Nat.card X = Set.ncard B * k
hk : k = 0
⊢ False
Tactic:
simp only [Nat.card_eq_fintype_card, hk, mul_zero, Fintype.card_eq_zero_iff, ← not_nonempty_iff] at h
State after:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
hk : k = 0
h : ¬Nonempty X
⊢ False

State before:
case inr.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hfX : Finite X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
this : Fintype X := Fintype.ofFinite X
hB_ne : Set.Nonempty B
k : ℕ
hB' : Set.ncard B * k < 2 * Set.ncard B
hk : k = 0
h : ¬Nonempty X
⊢ False
Tactic:
exact h (Set.Nonempty.to_type hB_ne)
State after:
no goals