Theorem: Equiv.Perm.IsPretransitive.of_partition (Jordan/PermMaximal.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
⊢ (∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b) → (∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b) → stabilizer G s ≠ ⊤ → IsPretransitive G α
Tactic:
intro hs hs' hG
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
⊢ IsPretransitive G α

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
⊢ ∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
Tactic:
by_contra hyp
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ¬∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ¬∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
⊢ False
Tactic:
push_neg at hyp
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ False
Tactic:
apply hG
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ stabilizer G s = ⊤

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ stabilizer G s = ⊤
Tactic:
rw [eq_top_iff, MulAction.le_stabilizer_iff_smul_le]
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ ∀ g ∈ ⊤, g • s ⊆ s

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ ∀ g ∈ ⊤, g • s ⊆ s
Tactic:
intro g _
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
⊢ g • s ⊆ s

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
⊢ g • s ⊆ s
Tactic:
rintro b ⟨a, ha, hgab⟩
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x => g • x) a = b
⊢ b ∈ s

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x => g • x) a = b
⊢ b ∈ s
Tactic:
by_contra hb
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x => g • x) a = b
hb : b ∉ s
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x => g • x) a = b
hb : b ∉ s
⊢ False
Tactic:
exact hyp a b g ha (Set.mem_compl hb) hgab
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hss' : ∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
⊢ IsPretransitive G α
Tactic:
obtain ⟨a, b, g, ha, hb, hgab⟩ := hss'
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ IsPretransitive G α

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ IsPretransitive G α
Tactic:
apply IsPretransitive.mk_base a
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ ∀ (x : α), ∃ g, g • a = x

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ ∀ (x : α), ∃ g, g • a = x
Tactic:
intro x
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
⊢ ∃ g, g • a = x

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
⊢ ∃ g, g • a = x
Tactic:
by_cases hx : x ∈ s
State after:
case pos
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ s
⊢ ∃ g, g • a = x

case neg
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ g, g • a = x

State before:
case pos
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ s
⊢ ∃ g, g • a = x
Tactic:
exact hs a ha x hx
State after:
no goals

State before:
case neg
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ g, g • a = x
Tactic:
rw [← Set.mem_compl_iff] at hx
State after:
case neg
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
⊢ ∃ g, g • a = x

State before:
case neg
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
⊢ ∃ g, g • a = x
Tactic:
obtain ⟨k, hk⟩ := hs' b hb x hx
State after:
case neg.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : G
hk : k • b = x
⊢ ∃ g, g • a = x

State before:
case neg.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : G
hk : k • b = x
⊢ ∃ g, g • a = x
Tactic:
use k * g
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : G
hk : k • b = x
⊢ (k * g) • a = x

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : G
hk : k • b = x
⊢ (k * g) • a = x
Tactic:
rw [MulAction.mul_smul, hgab, hk]
State after:
no goals