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

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
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X
Tactic:
have := Fintype.ofFinite X
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 B * Set.ncard (Set.range fun g => g • B) = Nat.card X

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) = Nat.card X
Tactic:
rw [← Setoid.nat_sum (IsBlockSystem.of_block hB hB_ne).1]
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 B * Set.ncard (Set.range fun g => g • B) = ∑ᶠ (x : ↑(Set.range fun g => g • B)), Nat.card ↑↑x

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) = ∑ᶠ (x : ↑(Set.range fun g => g • B)), Nat.card ↑↑x
Tactic:
simp only [finsum_eq_sum_of_fintype]
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 B * Set.ncard (Set.range fun g => g • B) = ∑ x : ↑(Set.range fun g => g • B), Nat.card ↑↑x

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) = ∑ x : ↑(Set.range fun g => g • B), Nat.card ↑↑x
Tactic:
simp_rw [Set.Nat.card_coe_set_eq]
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 B * Set.ncard (Set.range fun g => g • B) = ∑ x : ↑(Set.range fun g => g • B), Set.ncard ↑x

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) = ∑ x : ↑(Set.range fun g => g • B), Set.ncard ↑x
Tactic:
rw [Finset.sum_congr rfl ?_]
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 B * Set.ncard (Set.range fun g => g • B) = Finset.sum Finset.univ ?m.191744

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.range fun g => g • 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 = ?m.191744 x

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.sum Finset.univ ?m.191744

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.range fun g => g • 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 = ?m.191744 x
Tactic:
rw [Finset.sum_const]
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 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

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]
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

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
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

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']
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

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]
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

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⟩
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

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⟩⟩ _
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

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
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

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)
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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⟩ _
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 }

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
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 }

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]
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

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
State after:
no goals