internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ z x = ↑(v { val := c, property := hc }) x

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Tactic:
rw [← h, hθ_2 _ x ⟨c, hc⟩]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ Equiv.Perm.cycleOf g x = ↑{ val := c, property := hc }

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ Equiv.Perm.cycleOf g x = ↑{ val := c, property := hc }

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Tactic:
exact (Equiv.Perm.cycle_is_cycleOf hx hc).symm
Proof state after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ (Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc')) x = ↑(v { val := c, property := hc }) x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
obtain ⟨m, hm⟩ := (v ⟨c, hc⟩).prop
Proof state after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : (fun x => ↑{ val := c, property := hc } ^ x) m = ↑(v { val := c, property := hc })
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : (fun x => ↑{ val := c, property := hc } ^ x) m = ↑(v { val := c, property := hc })
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
dsimp only at hm
Proof state after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
rw [← hm]
Proof state after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x = (c ^ m) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x = (c ^ m) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
apply symm
Proof state after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ (c ^ m) x = x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ (c ^ m) x = x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
rw [← Equiv.Perm.not_mem_support]
Proof state after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x ∉ Equiv.Perm.support (c ^ m)

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x ∉ Equiv.Perm.support (c ^ m)

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
intro hx'
Proof state after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
hx' : x ∈ Equiv.Perm.support (c ^ m)
⊢ False

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
hx' : x ∈ Equiv.Perm.support (c ^ m)
⊢ False

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
apply hx
Proof state after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
hx' : x ∈ Equiv.Perm.support (c ^ m)
⊢ x ∈ Equiv.Perm.support c

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
hx' : x ∈ Equiv.Perm.support (c ^ m)
⊢ x ∈ Equiv.Perm.support c

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
exact (Equiv.Perm.support_zpow_le c m) hx'
Proof state after:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.hψ_range_card'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(Set.range ⇑(θ g)) = Fintype.card ↥(MonoidHom.ker (φ g))
Tactic:
let u : (Set.range (θ g)) → (φ g).ker := fun ⟨z, hz⟩ => by
  rw [← hφ_ker_eq_θ_range] at hz
  suffices ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g by
    use ⟨ConjAct.toConjAct z, this⟩
    have hK : Function.Injective (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g).subtype := by
      apply Subgroup.subtype_injective
    rw [← Subgroup.mem_map_iff_mem hK]
    simp only [Subgroup.coeSubtype, Subgroup.coe_mk]
    exact hz
  obtain ⟨u, ⟨_, hu'⟩⟩ := hz
  rw [← hu']
  exact u.prop
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Fintype.card ↑(Set.range ⇑(θ g)) = Fintype.card ↥(MonoidHom.ker (φ g))