internlm/Lean-Github huggingface dataset:
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
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_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = Finset.univ.card • ?m.191918

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_ne : Set.Nonempty B
this : Fintype X
⊢ ℕ

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = ?m.191918
Tactic:
rw [mul_comm]
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_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard (Set.range fun g => g • B) * Set.ncard B = Finset.univ.card • ?m.191918

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_ne : Set.Nonempty B
this : Fintype X
⊢ ℕ

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_ne : Set.Nonempty B
this : Fintype X
⊢ ℕ

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = ?m.191918
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
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_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard (Set.range fun g => g • B) * Set.ncard B = Finset.univ.card • ?m.191918

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_ne : Set.Nonempty B
this : Fintype X
⊢ ℕ

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_ne : Set.Nonempty B
this : Fintype X
⊢ ℕ

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = ?m.191918
Tactic:
congr
Proof state after:
case e_a
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_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard (Set.range fun g => g • B) = Finset.univ.card

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = Set.ncard B
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a
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_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard (Set.range fun g => g • B) = Finset.univ.card

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = Set.ncard B
Tactic:
rw [Set.ncard_eq_toFinset_card']
Proof state after:
case e_a
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_ne : Set.Nonempty B
this : Fintype X
⊢ (Set.toFinset (Set.range fun g => g • B)).card = Finset.univ.card

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = Set.ncard B
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a
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_ne : Set.Nonempty B
this : Fintype X
⊢ (Set.toFinset (Set.range fun g => g • B)).card = Finset.univ.card

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = Set.ncard B
Tactic:
rw [Finset.card_congr]
Proof state after:
case e_a.f
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_ne : Set.Nonempty B
this : Fintype X
⊢ (a : Set X) → a ∈ Set.toFinset (Set.range fun g => g • B) → ↑(Set.range fun g => g • B)

case e_a.h₁
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ (a : Set X) (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), ?e_a.f✝ a ha ∈ Finset.univ

case e_a.h₂
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ (a b : Set X) (ha : a ∈ Set.toFinset (Set.range fun g => g • B)) (hb : b ∈ Set.toFinset (Set.range fun g => g • B)),
    ?e_a.f✝ a ha = ?e_a.f✝ b hb → a = b

case e_a.h₃
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ b ∈ Finset.univ, ∃ a, ∃ (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), ?e_a.f✝ a ha = b

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = Set.ncard B
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a.f
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_ne : Set.Nonempty B
this : Fintype X
⊢ (a : Set X) → a ∈ Set.toFinset (Set.range fun g => g • B) → ↑(Set.range fun g => g • B)

case e_a.h₁
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ (a : Set X) (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), ?e_a.f✝ a ha ∈ Finset.univ

case e_a.h₂
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ (a b : Set X) (ha : a ∈ Set.toFinset (Set.range fun g => g • B)) (hb : b ∈ Set.toFinset (Set.range fun g => g • B)),
    ?e_a.f✝ a ha = ?e_a.f✝ b hb → a = b

case e_a.h₃
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ b ∈ Finset.univ, ∃ a, ∃ (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), ?e_a.f✝ a ha = b

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = Set.ncard B
Tactic:
exact fun s hs => ⟨s, Set.mem_toFinset.mp hs⟩
Proof state after:
case e_a.h₁
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ (a : Set X) (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), { val := a, property := ⋯ } ∈ Finset.univ

case e_a.h₂
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ (a b : Set X) (ha : a ∈ Set.toFinset (Set.range fun g => g • B)) (hb : b ∈ Set.toFinset (Set.range fun g => g • B)),
    { val := a, property := ⋯ } = { val := b, property := ⋯ } → a = b

case e_a.h₃
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ b ∈ Finset.univ, ∃ a, ∃ (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), { val := a, property := ⋯ } = b

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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = Set.ncard B
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = Set.ncard B
Tactic:
rintro ⟨x, ⟨g, rfl⟩⟩ _
Proof state after:
case mk.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_ne : Set.Nonempty B
this : Fintype X
g : G
a✝ : { val := (fun g => g • B) g, property := ⋯ } ∈ Finset.univ
⊢ Set.ncard ↑{ val := (fun g => g • B) g, property := ⋯ } = Set.ncard B
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case mk.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_ne : Set.Nonempty B
this : Fintype X
g : G
a✝ : { val := (fun g => g • B) g, property := ⋯ } ∈ Finset.univ
⊢ Set.ncard ↑{ val := (fun g => g • B) g, property := ⋯ } = Set.ncard B
Tactic:
simp only
Proof state after:
case mk.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_ne : Set.Nonempty B
this : Fintype X
g : G
a✝ : { val := (fun g => g • B) g, property := ⋯ } ∈ Finset.univ
⊢ Set.ncard (g • B) = Set.ncard B
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case mk.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_ne : Set.Nonempty B
this : Fintype X
g : G
a✝ : { val := (fun g => g • B) g, property := ⋯ } ∈ Finset.univ
⊢ Set.ncard (g • B) = Set.ncard B
Tactic:
exact Set.ncard_image_of_injective B (MulAction.injective g)
Proof state after:
no goals
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a.h₁
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ (a : Set X) (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), { val := a, property := ⋯ } ∈ Finset.univ
Tactic:
intro s hs
Proof state after:
case e_a.h₁
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_ne : Set.Nonempty B
this : Fintype X
s : Set X
hs : s ∈ Set.toFinset (Set.range fun g => g • B)
⊢ { val := s, property := ⋯ } ∈ Finset.univ
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a.h₁
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_ne : Set.Nonempty B
this : Fintype X
s : Set X
hs : s ∈ Set.toFinset (Set.range fun g => g • B)
⊢ { val := s, property := ⋯ } ∈ Finset.univ
Tactic:
apply Finset.mem_univ
Proof state after:
no goals
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a.h₂
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ (a b : Set X) (ha : a ∈ Set.toFinset (Set.range fun g => g • B)) (hb : b ∈ Set.toFinset (Set.range fun g => g • B)),
    { val := a, property := ⋯ } = { val := b, property := ⋯ } → a = b
Tactic:
intro s t hs ht hst
Proof state after:
case e_a.h₂
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_ne : Set.Nonempty B
this : Fintype X
s t : Set X
hs : s ∈ Set.toFinset (Set.range fun g => g • B)
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
hst : { val := s, property := ⋯ } = { val := t, property := ⋯ }
⊢ s = t
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a.h₂
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_ne : Set.Nonempty B
this : Fintype X
s t : Set X
hs : s ∈ Set.toFinset (Set.range fun g => g • B)
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
hst : { val := s, property := ⋯ } = { val := t, property := ⋯ }
⊢ s = t
Tactic:
rw [← Subtype.val_inj] at hst
Proof state after:
case e_a.h₂
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_ne : Set.Nonempty B
this : Fintype X
s t : Set X
hs : s ∈ Set.toFinset (Set.range fun g => g • B)
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
hst : ↑{ val := s, property := ⋯ } = ↑{ val := t, property := ⋯ }
⊢ s = t
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a.h₂
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_ne : Set.Nonempty B
this : Fintype X
s t : Set X
hs : s ∈ Set.toFinset (Set.range fun g => g • B)
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
hst : ↑{ val := s, property := ⋯ } = ↑{ val := t, property := ⋯ }
⊢ s = t
Tactic:
exact hst
Proof state after:
no goals
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a.h₃
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_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ b ∈ Finset.univ, ∃ a, ∃ (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), { val := a, property := ⋯ } = b
Tactic:
rintro ⟨b, hb⟩ _
Proof state after:
case e_a.h₃.mk
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_ne : Set.Nonempty B
this : Fintype X
b : Set X
hb : b ∈ Set.range fun g => g • B
a✝ : { val := b, property := hb } ∈ Finset.univ
⊢ ∃ a, ∃ (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), { val := a, property := ⋯ } = { val := b, property := hb }
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case e_a.h₃.mk
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_ne : Set.Nonempty B
this : Fintype X
b : Set X
hb : b ∈ Set.range fun g => g • B
a✝ : { val := b, property := hb } ∈ Finset.univ
⊢ ∃ a, ∃ (ha : a ∈ Set.toFinset (Set.range fun g => g • B)), { val := a, property := ⋯ } = { val := b, property := hb }
Tactic:
use b
Proof state after:
case h
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_ne : Set.Nonempty B
this : Fintype X
b : Set X
hb : b ∈ Set.range fun g => g • B
a✝ : { val := b, property := hb } ∈ Finset.univ
⊢ ∃ (ha : b ∈ Set.toFinset (Set.range fun g => g • B)), { val := b, property := ⋯ } = { val := b, property := hb }
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case h
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_ne : Set.Nonempty B
this : Fintype X
b : Set X
hb : b ∈ Set.range fun g => g • B
a✝ : { val := b, property := hb } ∈ Finset.univ
⊢ ∃ (ha : b ∈ Set.toFinset (Set.range fun g => g • B)), { val := b, property := ⋯ } = { val := b, property := hb }
Tactic:
simp only [Set.mem_toFinset]
Proof state after:
case h
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_ne : Set.Nonempty B
this : Fintype X
b : Set X
hb : b ∈ Set.range fun g => g • B
a✝ : { val := b, property := hb } ∈ Finset.univ
⊢ ∃ (_ : b ∈ Set.range fun g => g • B), True
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
case h
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_ne : Set.Nonempty B
this : Fintype X
b : Set X
hb : b ∈ Set.range fun g => g • B
a✝ : { val := b, property := hb } ∈ Finset.univ
⊢ ∃ (_ : b ∈ Set.range fun g => g • B), True
Tactic:
use 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
hB' : Nat.card X < 2 * Set.ncard B
⊢ B = ⊤
Tactic:
letI := Fintype.ofFinite X
Proof 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 = ⊤
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
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
Proof 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 = ⊤
Theorem: MulAction.is_top_of_large_block
Proof 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']
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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]
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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' ⊢
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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]
Proof 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
Theorem: MulAction.is_top_of_large_block
Proof 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
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 ≤ 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
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 B
this : Fintype X := Fintype.ofFinite X
hB_e : B = ∅
⊢ B = ⊤
Tactic:
exfalso
Proof 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
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 B
this : Fintype X := Fintype.ofFinite X
hB_e : B = ∅
⊢ False
Tactic:
rw [hB_e] at hB'
Proof 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