internlm/Lean-Github huggingface dataset:
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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⟩
Proof 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✝ }
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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)⟩
Proof 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✝ }
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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'
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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'
Proof state after:
no goals
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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 ⊢
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof state after:
no goals
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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 ⊢
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof state after:
no goals
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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]
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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]
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof state after:
no goals
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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]
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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]
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof state after:
no goals
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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⟩
Proof 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✝ }
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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)⟩
Proof 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✝ }
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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 ⊢
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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
Proof 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
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof 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]
Proof 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