∀U : set α, is_open U → set.nonempty U → rigid_stabilizer G U ≠ ⊥
lemma dense_locally_moving : t2_space α ∧ has_no_isolated_points α ∧ is_locally_dense G α → is_locally_moving G α := begin
rintros ⟨t2α,nipα,ildGα⟩ U ioU neU,
by_contra,
have some_in_U := ildGα U neU.some neU.some_mem,
rw [h,orbit_bot G neU.some,@closure_singleton α _ (@t2_space.t1_space α _ t2α) neU.some,@interior_singleton α _ neU.some (nipα neU.some)] at some_in_U,
tauto
end
-- lemma dense_locally_moving : t2_space α ∧ has_no_isolated_points α ∧ is_locally_dense G α → is_locally_moving G α := begin
-- rintros ⟨t2α,nipα,ildGα⟩ U ioU neU,
-- by_contra,
-- have some_in_U := ildGα U neU.some neU.some_mem,
-- rw [h,orbit_bot G neU.some,@closure_singleton α _ (@t2_space.t1_space α _ t2α) neU.some,@interior_singleton α _ neU.some (nipα neU.some)] at some_in_U,
-- tauto
-- end
lemma disjoint_nbhd {g : G} {x : α} [t2_space α] : g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ disjoint U (g •'' U) := begin
intro xmoved,
rcases t2_space.t2 (g • x) x xmoved with ⟨V,W,open_V,open_W,gx_in_V,x_in_W,disjoint_V_W⟩,
let U := (g⁻¹ •'' V) ∩ W,
use U,
split,
exact is_open.inter (img_open_open g⁻¹ V open_V) open_W,
split,
exact ⟨mem_inv_smul''.mpr gx_in_V,x_in_W⟩,
exact set.disjoint_of_subset
(set.inter_subset_right (g⁻¹•''V) W)
(λ y hy, smul_inv_smul g y ▸ mem_inv_smul''.mp (set.mem_of_mem_inter_left (mem_smul''.mp hy)) : g•''U ⊆ V)
disjoint_V_W.symm
end
-- lemma disjoint_nbhd {g : G} {x : α} [t2_space α] : g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ disjoint U (g •'' U) := begin
-- intro xmoved,
-- rcases t2_space.t2 (g • x) x xmoved with ⟨V,W,open_V,open_W,gx_in_V,x_in_W,disjoint_V_W⟩,
-- let U := (g⁻¹ •'' V) ∩ W,
-- use U,
-- split,
-- exact is_open.inter (img_open_open g⁻¹ V open_V) open_W,
-- split,
-- exact ⟨mem_inv_smul''.mpr gx_in_V,x_in_W⟩,
-- exact set.disjoint_of_subset
-- (set.inter_subset_right (g⁻¹•''V) W)
-- (λ y hy, smul_inv_smul g y ▸ mem_inv_smul''.mp (set.mem_of_mem_inter_left (mem_smul''.mp hy)) : g•''U ⊆ V)
-- disjoint_V_W.symm
-- end
lemma disjoint_nbhd_in {g : G} {x : α} [t2_space α] {V : set α} : is_open V → x ∈ V → g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ U ⊆ V ∧ disjoint U (g •'' U) := begin
intros open_V x_in_V xmoved,
rcases disjoint_nbhd xmoved with ⟨W,open_W,x_in_W,disjoint_W⟩,
let U := W ∩ V,
use U,
split,
exact is_open.inter open_W open_V,
split,
exact ⟨x_in_W,x_in_V⟩,
split,
exact set.inter_subset_right W V,
exact set.disjoint_of_subset
(set.inter_subset_left W V)
((@smul''_inter _ _ _ _ g W V).symm ▸ set.inter_subset_left (g•''W) (g•''V) : g•''U ⊆ g•''W)
disjoint_W
end
-- lemma disjoint_nbhd_in {g : G} {x : α} [t2_space α] {V : set α} : is_open V → x ∈ V → g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ U ⊆ V ∧ disjoint U (g •'' U) := begin
-- intros open_V x_in_V xmoved,
-- rcases disjoint_nbhd xmoved with ⟨W,open_W,x_in_W,disjoint_W⟩,
-- let U := W ∩ V,
-- use U,
-- split,
-- exact is_open.inter open_W open_V,
-- split,
-- exact ⟨x_in_W,x_in_V⟩,
-- split,
-- exact set.inter_subset_right W V,
-- exact set.disjoint_of_subset
-- (set.inter_subset_left W V)
-- ((@smul''_inter _ _ _ _ g W V).symm ▸ set.inter_subset_left (g•''W) (g•''V) : g•''U ⊆ g•''W)
-- disjoint_W
-- end
lemma rewrite_Union (f : fin 2 × fin 2 → set α) : (⋃(i : fin 2 × fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) := begin
ext,
simp only [set.mem_Union, set.mem_union],
split,
{ simp only [forall_exists_index],
intro i,
fin_cases i; simp {contextual := tt}, },
{ rintro ((h|h)|(h|h)); exact ⟨_, h⟩, },
end
-- lemma rewrite_Union (f : fin 2 × fin 2 → set α) : (⋃(i : fin 2 × fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) := begin
-- ext,
-- simp only [set.mem_Union, set.mem_union],
-- split,
-- { simp only [forall_exists_index],
-- intro i,
-- fin_cases i; simp {contextual := tt}, },
-- { rintro ((h|h)|(h|h)); exact ⟨_, h⟩, },
-- end
lemma proposition_1_1_1 (f g : G) (locally_moving : is_locally_moving G α) [t2_space α] : disjoint (support α f) (support α g) → is_algebraically_disjoint f g := begin
intros disjoint_f_g h hfh,
let support_f := support α f,
-- h is not the identity on support α f
cases set.not_disjoint_iff.mp (mt (@disjoint_commute G α _ _ _ _ _) hfh) with x hx,
let x_in_support_f := hx.1,
let hx_ne_x := mem_support.mp hx.2,
-- so since α is Hausdoff there is V nonempty ⊆ support α f with h•''V disjoint from V
rcases disjoint_nbhd_in (support_open f) x_in_support_f hx_ne_x with ⟨V,open_V,x_in_V,V_in_support,disjoint_img_V⟩,
let ristV_ne_bot := locally_moving V open_V (set.nonempty_of_mem x_in_V),
-- let f₂ be a nontrivial element of rigid_stabilizer G V
rcases (or_iff_right ristV_ne_bot).mp (subgroup.bot_or_exists_ne_one _) with ⟨f₂,f₂_in_ristV,f₂_ne_one⟩,
-- again since α is Hausdorff there is W nonempty ⊆ V with f₂•''W disjoint from W
rcases faithful_moves_point' α f₂_ne_one with ⟨y,ymoved⟩,
let y_in_V : y ∈ V := (rist_supported_in_set f₂_in_ristV) (mem_support.mpr ymoved),
rcases disjoint_nbhd_in open_V y_in_V ymoved with ⟨W,open_W,y_in_W,W_in_V,disjoint_img_W⟩,
-- let f₁ be a nontrivial element of rigid_stabilizer G W
let ristW_ne_bot := locally_moving W open_W (set.nonempty_of_mem y_in_W),
rcases (or_iff_right ristW_ne_bot).mp (subgroup.bot_or_exists_ne_one _) with ⟨f₁,f₁_in_ristW,f₁_ne_one⟩,
use f₁, use f₂,
-- note that f₁,f₂ commute with g since their support is in support α f
-- -- we claim that [f₁,[f₂,h]] is a nontrivial element of centralizer G g
-- let k := ⁅f₂,h⁆,
-- -- first, h*f₂⁻¹*h⁻¹ is supported on h V, so k := [f₂,h] agrees with f₂ on V
-- have h2 : ∀z ∈ W, f₂•z = k•z := λ z z_in_W,
-- (disjoint_support_comm f₂ h (rist_supported_in_set f₂_in_ristV) disjoint_img_V z (W_in_V z_in_W)).symm,
-- -- then k*f₁⁻¹*k⁻¹ is supported on k W = f₂ W, so [f₁,k] is supported on W ∪ f₂ W ⊆ V ⊆ support f, so commutes with g.
-- have h3 : support α ⁅f₁,k⁆ ⊆ support α f := begin
-- let := (support_comm α k f₁).trans (set.union_subset_union (rist_supported_in_set f₁_in_ristW) (smul''_subset k $ rist_supported_in_set f₁_in_ristW)),
-- rw [← commutator_element_inv,support_inv,(smul''_eq_of_smul_eq h2).symm] at this,
-- exact (this.trans $ (set.union_subset_union W_in_V (moves_subset_within_support f₂ W V W_in_V $ rist_supported_in_set f₂_in_ristV)).trans $ eq.subset V.union_self).trans V_in_support
-- let U_inc := set.Inter_subset (λ p : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some) ⟨⟨i,j⟩,i_ne_j⟩,
-- let := (disjoint_smul'' (f j) (set.disjoint_of_subset U_inc (smul''_subset ((f j)⁻¹ * (f i)) U_inc) (disjoint_hyp i j i_ne_j).some_spec.2.2)).symm,
-- simp only [subtype.val_eq_coe, smul''_mul, mul_inv_cancel_left] at this,
-- from this
-- end
lemma moves_inj {g : G} {x : α} {n : ℕ} (period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℤ) • x) := begin
rw [← mul_smul,← mul_smul,← zpow_add,← zpow_add,add_comm] at same_img',
simp only [add_left_neg, zpow_zero, one_smul] at same_img',
let ij := |(i:ℤ) - (j:ℤ)|,
rw ← sub_eq_add_neg at same_img',
have xfixed : g^ij • x = x := begin
cases abs_cases ((i:ℤ) - (j:ℤ)),
{ rw ← h.1 at same_img', exact same_img' },
{ rw [smul_eq_iff_inv_smul_eq,← zpow_neg,← h.1] at same_img', exact same_img' }
end,
have ij_ge_1 : 1 ≤ ij := int.add_one_le_iff.mpr (abs_pos.mpr $ sub_ne_zero.mpr $ norm_num.nat_cast_ne i j ↑i ↑j rfl rfl (fin.vne_of_ne i_ne_j)),
let neg_le := int.sub_lt_sub_of_le_of_lt (nat.cast_nonneg i) (nat.cast_lt.mpr (fin.prop _)),
rw zero_sub at neg_le,
let le_pos := int.sub_lt_sub_of_lt_of_le (nat.cast_lt.mpr (fin.prop _)) (nat.cast_nonneg j),
rw sub_zero at le_pos,
have ij_lt_n : ij < n := abs_lt.mpr ⟨ neg_le, le_pos ⟩,
exact period_ge_n ij ij_ge_1 ij_lt_n xfixed,
end
-- lemma moves_inj {g : G} {x : α} {n : ℕ} (period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℤ) • x) := begin
lemma moves_inj_N {g : G} {x : α} {n : ℕ} (period_ge_n' : ∀ (k : ℕ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℕ) • x) := begin
have period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x,
{ intros k one_le_k k_lt_n,
have one_le_k_nat : 1 ≤ k.nat_abs := ((int.coe_nat_le_coe_nat_iff 1 k.nat_abs).1 ((int_to_nat k one_le_k) ▸ one_le_k)),
have k_nat_lt_n : k.nat_abs < n := ((int.coe_nat_lt_coe_nat_iff k.nat_abs n).1 ((int_to_nat k one_le_k) ▸ k_lt_n)),
have := period_ge_n' k.nat_abs one_le_k_nat k_nat_lt_n,
rw [(zpow_coe_nat g k.nat_abs).symm, (int_to_nat k one_le_k).symm] at this,
exact this },
have := moves_inj period_ge_n,
finish
end
-- lemma moves_inj_N {g : G} {x : α} {n : ℕ} (period_ge_n' : ∀ (k : ℕ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℕ) • x) := begin
-- have period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x,
-- { intros k one_le_k k_lt_n,
-- have one_le_k_nat : 1 ≤ k.nat_abs := ((int.coe_nat_le_coe_nat_iff 1 k.nat_abs).1 ((int_to_nat k one_le_k) ▸ one_le_k)),
-- have k_nat_lt_n : k.nat_abs < n := ((int.coe_nat_lt_coe_nat_iff k.nat_abs n).1 ((int_to_nat k one_le_k) ▸ k_lt_n)),
-- have := period_ge_n' k.nat_abs one_le_k_nat k_nat_lt_n,
-- rw [(zpow_coe_nat g k.nat_abs).symm, (int_to_nat k one_le_k).symm] at this,
-- exact this },
-- have := moves_inj period_ge_n,
-- finish
-- end
lemma moves_1234_of_moves_12 {g : G} {x : α} (xmoves : g^12 • x ≠ x) : function.injective (λi : fin 5, g^(i:ℤ) • x) := begin
apply moves_inj,
intros k k_ge_1 k_lt_5,
by_contra xfixed,
have k_div_12 : k * (12 / k) = 12 := begin
interval_cases using k_ge_1 k_lt_5; norm_num
end,
have veryfixed : g^12 • x = x := begin
let := smul_zpow_eq_of_smul_eq (12/k) xfixed,
rw [← zpow_mul,k_div_12] at this,
norm_cast at this
end,
exact xmoves veryfixed
end
-- lemma moves_1234_of_moves_12 {g : G} {x : α} (xmoves : g^12 • x ≠ x) : function.injective (λi : fin 5, g^(i:ℤ) • x) := begin
-- apply moves_inj,
-- intros k k_ge_1 k_lt_5,
-- by_contra xfixed,
-- have k_div_12 : k * (12 / k) = 12 := begin
-- interval_cases using k_ge_1 k_lt_5; norm_num
-- end,
-- have veryfixed : g^12 • x = x := begin
-- let := smul_zpow_eq_of_smul_eq (12/k) xfixed,
-- rw [← zpow_mul,k_div_12] at this,
-- norm_cast at this
-- end,
-- exact xmoves veryfixed
-- end
lemma proposition_1_1_2 (f g : G) [t2_space α] : is_locally_moving G α → is_algebraically_disjoint f g → disjoint (support α f) (support α (g^12)) := begin
intros locally_moving alg_disjoint,
-- suppose to the contrary that the set U = supp(f) ∩ supp(g^12) is nonempty
by_contra not_disjoint,
let U := support α f ∩ support α (g^12),
have U_nonempty : U.nonempty := set.not_disjoint_iff_nonempty_inter.mp not_disjoint,
-- since X is Hausdorff, we can find a nonempty open set V ⊆ U such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint
let x := U_nonempty.some,
have five_points : function.injective (λi : fin 5, g^(i:ℤ) • x) := moves_1234_of_moves_12 (mem_support.mp $ (set.inter_subset_right _ _) U_nonempty.some_mem),
rcases disjoint_nbhd_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩,
simp only at disjoint_img_V₁,
let V := V₀ ∩ V₁,
-- let h be a nontrivial element of rigid_stabilizer G V, and note that [f,h]≠1 since f(V) is disjoint from V
let ristV_ne_bot := locally_moving V (is_open.inter open_V₀ open_V₁) (set.nonempty_of_mem ⟨x_in_V₀,x_in_V₁⟩),
rcases (or_iff_right ristV_ne_bot).mp (subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩,
have comm_non_trivial : ¬commute f h := begin
by_contra comm_trivial,
rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨z,z_in_V,z_moved⟩,
let act_comm := disjoint_support_comm h f (rist_supported_in_set h_in_ristV) (set.disjoint_of_subset (set.inter_subset_left V₀ V₁) (smul''_subset f (set.inter_subset_left V₀ V₁)) disjoint_img_V₀) z z_in_V,
rw [commutator_element_eq_one_iff_commute.mpr comm_trivial.symm,one_smul] at act_comm,
exact z_moved act_comm.symm,
end,
-- since g is algebraically disjoint from f, there exist f₁,f₂ ∈ C_G(g) so that the commutator h' = [f1,[f2,h]] is a nontrivial element of C_G(g)
rcases alg_disjoint h comm_non_trivial with ⟨f₁,f₂,f₁_commutes,f₂_commutes,h'_commutes,h'_non_trivial⟩,
let h' := ⁅f₁,⁅f₂,h⁆⁆,
-- now observe that supp([f₂, h]) ⊆ V ∪ f₂(V), and by the same reasoning supp(h')⊆V∪f₁(V)∪f₂(V)∪f₁f₂(V)
have support_f₂h : support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := (support_comm α f₂ h).trans (set.union_subset_union (rist_supported_in_set h_in_ristV) $ smul''_subset f₂ $ rist_supported_in_set h_in_ristV),
have support_h' : support α h' ⊆ ⋃(i : fin 2 × fin 2), (f₁^i.1.val*f₂^i.2.val) •'' V := begin
let this := (support_comm α f₁ ⁅f₂,h⁆).trans (set.union_subset_union support_f₂h (smul''_subset f₁ support_f₂h)),
rw [smul''_union,← one_smul'' V,← mul_smul'',← mul_smul'',← mul_smul'',mul_one,mul_one] at this,
let rw_u := rewrite_Union (λi : fin 2 × fin 2, (f₁^i.1.val*f₂^i.2.val) •'' V),
simp only [fin.val_eq_coe, fin.val_zero', pow_zero, mul_one, fin.val_one, pow_one, one_mul] at rw_u,
exact rw_u.symm ▸ this,
end,
-- since h' is nontrivial, it has at least one point p in its support
cases faithful_moves_point' α h'_non_trivial with p p_moves,
-- since g commutes with h', all five of the points {gi(p):i=0..4} lie in supp(h')
have gi_in_support : ∀i : fin 5, g^i.val • p ∈ support α h' := begin
intro i,
rw mem_support,
by_contra p_fixed,
rw [← mul_smul,(h'_commutes.pow_right i.val).eq,mul_smul,smul_left_cancel_iff] at p_fixed,
exact p_moves p_fixed,
end,
-- by the pigeonhole principle, one of the four sets V, f₁(V), f₂(V), f₁f₂(V) must contain two of these points, say g^i(p),g^j(p) ∈ k(V) for some 0 ≤ i < j ≤ 4 and k ∈ {1,f₁,f₂,f₁f₂}
let pigeonhole : fintype.card (fin 5) > fintype.card (fin 2 × fin 2) := dec_trivial,
let choice := λi : fin 5, (set.mem_Union.mp $ support_h' $ gi_in_support i).some,
rcases finset.exists_ne_map_eq_of_card_lt_of_maps_to pigeonhole (λ(i : fin 5) _, finset.mem_univ (choice i)) with ⟨i,_,j,_,i_ne_j,same_choice⟩,
clear h_1_w h_1_h_h_w pigeonhole,
let k := f₁^(choice i).1.val*f₂^(choice i).2.val,
have same_k : f₁^(choice j).1.val*f₂^(choice j).2.val = k := by { simp only at same_choice,
rw ← same_choice },
have g_i : g^i.val • p ∈ k •'' V := (set.mem_Union.mp $ support_h' $ gi_in_support i).some_spec,
have g_j : g^j.val • p ∈ k •'' V := same_k ▸ (set.mem_Union.mp $ support_h' $ gi_in_support j).some_spec,
-- but since g^(j−i)(V) is disjoint from V and k commutes with g, we know that g^(j−i)k(V) is disjoint from k(V), a contradiction since g^i(p) and g^j(p) both lie in k(V).
have g_disjoint : disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := begin
let := (disjoint_smul'' (g^(-(i.val+j.val : ℤ))) (disjoint_img_V₁ i j i_ne_j)).symm,
rw [← mul_smul'',← mul_smul'',← zpow_add,← zpow_add] at this,
simp only [fin.val_eq_coe, neg_add_rev, coe_coe, neg_add_cancel_right, zpow_neg, zpow_coe_nat, neg_add_cancel_comm] at this,
from set.disjoint_of_subset (smul''_subset _ (set.inter_subset_right V₀ V₁)) (smul''_subset _ (set.inter_subset_right V₀ V₁)) this
end,
have k_commutes : commute k g := commute.mul_left (f₁_commutes.pow_left (choice i).1.val) (f₂_commutes.pow_left (choice i).2.val),
have g_k_disjoint : disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := begin
let this := disjoint_smul'' k g_disjoint,
rw [← mul_smul'',← mul_smul'',← inv_pow g i.val,← inv_pow g j.val,
← (k_commutes.symm.inv_left.pow_left i.val).eq,
← (k_commutes.symm.inv_left.pow_left j.val).eq,
mul_smul'',inv_pow g i.val,mul_smul'' (g⁻¹^j.val) k V,inv_pow g j.val] at this,
-- lemma proposition_1_1_2 (f g : G) [t2_space α] : is_locally_moving G α → is_algebraically_disjoint f g → disjoint (support α f) (support α (g^12)) := begin
-- intros locally_moving alg_disjoint,
-- -- suppose to the contrary that the set U = supp(f) ∩ supp(g^12) is nonempty
-- by_contra not_disjoint,
-- let U := support α f ∩ support α (g^12),
-- have U_nonempty : U.nonempty := set.not_disjoint_iff_nonempty_inter.mp not_disjoint,
-- -- since X is Hausdorff, we can find a nonempty open set V ⊆ U such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint
-- let x := U_nonempty.some,
-- have five_points : function.injective (λi : fin 5, g^(i:ℤ) • x) := moves_1234_of_moves_12 (mem_support.mp $ (set.inter_subset_right _ _) U_nonempty.some_mem),
-- rcases disjoint_nbhd_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩,
-- simp only at disjoint_img_V₁,
-- let V := V₀ ∩ V₁,
-- -- let h be a nontrivial element of rigid_stabilizer G V, and note that [f,h]≠1 since f(V) is disjoint from V
-- let ristV_ne_bot := locally_moving V (is_open.inter open_V₀ open_V₁) (set.nonempty_of_mem ⟨x_in_V₀,x_in_V₁⟩),
-- rcases (or_iff_right ristV_ne_bot).mp (subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩,
-- have comm_non_trivial : ¬commute f h := begin
-- by_contra comm_trivial,
-- rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨z,z_in_V,z_moved⟩,
-- let act_comm := disjoint_support_comm h f (rist_supported_in_set h_in_ristV) (set.disjoint_of_subset (set.inter_subset_left V₀ V₁) (smul''_subset f (set.inter_subset_left V₀ V₁)) disjoint_img_V₀) z z_in_V,
-- rw [commutator_element_eq_one_iff_commute.mpr comm_trivial.symm,one_smul] at act_comm,
-- exact z_moved act_comm.symm,
-- end,
-- -- since g is algebraically disjoint from f, there exist f₁,f₂ ∈ C_G(g) so that the commutator h' = [f1,[f2,h]] is a nontrivial element of C_G(g)
-- rcases alg_disjoint h comm_non_trivial with ⟨f₁,f₂,f₁_commutes,f₂_commutes,h'_commutes,h'_non_trivial⟩,
-- let h' := ⁅f₁,⁅f₂,h⁆⁆,
-- -- now observe that supp([f₂, h]) ⊆ V ∪ f₂(V), and by the same reasoning supp(h')⊆V∪f₁(V)∪f₂(V)∪f₁f₂(V)
-- have support_f₂h : support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := (support_comm α f₂ h).trans (set.union_subset_union (rist_supported_in_set h_in_ristV) $ smul''_subset f₂ $ rist_supported_in_set h_in_ristV),
-- have support_h' : support α h' ⊆ ⋃(i : fin 2 × fin 2), (f₁^i.1.val*f₂^i.2.val) •'' V := begin
-- let this := (support_comm α f₁ ⁅f₂,h⁆).trans (set.union_subset_union support_f₂h (smul''_subset f₁ support_f₂h)),
-- rw [smul''_union,← one_smul'' V,← mul_smul'',← mul_smul'',← mul_smul'',mul_one,mul_one] at this,
-- let rw_u := rewrite_Union (λi : fin 2 × fin 2, (f₁^i.1.val*f₂^i.2.val) •'' V),
-- simp only [fin.val_eq_coe, fin.val_zero', pow_zero, mul_one, fin.val_one, pow_one, one_mul] at rw_u,
-- exact rw_u.symm ▸ this,
-- end,
-- -- since h' is nontrivial, it has at least one point p in its support
-- cases faithful_moves_point' α h'_non_trivial with p p_moves,
-- -- since g commutes with h', all five of the points {gi(p):i=0..4} lie in supp(h')
-- have gi_in_support : ∀i : fin 5, g^i.val • p ∈ support α h' := begin
-- intro i,
-- rw mem_support,
-- by_contra p_fixed,
-- rw [← mul_smul,(h'_commutes.pow_right i.val).eq,mul_smul,smul_left_cancel_iff] at p_fixed,
-- exact p_moves p_fixed,
-- end,
-- -- by the pigeonhole principle, one of the four sets V, f₁(V), f₂(V), f₁f₂(V) must contain two of these points, say g^i(p),g^j(p) ∈ k(V) for some 0 ≤ i < j ≤ 4 and k ∈ {1,f₁,f₂,f₁f₂}
-- let pigeonhole : fintype.card (fin 5) > fintype.card (fin 2 × fin 2) := dec_trivial,
-- let choice := λi : fin 5, (set.mem_Union.mp $ support_h' $ gi_in_support i).some,
-- rcases finset.exists_ne_map_eq_of_card_lt_of_maps_to pigeonhole (λ(i : fin 5) _, finset.mem_univ (choice i)) with ⟨i,_,j,_,i_ne_j,same_choice⟩,
-- clear h_1_w h_1_h_h_w pigeonhole,
-- let k := f₁^(choice i).1.val*f₂^(choice i).2.val,
-- have same_k : f₁^(choice j).1.val*f₂^(choice j).2.val = k := by { simp only at same_choice,
-- rw ← same_choice },
-- have g_i : g^i.val • p ∈ k •'' V := (set.mem_Union.mp $ support_h' $ gi_in_support i).some_spec,
-- have g_j : g^j.val • p ∈ k •'' V := same_k ▸ (set.mem_Union.mp $ support_h' $ gi_in_support j).some_spec,
-- -- but since g^(j−i)(V) is disjoint from V and k commutes with g, we know that g^(j−i)k(V) is disjoint from k(V), a contradiction since g^i(p) and g^j(p) both lie in k(V).
-- have g_disjoint : disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := begin
-- let := (disjoint_smul'' (g^(-(i.val+j.val : ℤ))) (disjoint_img_V₁ i j i_ne_j)).symm,
-- rw [← mul_smul'',← mul_smul'',← zpow_add,← zpow_add] at this,
-- simp only [fin.val_eq_coe, neg_add_rev, coe_coe, neg_add_cancel_right, zpow_neg, zpow_coe_nat, neg_add_cancel_comm] at this,
-- from set.disjoint_of_subset (smul''_subset _ (set.inter_subset_right V₀ V₁)) (smul''_subset _ (set.inter_subset_right V₀ V₁)) this
-- end,
-- have k_commutes : commute k g := commute.mul_left (f₁_commutes.pow_left (choice i).1.val) (f₂_commutes.pow_left (choice i).2.val),
-- have g_k_disjoint : disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := begin
-- let this := disjoint_smul'' k g_disjoint,
-- rw [← mul_smul'',← mul_smul'',← inv_pow g i.val,← inv_pow g j.val,
