case intro
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
⊢ P σ
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
⊢ P σ
cases nonempty_fintype β
case intro
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
⊢ ∀ (l : List (Perm β)), (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
case intro
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
⊢ P σ
suffices ∀ l : List (Perm β),
    (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
  classical
    let x := σ.truncCycleFactors.out
    exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
case intro
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
l : List (Perm β)
⊢ (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
case intro
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
⊢ ∀ (l : List (Perm β)), (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
intro l
case intro.nil
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
⊢ (∀ (τ : Perm β), τ ∈ [] → IsCycle τ) → List.Pairwise Disjoint [] → P (List.prod [])

case intro.cons
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
⊢ (∀ (τ : Perm β), τ ∈ σ :: l → IsCycle τ) → List.Pairwise Disjoint (σ :: l) → P (List.prod (σ :: l))
case intro
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
l : List (Perm β)
⊢ (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
induction' l with σ l ih
no goals
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
this : ∀ (l : List (Perm β)), (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
⊢ P σ
classical
  let x := σ.truncCycleFactors.out
  exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
this : ∀ (l : List (Perm β)), (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
x : { l // List.prod l = σ ∧ (∀ (g : Perm β), g ∈ l → IsCycle g) ∧ List.Pairwise Disjoint l } :=
  Trunc.out (truncCycleFactors σ)
⊢ P σ
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
this : ∀ (l : List (Perm β)), (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
⊢ P σ
let x := σ.truncCycleFactors.out
no goals
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
this : ∀ (l : List (Perm β)), (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
x : { l // List.prod l = σ ∧ (∀ (g : Perm β), g ∈ l → IsCycle g) ∧ List.Pairwise Disjoint l } :=
  Trunc.out (truncCycleFactors σ)
⊢ P σ
exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
no goals
case intro.nil
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
⊢ (∀ (τ : Perm β), τ ∈ [] → IsCycle τ) → List.Pairwise Disjoint [] → P (List.prod [])
exact fun _ _ => base_one
case intro.cons
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
h1 : ∀ (τ : Perm β), τ ∈ σ :: l → IsCycle τ
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (List.prod (σ :: l))
case intro.cons
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
⊢ (∀ (τ : Perm β), τ ∈ σ :: l → IsCycle τ) → List.Pairwise Disjoint (σ :: l) → P (List.prod (σ :: l))
intro h1 h2
case intro.cons
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
h1 : ∀ (τ : Perm β), τ ∈ σ :: l → IsCycle τ
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ * List.prod l)
case intro.cons
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
h1 : ∀ (τ : Perm β), τ ∈ σ :: l → IsCycle τ
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (List.prod (σ :: l))
rw [List.prod_cons]
no goals
case intro.cons
ι : Type ?u.2779478
α : Type ?u.2779481
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), IsCycle σ → P σ
induction_disjoint : ∀ (σ τ : Perm β), Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ (τ : Perm β), τ ∈ l → IsCycle τ) → List.Pairwise Disjoint l → P (List.prod l)
h1 : ∀ (τ : Perm β), τ ∈ σ :: l → IsCycle τ
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ * List.prod l)
exact
  induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
    (h1 _ (List.mem_cons_self _ _)) (base_cycles σ (h1 σ (l.mem_cons_self σ)))
    (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)