internlm/Lean-Github huggingface dataset:
Theorem: MulAction.is_top_of_large_block
Proof 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'
Proof state after:
no goals
Theorem: MulAction.is_top_of_large_block
Proof 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]
Proof state after:
no goals
Theorem: MulAction.is_top_of_large_block
Proof 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]
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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'
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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'
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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]
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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
Proof state after:
no goals
Theorem: MulAction.is_top_of_large_block
Proof 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]
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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)
Proof state after:
no goals
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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]
Proof 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}
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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'
Proof 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
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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'
Proof 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)
Theorem: MulAction.IsBlock.is_subsingleton
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subset
Proof state before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B
Proof state after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Theorem: MulAction.IsBlock.of_subset
Proof state before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
cases' Set.eq_empty_or_nonempty B with hfB_e hfB_ne
Proof state after:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Theorem: MulAction.IsBlock.of_subset
Proof state before:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by
  intro k hk
  exact Set.biInter_subset_of_mem hk
Proof state after:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)