internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ ∀ x ∈ cycleFactorsFinset g, Commute k x
Tactic:
exact hk
Proof state after:
no goals
Theorem: Equiv.Perm.self_mem_cycle_factors_commute
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ Commute c g
Tactic:
apply Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute
Proof state after:
case hk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ ∀ c_1 ∈ cycleFactorsFinset g, Commute c c_1
Theorem: Equiv.Perm.self_mem_cycle_factors_commute
Proof state before:
case hk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ ∀ c_1 ∈ cycleFactorsFinset g, Commute c c_1
Tactic:
intro c' hc'
Proof state after:
case hk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
⊢ Commute c c'
Theorem: Equiv.Perm.self_mem_cycle_factors_commute
Proof state before:
case hk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
⊢ Commute c c'
Tactic:
by_cases hcc' : c = c'
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : c = c'
⊢ Commute c c'

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ Commute c c'
Theorem: Equiv.Perm.self_mem_cycle_factors_commute
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : c = c'
⊢ Commute c c'

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ Commute c c'
Tactic:
rw [hcc']
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ Commute c c'
Theorem: Equiv.Perm.self_mem_cycle_factors_commute
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ Commute c c'
Tactic:
apply g.cycleFactorsFinset_mem_commute hc hc'
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ c ≠ c'
Theorem: Equiv.Perm.self_mem_cycle_factors_commute
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ c ≠ c'
Tactic:
exact hcc'
Proof state after:
no goals
Theorem: Equiv.Perm.mem_support_of_commute
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
⊢ ∀ (x : α), x ∈ support c ↔ g x ∈ support c
Tactic:
intro x
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ x ∈ support c ↔ g x ∈ support c
Theorem: Equiv.Perm.mem_support_of_commute
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ x ∈ support c ↔ g x ∈ support c
Tactic:
simp only [Equiv.Perm.mem_support, not_iff_not, ← Equiv.Perm.mul_apply]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ (c * g) x = g x
Theorem: Equiv.Perm.mem_support_of_commute
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ (c * g) x = g x
Tactic:
rw [← hgc, Equiv.Perm.mul_apply]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ g (c x) = g x
Theorem: Equiv.Perm.mem_support_of_commute
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ g (c x) = g x
Tactic:
exact (Equiv.apply_eq_iff_eq g).symm
Proof state after:
no goals
Theorem: Equiv.Perm.mem_support_cycle_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
⊢ ∀ (x : α), x ∈ support c ↔ d x ∈ support c
Tactic:
intro x
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
⊢ x ∈ support c ↔ d x ∈ support c
Theorem: Equiv.Perm.mem_support_cycle_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
⊢ x ∈ support c ↔ d x ∈ support c
Tactic:
simp only [Equiv.Perm.mem_support, not_iff_not]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
⊢ c x = x ↔ c (d x) = d x
Theorem: Equiv.Perm.mem_support_cycle_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
⊢ c x = x ↔ c (d x) = d x
Tactic:
by_cases h : c = d
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : c = d
⊢ c x = x ↔ c (d x) = d x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x
Theorem: Equiv.Perm.mem_support_cycle_of_cycle
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : c = d
⊢ c x = x ↔ c (d x) = d x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x
Tactic:
rw [← h, EmbeddingLike.apply_eq_iff_eq]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x
Theorem: Equiv.Perm.mem_support_cycle_of_cycle
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x
Tactic:
rw [← Equiv.Perm.mul_apply,
    Commute.eq (Equiv.Perm.cycleFactorsFinset_mem_commute g hc hd h),
    Equiv.Perm.mul_apply, EmbeddingLike.apply_eq_iff_eq]
Proof state after:
no goals
Theorem: Equiv.Perm.mem_cycleFactorsFinset_support
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
a : α
⊢ a ∈ support c ↔ g a ∈ support c
Tactic:
apply Equiv.Perm.mem_support_of_commute
Proof state after:
case hgc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
a : α
⊢ Commute g c
Theorem: Equiv.Perm.mem_cycleFactorsFinset_support
Proof state before:
case hgc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
a : α
⊢ Commute g c
Tactic:
exact (Equiv.Perm.self_mem_cycle_factors_commute hc).symm
Proof state after:
no goals
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ ↑c = Equiv.Perm.cycleOf g x ↔ Equiv.Perm.SameCycle g y x
Tactic:
rw [Equiv.Perm.cycle_is_cycleOf hy c.prop]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x ↔ Equiv.Perm.SameCycle g y x
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x ↔ Equiv.Perm.SameCycle g y x
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x → Equiv.Perm.SameCycle g y x

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.SameCycle g y x → Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x → Equiv.Perm.SameCycle g y x
Tactic:
intro hx'
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Equiv.Perm.SameCycle g y x
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Equiv.Perm.SameCycle g y x
Tactic:
apply And.left
Proof state after:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Equiv.Perm.SameCycle g y x ∧ ?mp.b

case mp.b
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Prop
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Equiv.Perm.SameCycle g y x ∧ ?mp.b

case mp.b
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Prop
Tactic:
rw [← Equiv.Perm.mem_support_cycleOf_iff]
Proof state after:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g y)
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g y)
Tactic:
rw [hx', Equiv.Perm.mem_support, Equiv.Perm.cycleOf_apply_self, ← Equiv.Perm.mem_support]
Proof state after:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ x ∈ Equiv.Perm.support g
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ x ∈ Equiv.Perm.support g
Tactic:
exact hx
Proof state after:
no goals
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.SameCycle g y x → Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
Tactic:
intro hxy
Proof state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hxy : Equiv.Perm.SameCycle g y x
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
Theorem: Equiv.Perm.eq_cycleOf_iff_sameCycle
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hxy : Equiv.Perm.SameCycle g y x
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
Tactic:
rw [Equiv.Perm.SameCycle.cycleOf_eq hxy]
Proof state after:
no goals
Theorem: Equiv.Perm.SameCycle.eq_cycleOf
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : Equiv.Perm.SameCycle g y x
hy : y ∈ Equiv.Perm.support ↑c
⊢ ↑c = Equiv.Perm.cycleOf g x
Tactic:
rw [Equiv.Perm.cycle_is_cycleOf hy c.prop, Equiv.Perm.SameCycle.cycleOf_eq hx]
Proof state after:
no goals
Theorem: Equiv.Perm.sameCycle_of_mem_support
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∃ c, ∀ y ∈ Equiv.Perm.support ↑c, Equiv.Perm.SameCycle g y x
Tactic:
use ⟨g.cycleOf x, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx⟩
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∀ y ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }, Equiv.Perm.SameCycle g y x
Theorem: Equiv.Perm.sameCycle_of_mem_support
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∀ y ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }, Equiv.Perm.SameCycle g y x
Tactic:
intro y hy
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
y : α
hy : y ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }
⊢ Equiv.Perm.SameCycle g y x
Theorem: Equiv.Perm.sameCycle_of_mem_support
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
y : α
hy : y ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }
⊢ Equiv.Perm.SameCycle g y x
Tactic:
rw [← Equiv.Perm.eq_cycleOf_iff_sameCycle hx hy]
Proof state after:
no goals
Theorem: Equiv.Perm.subtypePerm_apply_pow_of_mem
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
Tactic:
revert x
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
Theorem: Equiv.Perm.subtypePerm_apply_pow_of_mem
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
Tactic:
induction' n with n hrec
Proof state after:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ Nat.zero) { val := x, property := hx }) = (g ^ Nat.zero) x

