-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycle_induction_on [Finite β] (P : Perm β → Prop) (σ : Perm β) (base_one : P 1)
    (base_cycles : ∀ σ : Perm β, σ.IsCycle → P σ)
    (induction_disjoint : ∀ σ τ : Perm β,
      Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)) : P σ

Proof state:
β : Type u_3
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 β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
x : { l // l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l } := σ.truncCycleFactors.out
⊢ P σ

Tactic:
exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)

Result:
no goals

Proof state:
case intro.cons
β : Type u_3
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 : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ :: l).prod

Tactic:
rw [List.prod_cons]

Result:
case intro.cons
β : Type u_3
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 : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ * l.prod)

Proof state:
case intro
β : Type u_3
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 β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod

Tactic:
intro l

Result:
case intro
β : Type u_3
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 β)
⊢ (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod

Proof state:
β : Type u_3
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 β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
⊢ P σ

Tactic:
let x := σ.truncCycleFactors.out

Result:
β : Type u_3
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 β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
x : { l // l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l } := σ.truncCycleFactors.out
⊢ P σ

Proof state:
case intro.cons
β : Type u_3
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 : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ * l.prod)

Tactic:
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)

Result:
no goals

Proof state:
case intro.nil
β : Type u_3
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 β
⊢ (∀ τ ∈ [], τ.IsCycle) → List.Pairwise Disjoint [] → P [].prod

Tactic:
exact fun _ _ => base_one

Result:
no goals

Proof state:
β : Type u_3
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 β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
⊢ P σ

Tactic:
classical
  let x := σ.truncCycleFactors.out
  exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)

Result:
no goals

Proof state:
case intro.cons
β : Type u_3
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 : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
⊢ (∀ τ ∈ σ :: l, τ.IsCycle) → List.Pairwise Disjoint (σ :: l) → P (σ :: l).prod

Tactic:
intro h1 h2

Result:
case intro.cons
β : Type u_3
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 : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ :: l).prod

Proof state:
case intro
β : Type u_3
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 σ

Tactic:
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)

Result:
case intro
β : Type u_3
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 β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod

Proof state:
case intro
β : Type u_3
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 β)
⊢ (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod

Tactic:
induction' l with σ l ih

Result:
case intro.nil
β : Type u_3
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 β
⊢ (∀ τ ∈ [], τ.IsCycle) → List.Pairwise Disjoint [] → P [].prod

case intro.cons
β : Type u_3
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 : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
⊢ (∀ τ ∈ σ :: l, τ.IsCycle) → List.Pairwise Disjoint (σ :: l) → P (σ :: l).prod

Proof state:
β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
⊢ P σ

Tactic:
cases nonempty_fintype β

Result:
case intro
β : Type u_3
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 σ