-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem zpow_eq_ofSubtype_subtypePerm_iff
    {g c : Equiv.Perm α} {s : Finset α}
    (hg : ∀ x, x ∈ s ↔ g x ∈ s) (hc : c.support ⊆ s) (n : ℤ) :
    c ^ n = ofSubtype (g.subtypePerm hg) ↔
      c.subtypePerm (isInvariant_of_support_le hc) ^ n = g.subtypePerm hg

Proof state:
case mpr.H
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Tactic:
by_cases hx : x ∈ s

Result:
case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Proof state:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ x ∉ (c ^ n).support

Tactic:
exact fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c ^ n = ofSubtype (g.subtypePerm hg) → c.subtypePerm ⋯ ^ n = g.subtypePerm hg

Tactic:
intro h

Result:
case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg

Proof state:
case mpr.H
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
⊢ (c ^ n) x = (ofSubtype (g.subtypePerm hg)) x

Tactic:
rw [← h]

Result:
case mpr.H
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Proof state:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)

Tactic:
intro h

Result:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
⊢ c ^ n = ofSubtype (g.subtypePerm hg)

Proof state:
case mp.H.mk.a.ha
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
x : α
hx : x ∈ s
⊢ x ∈ s

Tactic:
exact hx

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c ^ n = ofSubtype (g.subtypePerm hg) ↔ c.subtypePerm ⋯ ^ n = g.subtypePerm hg

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c ^ n = ofSubtype (g.subtypePerm hg) → c.subtypePerm ⋯ ^ n = g.subtypePerm hg

case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)

Proof state:
case mp.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
x : α
hx : x ∈ s
⊢ ↑((g.subtypePerm hg) ⟨x, ?mp.H.mk.a.ha⟩) = g x

Tactic:
simp only [Subtype.coe_mk, subtypePerm_apply]

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Tactic:
rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
  subtypePerm_zpow, subtypePerm_apply]

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
⊢ c ^ n = ofSubtype (g.subtypePerm hg)

Tactic:
ext x

Result:
case mpr.H
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
⊢ (c ^ n) x = (ofSubtype (g.subtypePerm hg)) x

Proof state:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Tactic:
rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,
  ← not_mem_support]

Result:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ x ∉ (c ^ n).support

Proof state:
case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg

Tactic:
ext ⟨x, hx⟩

Result:
case mp.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
x : α
hx : x ∈ s
⊢ ↑((c.subtypePerm ⋯ ^ n) ⟨x, hx⟩) = ↑((g.subtypePerm hg) ⟨x, hx⟩)

Proof state:
case mp.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
x : α
hx : x ∈ s
⊢ ↑((c.subtypePerm ⋯ ^ n) ⟨x, hx⟩) = ↑((g.subtypePerm hg) ⟨x, hx⟩)

Tactic:
simp only [Perm.congr_fun h x, subtypePerm_apply_zpow_of_mem, Subtype.coe_mk, subtypePerm_apply]

Result:
case mp.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
x : α
hx : x ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) x = g x

Proof state:
case mp.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
x : α
hx : x ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) x = g x

Tactic:
rw [ofSubtype_apply_of_mem]

Result:
case mp.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
x : α
hx : x ∈ s
⊢ ↑((g.subtypePerm hg) ⟨x, ?mp.H.mk.a.ha⟩) = g x

case mp.H.mk.a.ha
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = ofSubtype (g.subtypePerm hg)
x : α
hx : x ∈ s
⊢ x ∈ s