internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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⟩
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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]
Proof 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)
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlockSystem.of_block
Proof 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]
Proof 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 = ∅
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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 = ∅
Theorem: MulAction.IsBlockSystem.of_block
Proof 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]
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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]
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlockSystem.of_block
Proof 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]
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlockSystem.of_block
Proof 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']
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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']
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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')
Proof 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)
Theorem: MulAction.IsBlockSystem.of_block
Proof 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]
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_block
Proof 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']
Proof 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'
Theorem: MulAction.IsBlockSystem.of_block
Proof 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⟩
Proof state after:
no goals
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ Setoid.IsPartition (Set.range fun a => orbit G a)
Tactic:
constructor
Proof state after:
case left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ ∅ ∉ Set.range fun a => orbit G a

case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃! b x, a ∈ b
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃! b x, a ∈ b
Tactic:
intro a
Proof state after:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∃! b x, a ∈ b
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∃! b x, a ∈ b
Tactic:
use orbit G a
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (fun b => ∃! x, a ∈ b) (orbit G a) ∧ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = orbit G a
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (fun b => ∃! x, a ∈ b) (orbit G a) ∧ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = orbit G a
Tactic:
constructor
Proof state after:
case h.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (fun b => ∃! x, a ∈ b) (orbit G a)

case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = orbit G a
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ ∅ ∉ Set.range fun a => orbit G a
Tactic:
rintro ⟨a, ha : orbit G a = ∅⟩
Proof state after:
case left.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
ha : orbit G a = ∅
⊢ False
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case left.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
ha : orbit G a = ∅
⊢ False
Tactic:
exact Set.Nonempty.ne_empty (MulAction.orbit_nonempty a) ha
Proof state after:
no goals
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case h.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (fun b => ∃! x, a ∈ b) (orbit G a)
Tactic:
simp only [Set.mem_range_self, mem_orbit_self, exists_unique_iff_exists, exists_true_left]
Proof state after:
no goals
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = orbit G a
Tactic:
simp only [Set.mem_range, exists_unique_iff_exists, exists_prop, and_imp, forall_exists_index,
  forall_apply_eq_imp_iff']
Proof state after:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (y : Set X) (x : X), orbit G x = y → a ∈ y → y = orbit G a
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (y : Set X) (x : X), orbit G x = y → a ∈ y → y = orbit G a
Tactic:
rintro B b ⟨rfl⟩ ha
Proof state after:
case h.right.refl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ orbit G b = orbit G a
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case h.right.refl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ orbit G b = orbit G a
Tactic:
apply symm
Proof state after:
case h.right.refl.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ orbit G a = orbit G b
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case h.right.refl.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ orbit G a = orbit G b
Tactic:
rw [orbit_eq_iff]
Proof state after:
case h.right.refl.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ a ∈ orbit G b
Theorem: MulAction.IsPartition.of_orbits
Proof state before:
case h.right.refl.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ a ∈ orbit G b
Tactic:
exact ha
Proof state after:
no goals
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
⊢ IsBlock G (orbit (↥N) a)
Tactic:
rw [IsBlock.def_one]
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
⊢ ∀ (g : G), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
⊢ ∀ (g : G), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Tactic:
intro g
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
⊢ g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
⊢ g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Tactic:
suffices g • orbit N a = orbit N (g • a) by rw [this]; apply orbit.equal_or_disjoint
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
⊢ g • orbit (↥N) a = orbit (↥N) (g • a)
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
⊢ g • orbit (↥N) a = orbit (↥N) (g • a)
Tactic:
change ((fun x : X => g • x) '' Set.range fun k : N => k • a) = Set.range fun k : N => k • g • a
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
⊢ ((fun x => g • x) '' Set.range fun k => k • a) = Set.range fun k => k • g • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
⊢ ((fun x => g • x) '' Set.range fun k => k • a) = Set.range fun k => k • g • a
Tactic:
simp only [Set.image_smul, Set.smul_set_range]
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
⊢ (Set.range fun i => g • i • a) = Set.range fun k => k • g • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
⊢ (Set.range fun i => g • i • a) = Set.range fun k => k • g • a
Tactic:
ext
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
x✝ : X
⊢ (x✝ ∈ Set.range fun i => g • i • a) ↔ x✝ ∈ Set.range fun k => k • g • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
x✝ : X
⊢ (x✝ ∈ Set.range fun i => g • i • a) ↔ x✝ ∈ Set.range fun k => k • g • a
Tactic:
simp only [Set.mem_range]
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) ↔ ∃ y, y • g • a = x✝
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) ↔ ∃ y, y • g • a = x✝
Tactic:
constructor
Proof state after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) → ∃ y, y • g • a = x✝

case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
x✝ : X
⊢ (∃ y, y • g • a = x✝) → ∃ y, g • y • a = x✝