no goals
α : Type u_2
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_1
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ cycleType (extendDomain g f) = cycleType g
induction g using cycle_induction_on with
| base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
| base_cycles σ hσ =>
  rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
| induction_disjoint σ τ hd _ hσ hτ =>
  rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]
no goals
case base_one
α : Type u_2
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_1
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ cycleType (extendDomain 1 f) = cycleType 1
rw [extendDomain_one, cycleType_one, cycleType_one]
no goals
case base_cycles
α : Type u_2
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_1
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ : Perm α
hσ : IsCycle σ
⊢ cycleType (extendDomain σ f) = cycleType σ
rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
no goals
case induction_disjoint
α : Type u_2
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_1
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : cycleType (extendDomain σ f) = cycleType σ
hτ : cycleType (extendDomain τ f) = cycleType τ
⊢ cycleType (extendDomain (σ * τ) f) = cycleType (σ * τ)
rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]