internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
⊢ Fintype.card (Perm α) = 2
Tactic:
rw [Fintype.card_perm, ← Nat.card_eq_fintype_card, hα]
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
⊢ Nat.factorial 2 = 2
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
⊢ Nat.factorial 2 = 2
Tactic:
simp
Proof state after:
no goals
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr.inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊥
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
exfalso
Proof state after:
case inr.inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊥
⊢ False
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr.inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊥
⊢ False
Tactic:
exact ne_bot_of_gt hG h
Proof state after:
no goals
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
rw [h]
Proof state after:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ ⊤
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ ⊤
Tactic:
rw [← stabilizer_univ_eq_top (Equiv.Perm α) α]
Proof state after:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) _root_.Set.univ
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) _root_.Set.univ
Tactic:
apply this
Proof state after:
case inr.inr.inr.x
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ 1 < Set.ncard _root_.Set.univ
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr.inr.inr.x
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ 1 < Set.ncard _root_.Set.univ
Tactic:
rw [Set.ncard_univ, hα]
Proof state after:
case inr.inr.inr.x
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ 1 < 2
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr.inr.inr.x
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Equiv.Perm.Subtype.image_preimage_of_val
Proof state before:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
⊢ Subtype.val '' (Subtype.val ⁻¹' B) = B
Tactic:
apply Set.Subset.antisymm (Set.image_preimage_subset Subtype.val B)
Proof state after:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
⊢ B ⊆ Subtype.val '' (Subtype.val ⁻¹' B)
Theorem: Equiv.Perm.Subtype.image_preimage_of_val
Proof state before:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
⊢ B ⊆ Subtype.val '' (Subtype.val ⁻¹' B)
Tactic:
intro x hx
Proof state after:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
x : α
hx : x ∈ B
⊢ x ∈ Subtype.val '' (Subtype.val ⁻¹' B)
Theorem: Equiv.Perm.Subtype.image_preimage_of_val
Proof state before:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
x : α
hx : x ∈ B
⊢ x ∈ Subtype.val '' (Subtype.val ⁻¹' B)
Tactic:
use ⟨x, h hx⟩
Proof state after:
case h
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
x : α
hx : x ∈ B
⊢ { val := x, property := ⋯ } ∈ Subtype.val ⁻¹' B ∧ ↑{ val := x, property := ⋯ } = x
Theorem: Equiv.Perm.Subtype.image_preimage_of_val
Proof state before:
case h
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
x : α
hx : x ∈ B
⊢ { val := x, property := ⋯ } ∈ Subtype.val ⁻¹' B ∧ ↑{ val := x, property := ⋯ } = x
Tactic:
simp only [hx, Set.mem_preimage, Subtype.coe_mk, eq_self_iff_true, and_self_iff]
Proof state after:
no goals
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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 α
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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 α
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof state after:
no goals
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof state after:
no goals
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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 = ⊤
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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 = ⊤
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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]
Proof state after:
no goals
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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 α
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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]
Proof 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
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof state after:
no goals
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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 α
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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]
Proof 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 α
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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 ∅
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof 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 ∅
Theorem: MulAction.isTrivialBlock_or_2_mul_ncard_le_card
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.45087
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
constructor
Proof state after:
case out
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.45087
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsCoatom (stabilizer (Perm α) s)
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case out
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.45087
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsCoatom (stabilizer (Perm α) s)
Tactic:
constructor
Proof state after:
case out.left
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.45087
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
⊢ stabilizer (Perm α) s ≠ ⊤

case out.right
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.45087
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
⊢ ∀ (b : Subgroup (Perm α)), stabilizer (Perm α) s < b → b = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case out.left
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.45087
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
⊢ stabilizer (Perm α) s ≠ ⊤

case out.right
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.45087
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
⊢ ∀ (b : Subgroup (Perm α)), stabilizer (Perm α) s < b → b = ⊤
Tactic:
exact stabilizer_ne_top s h0 h1
Proof state after:
case out.right
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.45087
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
⊢ ∀ (b : Subgroup (Perm α)), stabilizer (Perm α) s < b → b = ⊤