ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f ∈ cycleFactorsFinset g
⊢ cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}
revert f
case refine'_1
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ fun {g} => ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}

case refine'_2
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ : Perm α),
    IsCycle σ → fun {g} =>
      ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}

case refine'_3
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ τ : Perm α),
    Disjoint σ τ →
      IsCycle σ →
        (fun {g} =>
            ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) →
          (fun {g} =>
              ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) →
            fun {g} =>
            ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}
refine'
  cycle_induction_on (P := fun {g : Perm α} ↦
    ∀ {f}, (f ∈ cycleFactorsFinset g)
      → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ _ _ _
no goals
case refine'_1
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ fun {g} => ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}
simp
case refine'_2
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ : Perm α
hσ : IsCycle σ
f : Perm α
hf : f ∈ cycleFactorsFinset σ
⊢ cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
case refine'_2
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ : Perm α),
    IsCycle σ → fun {g} =>
      ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}
intro σ hσ f hf
case refine'_2
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ : Perm α
hσ : IsCycle σ
f : Perm α
hf : f = σ
⊢ cycleFactorsFinset (σ * f⁻¹) = {σ} \ {f}
case refine'_2
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ : Perm α
hσ : IsCycle σ
f : Perm α
hf : f ∈ cycleFactorsFinset σ
⊢ cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf⊢
no goals
case refine'_2
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ : Perm α
hσ : IsCycle σ
f : Perm α
hf : f = σ
⊢ cycleFactorsFinset (σ * f⁻¹) = {σ} \ {f}
simp [hf]
case refine'_3
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
⊢ f ∈ cycleFactorsFinset (σ * τ) → cycleFactorsFinset (σ * τ * f⁻¹) = cycleFactorsFinset (σ * τ) \ {f}
case refine'_3
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ τ : Perm α),
    Disjoint σ τ →
      IsCycle σ →
        (fun {g} =>
            ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) →
          (fun {g} =>
              ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) →
            fun {g} =>
            ∀ {f : Perm α}, f ∈ cycleFactorsFinset g → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}
intro σ τ hd _ hσ hτ f
case refine'_3
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
⊢ f ∈ cycleFactorsFinset σ ∨ f ∈ cycleFactorsFinset τ →
    cycleFactorsFinset (σ * τ * f⁻¹) = (cycleFactorsFinset σ ∪ cycleFactorsFinset τ) \ {f}
case refine'_3
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
⊢ f ∈ cycleFactorsFinset (σ * τ) → cycleFactorsFinset (σ * τ * f⁻¹) = cycleFactorsFinset (σ * τ) \ {f}
simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset σ
⊢ cycleFactorsFinset (σ * τ * f⁻¹) = (cycleFactorsFinset σ ∪ cycleFactorsFinset τ) \ {f}

case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset τ
⊢ cycleFactorsFinset (σ * τ * f⁻¹) = (cycleFactorsFinset σ ∪ cycleFactorsFinset τ) \ {f}
case refine'_3
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
⊢ f ∈ cycleFactorsFinset σ ∨ f ∈ cycleFactorsFinset τ →
    cycleFactorsFinset (σ * τ * f⁻¹) = (cycleFactorsFinset σ ∪ cycleFactorsFinset τ) \ {f}
rintro (hf | hf)
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset σ
⊢ Disjoint τ (σ * f⁻¹)

case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset σ
⊢ ¬f ∈ cycleFactorsFinset τ
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset σ
⊢ cycleFactorsFinset (σ * τ * f⁻¹) = (cycleFactorsFinset σ ∪ cycleFactorsFinset τ) \ {f}
rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
  erase_eq_of_not_mem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
⊢ Disjoint τ (σ * f⁻¹)
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset σ
⊢ Disjoint τ (σ * f⁻¹)
rw [mem_cycleFactorsFinset_iff] at hf
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
⊢ ↑τ x = x ∨ ↑(σ * f⁻¹) x = x
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
⊢ Disjoint τ (σ * f⁻¹)
intro x
case refine'_3.inl.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑τ x = x
⊢ ↑τ x = x ∨ ↑(σ * f⁻¹) x = x

case refine'_3.inl.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
⊢ ↑τ x = x ∨ ↑(σ * f⁻¹) x = x
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
⊢ ↑τ x = x ∨ ↑(σ * f⁻¹) x = x
cases' hd.symm x with hx hx
no goals
case refine'_3.inl.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑τ x = x
⊢ ↑τ x = x ∨ ↑(σ * f⁻¹) x = x
exact Or.inl hx
case refine'_3.inl.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
⊢ ↑(σ * f⁻¹) x = x
case refine'_3.inl.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
⊢ ↑τ x = x ∨ ↑(σ * f⁻¹) x = x
refine' Or.inr _
case pos
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
hfx : ↑f x = x
⊢ ↑(σ * f⁻¹) x = x

