Theorem: MulAction.IsBlockSystem.of_block (Jordan/Blocks.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ IsBlockSystem G (Set.range fun g => g • B)
Tactic:
constructor
State after:
case left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ Setoid.IsPartition (Set.range fun g => g • B)

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

State before:
case left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ Setoid.IsPartition (Set.range fun g => g • B)

case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ b ∈ Set.range fun g => g • B, IsBlock G b
Tactic:
constructor
State after:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∅ ∉ Set.range fun g => g • B

case left.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ (a : X), ∃! b x, a ∈ b

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

State before:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ b ∈ Set.range fun g => g • B, IsBlock G b
Tactic:
intro b
State after:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
b : Set X
⊢ (b ∈ Set.range fun g => g • B) → IsBlock G b

State before:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
b : Set X
⊢ (b ∈ Set.range fun g => g • B) → IsBlock G b
Tactic:
rintro ⟨g, hg : g • B = b⟩
State after:
case right.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
b : Set X
g : G
hg : g • B = b
⊢ IsBlock G b

State before:
case right.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
b : Set X
g : G
hg : g • B = b
⊢ IsBlock G b
Tactic:
rw [← hg]
State after:
case right.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
b : Set X
g : G
hg : g • B = b
⊢ IsBlock G (g • B)

State before:
case right.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
b : Set X
g : G
hg : g • B = b
⊢ IsBlock G (g • B)
Tactic:
exact IsBlock_of_block g hB
State after:
no goals

State before:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∅ ∉ Set.range fun g => g • B
Tactic:
simp only [Set.mem_range, not_exists]
State after:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ (x : G), ¬x • B = ∅

State before:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ (x : G), ¬x • B = ∅
Tactic:
intro x hx
State after:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ False

State before:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ False
Tactic:
apply Set.Nonempty.ne_empty hBe
State after:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ B = ∅

State before:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ B = ∅
Tactic:
rw [← Set.image_eq_empty]
State after:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ ?m.112447 '' B = ∅

G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ Type ?u.112444

G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ X → ?m.112446

State before:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ ?m.112447 '' B = ∅

G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ Type ?u.112444

G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
x : G
hx : x • B = ∅
⊢ X → ?m.112446
Tactic:
exact hx
State after:
no goals

State before:
case left.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ (a : X), ∃! b x, a ∈ b
Tactic:
intro a
State after:
case left.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
a : X
⊢ ∃! b x, a ∈ b

State before:
case left.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
a : X
⊢ ∃! b x, a ∈ b
Tactic:
obtain ⟨b : X, hb : b ∈ B⟩ := hBe
State after:
case left.right.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
⊢ ∃! b x, a ∈ b

State before:
case left.right.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
⊢ ∃! b x, a ∈ b
Tactic:
obtain ⟨g, hab⟩ := exists_smul_eq G b a
State after:
case left.right.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
⊢ ∃! b x, a ∈ b

State before:
case left.right.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
⊢ ∃! b x, a ∈ b
Tactic:
have hg : a ∈ g • B := by
  change a ∈ (fun b => g • b) '' B
  rw [Set.mem_image]
  use b
State after:
case left.right.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ ∃! b x, a ∈ b

State before:
case left.right.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ ∃! b x, a ∈ b
Tactic:
use g • B
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ (fun b => ∃! x, a ∈ b) (g • B) ∧ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = g • B

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ (fun b => ∃! x, a ∈ b) (g • B) ∧ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = g • B
Tactic:
constructor
State after:
case h.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ (fun b => ∃! x, a ∈ b) (g • B)

case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = g • B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
⊢ a ∈ g • B
Tactic:
change a ∈ (fun b => g • b) '' B
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
⊢ a ∈ (fun b => g • b) '' B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
⊢ a ∈ (fun b => g • b) '' B
Tactic:
rw [Set.mem_image]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
⊢ ∃ x ∈ B, g • x = a

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
⊢ ∃ x ∈ B, g • x = a
Tactic:
use b
State after:
no goals

State before:
case h.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ (fun b => ∃! x, a ∈ b) (g • B)
Tactic:
simp only [Set.mem_range, exists_apply_eq_apply, exists_unique_iff_exists, exists_true_left]
State after:
case h.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ a ∈ g • B

State before:
case h.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ a ∈ g • B
Tactic:
exact hg
State after:
no goals

State before:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = g • B
Tactic:
simp only [Set.mem_range, exists_unique_iff_exists, exists_prop, and_imp, forall_exists_index,
  forall_apply_eq_imp_iff']
State after:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ ∀ (y : Set X) (x : G), x • B = y → a ∈ y → y = g • B

State before:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
⊢ ∀ (y : Set X) (x : G), x • B = y → a ∈ y → y = g • B
Tactic:
intro B' g' hg' ha
State after:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ B' = g • B

State before:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ B' = g • B
Tactic:
rw [← hg']
State after:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ g' • B = g • B

State before:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ g' • B = g • B
Tactic:
apply symm
State after:
case h.right.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ g • B = g' • B

State before:
case h.right.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ g • B = g' • B
Tactic:
apply Or.resolve_right (IsBlock.def.mp hB g g')
State after:
case h.right.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ ¬Disjoint (g • B) (g' • B)

State before:
case h.right.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ ¬Disjoint (g • B) (g' • B)
Tactic:
rw [Set.not_disjoint_iff]
State after:
case h.right.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ ∃ x ∈ g • B, x ∈ g' • B

State before:
case h.right.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ ∃ x ∈ g • B, x ∈ g' • B
Tactic:
use a
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ a ∈ g • B ∧ a ∈ g' • B

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ a ∈ g • B ∧ a ∈ g' • B
Tactic:
rw [hg']
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ a ∈ g • B ∧ a ∈ B'

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a b : X
hb : b ∈ B
g : G
hab : g • b = a
hg : a ∈ g • B
B' : Set X
g' : G
hg' : g' • B = B'
ha : a ∈ B'
⊢ a ∈ g • B ∧ a ∈ B'
Tactic:
exact ⟨hg, ha⟩
State after:
no goals