α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
⊢ ∀ {a b : Perm α}, a ∈ l → b ∈ l → Disjoint a b → a ≠ b
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
⊢ List.Nodup l
refine' List.Pairwise.imp_of_mem _ h2
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
τ σ : Perm α
h_mem : τ ∈ l
a✝¹ : σ ∈ l
h_disjoint : Disjoint τ σ
a✝ : τ = σ
⊢ False
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
⊢ ∀ {a b : Perm α}, a ∈ l → b ∈ l → Disjoint a b → a ≠ b
intro τ σ h_mem _ h_disjoint _
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
⊢ False
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
τ σ : Perm α
h_mem : τ ∈ l
a✝¹ : σ ∈ l
h_disjoint : Disjoint τ σ
a✝ : τ = σ
⊢ False
subst τ
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
⊢ σ = 1
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
⊢ False
suffices (σ : Perm α) = 1 by
  rw [this] at h_mem
  exact h1 h_mem
no goals
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
⊢ σ = 1
exact ext fun a => (or_self_iff _).mp (h_disjoint a)
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ : σ ∈ l
h_mem : 1 ∈ l
h_disjoint : Disjoint σ σ
this : σ = 1
⊢ False
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
this : σ = 1
⊢ False
rw [this] at h_mem
no goals
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ : σ ∈ l
h_mem : 1 ∈ l
h_disjoint : Disjoint σ σ
this : σ = 1
⊢ False
exact h1 h_mem