case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ Nat.succ n) { val := x, property := hx }) = (g ^ Nat.succ n) x
Theorem: Equiv.Perm.subtypePerm_apply_pow_of_mem
Proof state before:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ Nat.zero) { val := x, property := hx }) = (g ^ Nat.zero) x
Tactic:
intro x hx
Proof state after:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ Nat.zero) { val := x, property := hx }) = (g ^ Nat.zero) x
Theorem: Equiv.Perm.subtypePerm_apply_pow_of_mem
Proof state before:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ Nat.zero) { val := x, property := hx }) = (g ^ Nat.zero) x
Tactic:
simp only [pow_zero, Equiv.Perm.coe_one, id.def, Subtype.coe_mk]
Proof state after:
no goals
Theorem: Equiv.Perm.subtypePerm_apply_pow_of_mem
Proof state before:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ Nat.succ n) { val := x, property := hx }) = (g ^ Nat.succ n) x
Tactic:
intro x hx
Proof state after:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ Nat.succ n) { val := x, property := hx }) = (g ^ Nat.succ n) x
Theorem: Equiv.Perm.subtypePerm_apply_pow_of_mem
Proof state before:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ Nat.succ n) { val := x, property := hx }) = (g ^ Nat.succ n) x
Tactic:
simp only [pow_succ, Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ n) ((subtypePerm g hs) { val := x, property := hx })) = (g ^ n) (g x)
Theorem: Equiv.Perm.subtypePerm_apply_pow_of_mem
Proof state before:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ n) ((subtypePerm g hs) { val := x, property := hx })) = (g ^ n) (g x)
Tactic:
apply hrec
Proof state after:
no goals
Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
i : ℤ
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ i) { val := x, property := hx }) = (g ^ i) x
Tactic:
induction' i with i i
Proof state after:
case ofNat
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.ofNat i) { val := x, property := hx }) = (g ^ Int.ofNat i) x

case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.negSucc i) { val := x, property := hx }) = (g ^ Int.negSucc i) x
Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem
Proof state before:
case ofNat
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.ofNat i) { val := x, property := hx }) = (g ^ Int.ofNat i) x

case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.negSucc i) { val := x, property := hx }) = (g ^ Int.negSucc i) x
Tactic:
apply Equiv.Perm.subtypePerm_apply_pow_of_mem
Proof state after:
case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.negSucc i) { val := x, property := hx }) = (g ^ Int.negSucc i) x
Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem
Proof state before:
case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.negSucc i) { val := x, property := hx }) = (g ^ Int.negSucc i) x
Tactic:
simp only [zpow_negSucc]
Proof state after:
case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = (g ^ (i + 1))⁻¹ x
Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem
Proof state before:
case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = (g ^ (i + 1))⁻¹ x
Tactic:
apply Equiv.injective (g ^ (i + 1))
Proof state after:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ (g ^ (i + 1)) ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = (g ^ (i + 1)) ((g ^ (i + 1))⁻¹ x)
Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem
Proof state before:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ (g ^ (i + 1)) ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = (g ^ (i + 1)) ((g ^ (i + 1))⁻¹ x)
Tactic:
simp only [Equiv.Perm.apply_inv_self]
Proof state after:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ (g ^ (i + 1)) ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = x