internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ 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
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ s
Tactic:
intro ha'
Proof 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
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
ha' : a ∈ support c
⊢ 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
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ s
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
ha' : a ∈ support c
⊢ 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
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ s
Tactic:
exact ha (hc ha')
Proof 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
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ s
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ s
Tactic:
exact ha
Proof state after:
no goals
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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)
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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⟩
Proof 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 })
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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 })
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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)
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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'
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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'
Proof 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
Theorem: Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ Commute g c ↔ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c
Tactic:
rw [Equiv.Perm.IsCycle.commute_iff' hc]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ (∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
      subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)) ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ (∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
      subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)) ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c
Tactic:
apply exists_congr
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ ∀ (a : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
    subtypePerm g a ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ ofSubtype (subtypePerm g a) ∈ Subgroup.zpowers c
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ ∀ (a : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
    subtypePerm g a ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ ofSubtype (subtypePerm g a) ∈ Subgroup.zpowers c
Tactic:
intro hc'
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
⊢ subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
⊢ subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c
Tactic:
simp only [Subgroup.mem_zpowers_iff]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
⊢ (∃ k, subtypePermOfSupport c ^ k = subtypePerm g hc') ↔ ∃ k, c ^ k = ofSubtype (subtypePerm g hc')
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
⊢ (∃ k, subtypePermOfSupport c ^ k = subtypePerm g hc') ↔ ∃ k, c ^ k = ofSubtype (subtypePerm g hc')
Tactic:
apply exists_congr
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
⊢ ∀ (a : ℤ), subtypePermOfSupport c ^ a = subtypePerm g hc' ↔ c ^ a = ofSubtype (subtypePerm g hc')
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
⊢ ∀ (a : ℤ), subtypePermOfSupport c ^ a = subtypePerm g hc' ↔ c ^ a = ofSubtype (subtypePerm g hc')
Tactic:
intro k
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePermOfSupport c ^ k = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')