Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card (Jordan/PermMaximal.lean)

State before:
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α
Tactic:
by_cases hBne : Set.Nonempty B
State after:
case pos
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α

case neg
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : ¬Set.Nonempty B
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α

State before:
case pos
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α
Tactic:
obtain ⟨m, hm⟩ := ncard_of_block_divides hB hBne
State after:
case pos.intro
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * m
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α

State before:
case pos.intro
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * m
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α
Tactic:
match m with
| 0 =>
  left; left
  simp only [mul_zero, Finite.card_eq_zero_iff] at hm
  exact Set.subsingleton_of_subsingleton
| 1 =>
  left; right
  simp only [mul_one] at hm
  rw [Set.eq_top_iff_ncard, ← hm, Nat.card_eq_fintype_card]
| m + 2 =>
  right
  rw [hm, mul_comm, add_comm, mul_add]
  apply Nat.le_add_right
State after:
no goals

State before:
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 0
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α
Tactic:
left
State after:
case h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 0
⊢ IsTrivialBlock B

State before:
case h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 0
⊢ IsTrivialBlock B
Tactic:
left
State after:
case h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 0
⊢ Set.Subsingleton B

State before:
case h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 0
⊢ Set.Subsingleton B
Tactic:
simp only [mul_zero, Finite.card_eq_zero_iff] at hm
State after:
case h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : IsEmpty α
⊢ Set.Subsingleton B

State before:
case h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : IsEmpty α
⊢ Set.Subsingleton B
Tactic:
exact Set.subsingleton_of_subsingleton
State after:
no goals

State before:
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 1
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α
Tactic:
left
State after:
case h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 1
⊢ IsTrivialBlock B

State before:
case h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 1
⊢ IsTrivialBlock B
Tactic:
right
State after:
case h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 1
⊢ B = ⊤

State before:
case h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B * 1
⊢ B = ⊤
Tactic:
simp only [mul_one] at hm
State after:
case h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B
⊢ B = ⊤

State before:
case h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m : ℕ
hm : Nat.card α = Set.ncard B
⊢ B = ⊤
Tactic:
rw [Set.eq_top_iff_ncard, ← hm, Nat.card_eq_fintype_card]
State after:
no goals

State before:
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m✝ m : ℕ
hm : Nat.card α = Set.ncard B * (m + 2)
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α
Tactic:
right
State after:
case h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m✝ m : ℕ
hm : Nat.card α = Set.ncard B * (m + 2)
⊢ 2 * Set.ncard B ≤ Nat.card α

State before:
case h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m✝ m : ℕ
hm : Nat.card α = Set.ncard B * (m + 2)
⊢ 2 * Set.ncard B ≤ Nat.card α
Tactic:
rw [hm, mul_comm, add_comm, mul_add]
State after:
case h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m✝ m : ℕ
hm : Nat.card α = Set.ncard B * (m + 2)
⊢ Set.ncard B * 2 ≤ Set.ncard B * 2 + Set.ncard B * m

State before:
case h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : Set.Nonempty B
m✝ m : ℕ
hm : Nat.card α = Set.ncard B * (m + 2)
⊢ Set.ncard B * 2 ≤ Set.ncard B * 2 + Set.ncard B * m
Tactic:
apply Nat.le_add_right
State after:
no goals

State before:
case neg
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : ¬Set.Nonempty B
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α
Tactic:
simp only [Set.not_nonempty_iff_eq_empty] at hBne
State after:
case neg
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : B = ∅
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α

State before:
case neg
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : B = ∅
⊢ IsTrivialBlock B ∨ 2 * Set.ncard B ≤ Nat.card α
Tactic:
rw [hBne]
State after:
case neg
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : B = ∅
⊢ IsTrivialBlock ∅ ∨ 2 * Set.ncard ∅ ≤ Nat.card α

State before:
case neg
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : B = ∅
⊢ IsTrivialBlock ∅ ∨ 2 * Set.ncard ∅ ≤ Nat.card α
Tactic:
left
State after:
case neg.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : B = ∅
⊢ IsTrivialBlock ∅

State before:
case neg.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : B = ∅
⊢ IsTrivialBlock ∅
Tactic:
left
State after:
case neg.h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : B = ∅
⊢ Set.Subsingleton ∅

State before:
case neg.h.h
α : Type u_2
inst✝⁶ : DecidableEq α
G✝ : Type ?u.39967
inst✝⁵ : Group G✝
inst✝⁴ : MulAction G✝ α
inst✝³ : Fintype α
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
B : Set α
hB : IsBlock G B
hBne : B = ∅
⊢ Set.Subsingleton ∅
Tactic:
exact Set.subsingleton_empty
State after:
no goals