-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X]
    (hB : IsBlock G B) (hBe : B.Nonempty) :
    IsBlockSystem G (Set.range fun g : G => g • B)

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
⊢ IsBlock G ((fun g => g • B) g)

Tactic:
exact hB.translate g

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ ∀ (a : G), g • b ∈ a • B → a • B = g • B

Tactic:
exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ IsBlockSystem G (range fun g => g • B)

Tactic:
refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩

Result:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∅ ∉ range fun g => g • B

case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (a : X), ∃! b, (b ∈ range fun g => g • B) ∧ a ∈ b

case mem_blocks
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ ⦃B_1 : Set X⦄, (B_1 ∈ range fun g => g • B) → IsBlock G B_1

Proof state:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∅ ∉ range fun g => g • B

case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (a : X), ∃! b, (b ∈ range fun g => g • B) ∧ a ∈ b

case mem_blocks
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ ⦃B_1 : Set X⦄, (B_1 ∈ range fun g => g • B) → IsBlock G B_1

Tactic:
case mem_blocks => rintro B' ⟨g, rfl⟩; exact hB.translate g

Result:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∅ ∉ range fun g => g • B

case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (a : X), ∃! b, (b ∈ range fun g => g • B) ∧ a ∈ b

Proof state:
case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
a : X
⊢ ∃! b, (b ∈ range fun g => g • B) ∧ a ∈ b

Tactic:
obtain ⟨b : X, hb : b ∈ B⟩ := hBe

Result:
case cover.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
a b : X
hb : b ∈ B
⊢ ∃! b, (b ∈ range fun g => g • B) ∧ a ∈ b

Proof state:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ False

Tactic:
apply hBe.ne_empty

Result:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ B = ∅

Proof state:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (x : G), ¬x • B = ∅

Tactic:
intro g hg

Result:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ False

Proof state:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ B = ∅

Tactic:
simpa only [Set.smul_set_eq_empty] using hg

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ (fun b_1 => (b_1 ∈ range fun g => g • B) ∧ g • b ∈ b_1) (g • B) ∧
    ∀ (y : Set X), (fun b_1 => (b_1 ∈ range fun g => g • B) ∧ g • b ∈ b_1) y → y = g • B

Tactic:
simp only [Set.smul_mem_smul_set_iff, hb, existsUnique_iff_exists, Set.mem_range,
  exists_apply_eq_apply, exists_const, exists_prop, and_imp, forall_exists_index,
  forall_apply_eq_imp_iff, true_and]

Result:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ ∀ (a : G), g • b ∈ a • B → a • B = g • B

Proof state:
case cover.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
a b : X
hb : b ∈ B
⊢ ∃! b, (b ∈ range fun g => g • B) ∧ a ∈ b

Tactic:
obtain ⟨g, rfl⟩ := exists_smul_eq G b a

Result:
case cover.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ ∃! b_1, (b_1 ∈ range fun g => g • B) ∧ g • b ∈ b_1

Proof state:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∅ ∉ range fun g => g • B

Tactic:
simp only [Set.mem_range, not_exists]

Result:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (x : G), ¬x • B = ∅

Proof state:
case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (a : X), ∃! b, (b ∈ range fun g => g • B) ∧ a ∈ b

Tactic:
intro a

Result:
case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
a : X
⊢ ∃! b, (b ∈ range fun g => g • B) ∧ a ∈ b

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ ⦃B_1 : Set X⦄, (B_1 ∈ range fun g => g • B) → IsBlock G B_1

Tactic:
rintro B' ⟨g, rfl⟩

Result:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
⊢ IsBlock G ((fun g => g • B) g)

Proof state:
case cover.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ ∃! b_1, (b_1 ∈ range fun g => g • B) ∧ g • b ∈ b_1

Tactic:
use g • B

Result:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ (fun b_1 => (b_1 ∈ range fun g => g • B) ∧ g • b ∈ b_1) (g • B) ∧
    ∀ (y : Set X), (fun b_1 => (b_1 ∈ range fun g => g • B) ∧ g • b ∈ b_1) y → y = g • B