Theorem: isPretransitive_ofFixingSubgroup_inter (Jordan/Jordan.lean)

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
rw [Ne.def, Set.top_eq_univ, ← Set.compl_empty_iff, ← Ne.def, ← Set.nonempty_iff_ne_empty] at ha
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : Set.Nonempty (s ∪ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : Set.Nonempty (s ∪ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
obtain ⟨a, ha⟩ := ha
State after:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))

State before:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
have ha' : a ∈ (s ∩ g • s)ᶜ := by
  rw [Set.compl_inter]
  apply Set.mem_union_left
  rw [Set.compl_union] at ha
  apply Set.mem_of_mem_inter_left ha
State after:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))

State before:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
apply (IsPretransitive.mk_base_iff (⟨a, ha'⟩ : SubMulAction.ofFixingSubgroup G (s ∩ g • s))).mpr
State after:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ ∀ (x : ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))), ∃ g_1, g_1 • { val := a, property := ha' } = x

State before:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ ∀ (x : ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))), ∃ g_1, g_1 • { val := a, property := ha' } = x
Tactic:
rintro ⟨x, hx⟩
State after:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx }

State before:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx }
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff, Set.mem_inter_iff, not_and_or] at hx
State after:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s ∨ x ∉ g • s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }

State before:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s ∨ x ∉ g • s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
cases' hx with hx hx
State after:
case intro.mk.inl
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }

case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ (s ∩ g • s)ᶜ
Tactic:
rw [Set.compl_inter]
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ sᶜ ∪ (g • s)ᶜ

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ sᶜ ∪ (g • s)ᶜ
Tactic:
apply Set.mem_union_left
State after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ sᶜ

State before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ sᶜ
Tactic:
rw [Set.compl_union] at ha
State after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
⊢ a ∈ sᶜ

State before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
⊢ a ∈ sᶜ
Tactic:
apply Set.mem_of_mem_inter_left ha
State after:
no goals

State before:
case intro.mk.inl
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq
  ⟨a, (by intro ha'; apply ha; apply Set.mem_union_left _ ha')⟩
  ⟨x, hx⟩
State after:
case intro.mk.inl.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := a, property := ⋯ } = { val := x, property := hx }
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }

State before:
case intro.mk.inl.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := a, property := ⋯ } = { val := x, property := hx }
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
use ⟨k, (by
  rw [mem_fixingSubgroup_iff] at hk ⊢
  intro y  hy
  apply hk
  apply Set.mem_of_mem_inter_left hy)⟩
State after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := a, property := ⋯ } = { val := x, property := hx }
⊢ { val := k, property := ⋯ } • { val := a, property := ha' } = { val := x, property := hx✝ }

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
⊢ a ∈ SubMulAction.ofFixingSubgroup G s
Tactic:
intro ha'
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha'✝ : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
ha' : a ∈ s
⊢ False

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha'✝ : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
ha' : a ∈ s
⊢ False
Tactic:
apply ha
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha'✝ : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
ha' : a ∈ s
⊢ a ∈ s ∪ g • s

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha'✝ : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
ha' : a ∈ s
⊢ a ∈ s ∪ g • s
Tactic:
apply Set.mem_union_left _ ha'
State after:
no goals

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := a, property := ⋯ } = { val := x, property := hx }
⊢ k ∈ fixingSubgroup G (s ∩ g • s)
Tactic:
rw [mem_fixingSubgroup_iff] at hk ⊢
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := a, property := ⋯ } = { val := x, property := hx }
⊢ ∀ y ∈ s ∩ g • s, k • y = y

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := a, property := ⋯ } = { val := x, property := hx }
⊢ ∀ y ∈ s ∩ g • s, k • y = y
Tactic:
intro y  hy
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := a, property := ⋯ } = { val := x, property := hx }
y : α
hy : y ∈ s ∩ g • s
⊢ k • y = y

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := a, property := ⋯ } = { val := x, property := hx }
y : α
hy : y ∈ s ∩ g • s
⊢ k • y = y
Tactic:
apply hk
State after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := a, property := ⋯ } = { val := x, property := hx }
y : α
hy : y ∈ s ∩ g • s
⊢ y ∈ s

State before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := a, property := ⋯ } = { val := x, property := hx }
y : α
hy : y ∈ s ∩ g • s
⊢ y ∈ s
Tactic:
apply Set.mem_of_mem_inter_left hy
State after:
no goals

