α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
⊢ [a₁, b₁] ~ [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
simp [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.cons_eq_cons]
no goals
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
aesop
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [a₁, b₁] ~ [a₂, b₂]
rw [h₁, h₂]
no goals
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
first | done | apply List.Perm.swap'; rfl
no goals
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
done
case p
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [] ~ []
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
apply List.Perm.swap'
no goals
case p
α : Type u_1
β : Type ?u.49466
γ : Type ?u.49469
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [] ~ []
rfl