Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
⊢ c ^ n = ofSubtype (subtypePerm g hg) ↔ subtypePerm c ⋯ ^ n = subtypePerm g hg
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
⊢ c ^ n = ofSubtype (subtypePerm g hg) → subtypePerm c ⋯ ^ n = subtypePerm g hg

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

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
⊢ c ^ n = ofSubtype (subtypePerm g hg) → subtypePerm c ⋯ ^ n = subtypePerm g hg
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
⊢ subtypePerm c ⋯ ^ n = subtypePerm g hg

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
⊢ subtypePerm c ⋯ ^ n = subtypePerm g hg
Tactic:
ext ⟨x, hx⟩
State after:
case mp.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
⊢ ↑((subtypePerm c ⋯ ^ n) { val := x, property := hx }) = ↑((subtypePerm g hg) { val := x, property := hx })

State before:
case mp.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
⊢ ↑((subtypePerm c ⋯ ^ n) { val := x, property := hx }) = ↑((subtypePerm g hg) { val := x, property := hx })
Tactic:
let h' := Equiv.Perm.congr_fun h x
State after:
case mp.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ ↑((subtypePerm c ⋯ ^ n) { val := x, property := hx }) = ↑((subtypePerm g hg) { val := x, property := hx })

State before:
case mp.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ ↑((subtypePerm c ⋯ ^ n) { val := x, property := hx }) = ↑((subtypePerm g hg) { val := x, property := hx })
Tactic:
simp only [h', Equiv.Perm.subtypePerm_apply_zpow_of_mem, Subtype.coe_mk,
  Equiv.Perm.subtypePerm_apply]
State after:
case mp.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ (ofSubtype (subtypePerm g hg)) x = g x

State before:
case mp.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ (ofSubtype (subtypePerm g hg)) x = g x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem]
State after:
case mp.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ ↑((subtypePerm g hg) { val := x, property := ?mp.H.mk.a.ha }) = g x

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

State before:
case mp.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ ↑((subtypePerm g hg) { val := x, property := ?mp.H.mk.a.ha }) = g x

case mp.H.mk.a.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ x ∈ s
Tactic:
simp only [Subtype.coe_mk, Equiv.Perm.subtypePerm_apply]
State after:
case mp.H.mk.a.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ x ∈ s

State before:
case mp.H.mk.a.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : c ^ n = ofSubtype (subtypePerm g hg)
x : α
hx : x ∈ s
h' : (c ^ n) x = (ofSubtype (subtypePerm g hg)) x := Perm.congr_fun h x
⊢ x ∈ s
Tactic:
exact hx
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm g hg → c ^ n = ofSubtype (subtypePerm g hg)
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
⊢ c ^ n = ofSubtype (subtypePerm g hg)

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

State before:
case mpr.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
⊢ (c ^ n) x = (ofSubtype (subtypePerm g hg)) x
Tactic:
rw [← h]
State after:
case mpr.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
⊢ (c ^ n) x = (ofSubtype (subtypePerm c ⋯ ^ n)) x

State before:
case mpr.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
⊢ (c ^ n) x = (ofSubtype (subtypePerm c ⋯ ^ n)) x
Tactic:
by_cases hx : x ∈ s
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = (ofSubtype (subtypePerm c ⋯ ^ n)) x

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

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = (ofSubtype (subtypePerm c ⋯ ^ n)) x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = ↑((subtypePerm c ⋯ ^ n) { val := x, property := ?pos.ha✝ })

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

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = ↑((subtypePerm c ⋯ ^ n) { val := x, property := ?pos.ha✝ })

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∈ s
⊢ x ∈ s
Tactic:
simp only [subtypePerm_zpow, subtypePerm_apply]
State after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∈ s
⊢ x ∈ s

State before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∈ s
⊢ x ∈ s
Tactic:
exact hx
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
⊢ (c ^ n) x = (ofSubtype (subtypePerm c ⋯ ^ n)) x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
⊢ (c ^ n) x = x

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

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

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
⊢ x ∉ s
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
⊢ x ∉ support (c ^ n)

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

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

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
⊢ x ∉ s
Tactic:
intro hx'
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
hx' : x ∈ support (c ^ n)
⊢ False

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

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

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

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

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

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
⊢ x ∉ s
Tactic:
apply hc
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
hx' : x ∈ support (c ^ n)
⊢ x ∈ support c

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

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

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
⊢ x ∉ s
Tactic:
apply Equiv.Perm.support_zpow_le
State after:
case neg.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
hx' : x ∈ support (c ^ n)
⊢ x ∈ support (c ^ ?neg.a.n✝)

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

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

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

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

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

State before:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ⊆ s
n : ℤ
h : subtypePerm c ⋯ ^ n = subtypePerm g hg
x : α
hx : x ∉ s
⊢ x ∉ s
Tactic:
exact hx
State after:
no goals