α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
hs : Nodup s
hs' : Nodup s'
⊢ formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
hs : Nodup s
hs' : Nodup s'
⊢ formPerm s hs = formPerm s' hs' ↔ s = s' ∨ Subsingleton s ∧ Subsingleton s'
rw [Cycle.length_subsingleton_iff, Cycle.length_subsingleton_iff]
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s s' : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {s s' : Cycle α} {hs : Nodup s} {hs' : Nodup s'},
    formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
hs : Nodup s
hs' : Nodup s'
⊢ formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
revert s s'
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ {hs : Nodup s} {hs' : Nodup s'}, formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s s' : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {s s' : Cycle α} {hs : Nodup s} {hs' : Nodup s'},
    formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
intro s s'
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ (a₁ a₂ : List α) {hs : Nodup (Quotient.mk'' a₁)} {hs' : Nodup (Quotient.mk'' a₂)},
    formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔
      Quotient.mk'' a₁ = Quotient.mk'' a₂ ∨ length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ {hs : Nodup s} {hs' : Nodup s'}, formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
apply @Quotient.inductionOn₂' _ _ _ _ _ s s'
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
⊢ ∀ {hs : Nodup (Quotient.mk'' l)} {hs' : Nodup (Quotient.mk'' l')},
    formPerm (Quotient.mk'' l) hs = formPerm (Quotient.mk'' l') hs' ↔
      Quotient.mk'' l = Quotient.mk'' l' ∨ length (Quotient.mk'' l) ≤ 1 ∧ length (Quotient.mk'' l') ≤ 1
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ (a₁ a₂ : List α) {hs : Nodup (Quotient.mk'' a₁)} {hs' : Nodup (Quotient.mk'' a₂)},
    formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔
      Quotient.mk'' a₁ = Quotient.mk'' a₂ ∨ length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1
intro l l'
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
⊢ ∀ {hs : List.Nodup l} {hs' : List.Nodup l'},
    List.formPerm l = List.formPerm l' ↔ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
⊢ ∀ {hs : Nodup (Quotient.mk'' l)} {hs' : Nodup (Quotient.mk'' l')},
    formPerm (Quotient.mk'' l) hs = formPerm (Quotient.mk'' l') hs' ↔
      Quotient.mk'' l = Quotient.mk'' l' ∨ length (Quotient.mk'' l) ≤ 1 ∧ length (Quotient.mk'' l') ≤ 1
simp_all
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hs : List.Nodup l
hs' : List.Nodup l'
⊢ List.formPerm l = List.formPerm l' ↔ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
⊢ ∀ {hs : List.Nodup l} {hs' : List.Nodup l'},
    List.formPerm l = List.formPerm l' ↔ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
intro hs hs'
no goals
α✝ : Type ?u.33186
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hs : List.Nodup l
hs' : List.Nodup l'
⊢ List.formPerm l = List.formPerm l' ↔ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
constructor <;> intro h <;> simp_all only [formPerm_eq_formPerm_iff]