internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
Proof state before:
case pos.hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Tactic:
cases' hm with hm hm
Proof state after:
case pos.hnc.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
Proof state before:
case pos.hnc.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Tactic:
exact hm
Proof state after:
case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
Proof state before:
case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Tactic:
exfalso
Proof state after:
case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ False

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
Proof state before:
case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ False

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Tactic:
exact hm hm'
Proof state after:
case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
Proof state before:
case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Tactic:
exact hm'
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
      (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
    else 0) =
    0
Tactic:
rw [if_neg]
Proof state after:
case neg.hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬Even (Multiset.sum m + Multiset.card m)
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
Proof state before:
case neg.hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬Even (Multiset.sum m + Multiset.card m)
Tactic:
exact hm'
Proof state after:
no goals
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
⊢ (θ g) (k, 1) = Equiv.Perm.ofSubtype k
Tactic:
ext x
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Tactic:
by_cases hx : g.cycleOf x ∈ g.cycleFactorsFinset
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [hθ_2 _ x ⟨g.cycleOf x, hx⟩ rfl]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((k, 1).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = (Equiv.Perm.ofSubtype k) x
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((k, 1).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = (Equiv.Perm.ofSubtype k) x
Tactic:
simp only [Pi.one_apply, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ x = (Equiv.Perm.ofSubtype k) x
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem]
Proof state after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ x ∉ MulAction.fixedBy α g
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ x ∉ MulAction.fixedBy α g
Tactic:
simp only [MulAction.mem_fixedBy, Equiv.Perm.smul_def, ← Equiv.Perm.mem_support, ← Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff]
Proof state after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.not_mem_support] at hx
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [hθ_1 _ x hx, Equiv.Perm.ofSubtype_apply_of_mem]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ ↑((k, 1).1 { val := x, property := hx }) = ↑(k { val := x, property := ?neg.ha✝ })

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ x ∈ MulAction.fixedBy α g
Theorem: OnCycleFactors.θ_apply_fst
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ ↑((k, 1).1 { val := x, property := hx }) = ↑(k { val := x, property := ?neg.ha✝ })

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ x ∈ MulAction.fixedBy α g
Tactic:
rfl
Proof state after:
no goals
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
⊢ (θ g) (1, Pi.mulSingle c vc) = ↑vc
Tactic:
ext x
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x
Tactic:
by_cases hx : g.cycleOf x ∈ g.cycleFactorsFinset
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x
Tactic:
rw [hθ_2 _ x ⟨g.cycleOf x, hx⟩ rfl]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
by_cases hc : g.cycleOf x = c
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
suffices c = ⟨g.cycleOf x, hx⟩ by
  rw [← this]
  simp only [Pi.mulSingle_eq_same]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ c = { val := Equiv.Perm.cycleOf g x, property := hx }
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ c = { val := Equiv.Perm.cycleOf g x, property := hx }
Tactic:
rw [← Subtype.coe_inj, ← hc]
Proof state after:
no goals
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
this : c = { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
rw [← this]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
this : c = { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ↑((1, Pi.mulSingle c vc).2 c) x = ↑vc x
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
this : c = { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ↑((1, Pi.mulSingle c vc).2 c) x = ↑vc x
Tactic:
simp only [Pi.mulSingle_eq_same]
Proof state after:
no goals
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
simp only [ne_eq]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑(Pi.mulSingle c vc { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑(Pi.mulSingle c vc { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
rw [Pi.mulSingle_eq_of_ne]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑1 x = ↑vc x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c