ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
⊢ σ ∈ l₁ ↔ σ ∈ l₂
ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
⊢ l₁ ~ l₂
refine'
  (List.perm_ext (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
        (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
    fun σ => _
case pos
ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : IsCycle σ
⊢ σ ∈ l₁ ↔ σ ∈ l₂

case neg
ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : ¬IsCycle σ
⊢ σ ∈ l₁ ↔ σ ∈ l₂
ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
⊢ σ ∈ l₁ ↔ σ ∈ l₂
by_cases hσ : σ.IsCycle
case pos
ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : IsCycle σ
x✝ : ∃ x, ¬↑σ x = ↑1 x
⊢ σ ∈ l₁ ↔ σ ∈ l₂
case pos
ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : IsCycle σ
⊢ σ ∈ l₁ ↔ σ ∈ l₂
obtain _ := not_forall.mp (mt ext hσ.ne_one)
no goals
case pos
ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : IsCycle σ
x✝ : ∃ x, ¬↑σ x = ↑1 x
⊢ σ ∈ l₁ ↔ σ ∈ l₂
rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
no goals
case neg
ι : Type ?u.2673155
α✝ : Type ?u.2673158
β : Type ?u.2673161
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : List.prod l₁ = List.prod l₂
h₁l₁ : ∀ (σ : Perm α), σ ∈ l₁ → IsCycle σ
h₁l₂ : ∀ (σ : Perm α), σ ∈ l₂ → IsCycle σ
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : ¬IsCycle σ
⊢ σ ∈ l₁ ↔ σ ∈ l₂
exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)