case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
hfx : ¬↑f x = x
⊢ ↑(σ * f⁻¹) x = x
case refine'_3.inl.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
⊢ ↑(σ * f⁻¹) x = x
by_cases hfx : f x = x
case pos
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
hfx : ↑f x = x
⊢ ↑(σ * f⁻¹) (↑f x) = ↑f x
case pos
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
hfx : ↑f x = x
⊢ ↑(σ * f⁻¹) x = x
rw [← hfx]
no goals
case pos
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
hfx : ↑f x = x
⊢ ↑(σ * f⁻¹) (↑f x) = ↑f x
simpa [hx] using hfx.symm
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
hfx : ¬↑f x = x
⊢ ↑σ (↑f⁻¹ x) = x
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
hfx : ¬↑f x = x
⊢ ↑(σ * f⁻¹) x = x
rw [mul_apply]
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑f x = x
hfx : ¬↑f x = x
⊢ ↑σ (↑f⁻¹ x) = x
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑σ x = x
hfx : ¬↑f x = x
⊢ ↑σ (↑f⁻¹ x) = x
rw [← hf.right _ (mem_support.mpr hfx)] at hx
no goals
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑σ a
x : α
hx : ↑f x = x
hfx : ¬↑f x = x
⊢ ↑σ (↑f⁻¹ x) = x
contradiction
no goals
case refine'_3.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset σ
⊢ ¬f ∈ cycleFactorsFinset τ
exact fun H =>
not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))
case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset τ
⊢ Disjoint σ (τ * f⁻¹)

case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset τ
⊢ ¬f ∈ cycleFactorsFinset σ
case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset τ
⊢ cycleFactorsFinset (σ * τ * f⁻¹) = (cycleFactorsFinset σ ∪ cycleFactorsFinset τ) \ {f}
rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_not_mem, mul_assoc,
  Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
⊢ Disjoint σ (τ * f⁻¹)
case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset τ
⊢ Disjoint σ (τ * f⁻¹)
rw [mem_cycleFactorsFinset_iff] at hf
case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
⊢ ↑σ x = x ∨ ↑(τ * f⁻¹) x = x
case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
⊢ Disjoint σ (τ * f⁻¹)
intro x
case refine'_3.inr.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑σ x = x
⊢ ↑σ x = x ∨ ↑(τ * f⁻¹) x = x

case refine'_3.inr.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
⊢ ↑σ x = x ∨ ↑(τ * f⁻¹) x = x
case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
⊢ ↑σ x = x ∨ ↑(τ * f⁻¹) x = x
cases' hd x with hx hx
no goals
case refine'_3.inr.inl
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑σ x = x
⊢ ↑σ x = x ∨ ↑(τ * f⁻¹) x = x
exact Or.inl hx
case refine'_3.inr.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
⊢ ↑(τ * f⁻¹) x = x
case refine'_3.inr.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
⊢ ↑σ x = x ∨ ↑(τ * f⁻¹) x = x
refine' Or.inr _
case pos
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
hfx : ↑f x = x
⊢ ↑(τ * f⁻¹) x = x

case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
hfx : ¬↑f x = x
⊢ ↑(τ * f⁻¹) x = x
case refine'_3.inr.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
⊢ ↑(τ * f⁻¹) x = x
by_cases hfx : f x = x
case pos
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
hfx : ↑f x = x
⊢ ↑(τ * f⁻¹) (↑f x) = ↑f x
case pos
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
hfx : ↑f x = x
⊢ ↑(τ * f⁻¹) x = x
rw [← hfx]
no goals
case pos
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
hfx : ↑f x = x
⊢ ↑(τ * f⁻¹) (↑f x) = ↑f x
simpa [hx] using hfx.symm
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
hfx : ¬↑f x = x
⊢ ↑τ (↑f⁻¹ x) = x
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
hfx : ¬↑f x = x
⊢ ↑(τ * f⁻¹) x = x
rw [mul_apply]
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑f x = x
hfx : ¬↑f x = x
⊢ ↑τ (↑f⁻¹ x) = x
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑τ x = x
hfx : ¬↑f x = x
⊢ ↑τ (↑f⁻¹ x) = x
rw [← hf.right _ (mem_support.mpr hfx)] at hx
no goals
case neg
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑τ a
x : α
hx : ↑f x = x
hfx : ¬↑f x = x
⊢ ↑τ (↑f⁻¹ x) = x
contradiction
no goals
case refine'_3.inr
ι : Type ?u.2782985
α : Type u_1
β : Type ?u.2782991
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset σ → cycleFactorsFinset (σ * f⁻¹) = cycleFactorsFinset σ \ {f}
hτ : ∀ {f : Perm α}, f ∈ cycleFactorsFinset τ → cycleFactorsFinset (τ * f⁻¹) = cycleFactorsFinset τ \ {f}
f : Perm α
hf : f ∈ cycleFactorsFinset τ
⊢ ¬f ∈ cycleFactorsFinset σ
exact fun H =>
not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))