State before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := a, property := ⋯ } = { val := x, property := hx }
⊢ { val := k, property := ⋯ } • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
simp only [← SetLike.coe_eq_coe] at hkax ⊢
State after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk : k ∈ fixingSubgroup G s
hkax : ↑({ val := k, property := hk } • { val := a, property := ⋯ }) = x
⊢ ↑({ val := k, property := ⋯ } • { val := a, property := ha' }) = x

State before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
k : G
hk : k ∈ fixingSubgroup G s
hkax : ↑({ val := k, property := hk } • { val := a, property := ⋯ }) = x
⊢ ↑({ val := k, property := ⋯ } • { val := a, property := ha' }) = x
Tactic:
exact hkax
State after:
no goals

State before:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
⊢ g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff]
State after:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
⊢ g⁻¹ • x ∉ s

State before:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
⊢ g⁻¹ • x ∉ s
Tactic:
intro h
State after:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
h : g⁻¹ • x ∈ s
⊢ False

State before:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
h : g⁻¹ • x ∈ s
⊢ False
Tactic:
apply hx
State after:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
h : g⁻¹ • x ∈ s
⊢ x ∈ g • s

State before:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
h : g⁻¹ • x ∈ s
⊢ x ∈ g • s
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem]
State after:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
h : g⁻¹ • x ∈ s
⊢ g⁻¹ • x ∈ s

State before:
case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
h : g⁻¹ • x ∈ s
⊢ g⁻¹ • x ∈ s
Tactic:
exact h
State after:
no goals

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
⊢ g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff]
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
⊢ g⁻¹ • a ∉ s

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
⊢ g⁻¹ • a ∉ s
Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem]
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
⊢ a ∉ g • s

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
⊢ a ∉ g • s
Tactic:
intro h
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
h : a ∈ g • s
⊢ False

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
h : a ∈ g • s
⊢ False
Tactic:
apply ha
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
h : a ∈ g • s
⊢ a ∈ s ∪ g • s

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
h : a ∈ g • s
⊢ a ∈ s ∪ g • s
Tactic:
apply Set.mem_union_right _ h
State after:
no goals

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨g⁻¹ • a, hg'a⟩ ⟨g⁻¹ • x, hg'x⟩
State after:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }

State before:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
use ⟨g * k * g⁻¹, (by
  rw [mem_fixingSubgroup_iff] at hk ⊢
  intro y hy
  simp [← smul_smul, smul_eq_iff_eq_inv_smul g]
  apply hk
  rw [← Set.mem_smul_set_iff_inv_smul_mem]
  exact Set.mem_of_mem_inter_right hy)⟩
State after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
⊢ { val := g * k * g⁻¹, property := ⋯ } • { val := a, property := ha' } = { val := x, property := hx✝ }

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
⊢ g * k * g⁻¹ ∈ fixingSubgroup G (s ∩ g • s)
Tactic:
rw [mem_fixingSubgroup_iff] at hk ⊢
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
⊢ ∀ y ∈ s ∩ g • s, (g * k * g⁻¹) • y = y

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
⊢ ∀ y ∈ s ∩ g • s, (g * k * g⁻¹) • y = y
Tactic:
intro y hy
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ (g * k * g⁻¹) • y = y

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ (g * k * g⁻¹) • y = y
Tactic:
simp [← smul_smul, smul_eq_iff_eq_inv_smul g]
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ k • g⁻¹ • y = g⁻¹ • y

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ k • g⁻¹ • y = g⁻¹ • y
Tactic:
apply hk
State after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ g⁻¹ • y ∈ s

State before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ g⁻¹ • y ∈ s
Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem]
State after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ y ∈ g • s

State before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ y ∈ g • s
Tactic:
exact Set.mem_of_mem_inter_right hy
State after:
no goals

State before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
⊢ { val := g * k * g⁻¹, property := ⋯ } • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
simp only [← SetLike.coe_eq_coe] at hkax ⊢
State after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : ↑({ val := k, property := hk } • { val := g⁻¹ • a, property := hg'a }) = g⁻¹ • x
⊢ ↑({ val := g * k * g⁻¹, property := ⋯ } • { val := a, property := ha' }) = x

State before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : ↑({ val := k, property := hk } • { val := g⁻¹ • a, property := hg'a }) = g⁻¹ • x
⊢ ↑({ val := g * k * g⁻¹, property := ⋯ } • { val := a, property := ha' }) = x
Tactic:
simp only [SetLike.val_smul] at hkax ⊢
State after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • g⁻¹ • a = g⁻¹ • x
⊢ { val := g * k * g⁻¹, property := ⋯ } • a = x

State before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • g⁻¹ • a = g⁻¹ • x
⊢ { val := g * k * g⁻¹, property := ⋯ } • a = x
Tactic:
rw [← smul_eq_iff_eq_inv_smul] at hkax
State after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ { val := g * k * g⁻¹, property := ⋯ } • a = x

State before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ { val := g * k * g⁻¹, property := ⋯ } • a = x
Tactic:
change (g * k * g⁻¹) • a = x
State after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ (g * k * g⁻¹) • a = x

State before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ (g * k * g⁻¹) • a = x
Tactic:
simp only [← smul_smul]
State after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ g • k • g⁻¹ • a = x

State before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ g • k • g⁻¹ • a = x
Tactic:
exact hkax
State after:
no goals