-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.support_congr (hf : IsCycle f) (hg : IsCycle g) (h : f.support ⊆ g.support)
    (h' : ∀ x ∈ f.support, f x = g x) : f = g

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
this : f.support = g.support
⊢ ∀ x ∈ g.support, f x = g x

Tactic:
simpa [← this] using h'

Result:
no goals

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
⊢ z ∈ f.support

Tactic:
obtain ⟨x, hx, _⟩ := id hf

Result:
case intro.intro
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ z ∈ f.support

Proof state:
case intro.intro
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
⊢ z ∈ f.support

Tactic:
obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)

Result:
case intro.intro.intro
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
⊢ z ∈ f.support

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x✝ : α
hx✝ : f x✝ ≠ x✝
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x✝ y
hx' : g x✝ ≠ x✝
m : ℕ
hm : (g ^ m) x✝ = z
x : α
hx : x ∈ f.support ∩ g.support
⊢ f x = g x

Tactic:
exact h' x (mem_of_mem_inter_left hx)

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
h'' : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ z ∈ f.support

Tactic:
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]

Result:
no goals

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
this : f.support = g.support
⊢ f = g

Tactic:
refine Equiv.Perm.support_congr h ?_

Result:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
this : f.support = g.support
⊢ ∀ x ∈ g.support, f x = g x

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
⊢ f.support = g.support

Tactic:
refine le_antisymm h ?_

Result:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
⊢ g.support ≤ f.support

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
⊢ g.support ≤ f.support

Tactic:
intro z hz

Result:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
⊢ z ∈ f.support

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
⊢ ∀ x ∈ f.support ∩ g.support, f x = g x

Tactic:
intro x hx

Result:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x✝ : α
hx✝ : f x✝ ≠ x✝
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x✝ y
hx' : g x✝ ≠ x✝
m : ℕ
hm : (g ^ m) x✝ = z
x : α
hx : x ∈ f.support ∩ g.support
⊢ f x = g x

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
⊢ f = g

Tactic:
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]

Result:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
this : f.support = g.support
⊢ f = g

Proof state:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ g x ≠ x

Tactic:
rwa [← h' x (mem_support.mpr hx)]

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ z ∈ f.support

Tactic:
have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]

Result:
case intro.intro
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
⊢ z ∈ f.support

Proof state:
case intro.intro.intro
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
⊢ z ∈ f.support

Tactic:
have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
  intro x hx
  exact h' x (mem_of_mem_inter_left hx)

Result:
case intro.intro.intro
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
h'' : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ z ∈ f.support