ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
this : support f = support g
⊢ f = g
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
⊢ f = g
have : f.support = g.support := by
  refine' le_antisymm h _
  intro z hz
  obtain ⟨x, hx, _⟩ := id hf
  have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
  obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
  have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
    intro x hx
    exact h' x (mem_of_mem_inter_left hx)
  rwa [← hm, ←
    pow_eq_on_of_mem_support h'' _ x
      (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
    pow_apply_mem_support, mem_support]
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
this : support f = support g
⊢ ∀ (x : α), x ∈ support g → ↑f x = ↑g x
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
this : support f = support g
⊢ f = g
refine' Equiv.Perm.support_congr h _
no goals
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
this : support f = support g
⊢ ∀ (x : α), x ∈ support g → ↑f x = ↑g x
simpa [← this] using h'
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
⊢ support g ≤ support f
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
⊢ support f = support g
refine' le_antisymm h _
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
⊢ z ∈ support f
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
⊢ support g ≤ support f
intro z hz
case intro.intro
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ z ∈ support f
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
⊢ z ∈ support f
obtain ⟨x, hx, _⟩ := id hf
case intro.intro
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
hx' : ↑g x ≠ x
⊢ z ∈ support f
case intro.intro
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ z ∈ support f
have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
case intro.intro.intro
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
hx' : ↑g x ≠ x
m : ℕ
hm : ↑(g ^ m) x = z
⊢ z ∈ support f
case intro.intro
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
hx' : ↑g x ≠ x
⊢ z ∈ support f
obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
case intro.intro.intro
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
hx' : ↑g x ≠ x
m : ℕ
hm : ↑(g ^ m) x = z
h'' : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
⊢ z ∈ support f
case intro.intro.intro
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
hx' : ↑g x ≠ x
m : ℕ
hm : ↑(g ^ m) x = z
⊢ z ∈ support f
have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
  intro x hx
  exact h' x (mem_of_mem_inter_left hx)
no goals
case intro.intro.intro
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
hx' : ↑g x ≠ x
m : ℕ
hm : ↑(g ^ m) x = z
h'' : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
⊢ z ∈ support f
rwa [← hm, ←
  pow_eq_on_of_mem_support h'' _ x
    (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
  pow_apply_mem_support, mem_support]
no goals
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ ↑g x ≠ x
rwa [← h' x (mem_support.mpr hx)]
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x✝ : α
hx✝ : ↑f x✝ ≠ x✝
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x✝ y
hx' : ↑g x✝ ≠ x✝
m : ℕ
hm : ↑(g ^ m) x✝ = z
x : α
hx : x ∈ support f ∩ support g
⊢ ↑f x = ↑g x
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x : α
hx : ↑f x ≠ x
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
hx' : ↑g x ≠ x
m : ℕ
hm : ↑(g ^ m) x = z
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
intro x hx
no goals
ι : Type ?u.1119536
α : Type u_1
β : Type ?u.1119542
f g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
hg : IsCycle g
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support f → ↑f x = ↑g x
z : α
hz : z ∈ support g
x✝ : α
hx✝ : ↑f x✝ ≠ x✝
right✝ : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x✝ y
hx' : ↑g x✝ ≠ x✝
m : ℕ
hm : ↑(g ^ m) x✝ = z
x : α
hx : x ∈ support f ∩ support g
⊢ ↑f x = ↑g x
exact h' x (mem_of_mem_inter_left hx)