ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
⊢ f = g
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
⊢ f = g
have hx'' : x ∈ g.support := by rwa [mem_support, ← hx, ← mem_support]
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
this : support f ⊆ support g
⊢ f = g
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
⊢ f = g
have : f.support ⊆ g.support := by
  intro y hy
  obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
  rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
this : support f ⊆ support g
⊢ f = g
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
this : support f ⊆ support g
⊢ f = g
rw [(inter_eq_left_iff_subset _ _).mpr this] at h
no goals
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
this : support f ⊆ support g
⊢ f = g
exact hf.support_congr hg this h
no goals
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
⊢ x ∈ support g
rwa [mem_support, ← hx, ← mem_support]
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
y : α
hy : y ∈ support f
⊢ y ∈ support g
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
⊢ support f ⊆ support g
intro y hy
case intro
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
k : ℕ
hy : ↑(f ^ k) x ∈ support f
⊢ ↑(f ^ k) x ∈ support g
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
y : α
hy : y ∈ support f
⊢ y ∈ support g
obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
no goals
case intro
ι : Type ?u.1125909
α : Type u_1
β : Type ?u.1125915
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
hx : ↑f x = ↑g x
hx' : x ∈ support f
hx'' : x ∈ support g
k : ℕ
hy : ↑(f ^ k) x ∈ support f
⊢ ↑(f ^ k) x ∈ support g
rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]