no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
p✝ : α → Prop
f : (a : α) → p✝ a → β
l₁ l₂ : List α
p : l₁ ~ l₂
H₁ : ∀ (a : α), a ∈ l₁ → p✝ a
H₂ : ∀ (a : α), a ∈ l₂ → p✝ a
⊢ List.pmap f l₁ H₁ ~ List.pmap f l₂ H₂
induction p with
| nil => simp
| cons x _p IH => simp [IH, Perm.cons]
| swap x y => simp [swap]
| trans _p₁ p₂ IH₁ IH₂ =>
  refine' IH₁.trans IH₂
  exact fun a m => H₂ a (p₂.subset m)
no goals
case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ : List α
H₁ H₂ : ∀ (a : α), a ∈ [] → p a
⊢ List.pmap f [] H₁ ~ List.pmap f [] H₂
simp
no goals
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH : ∀ {H₁ : ∀ (a : α), a ∈ l₁✝ → p a} {H₂ : ∀ (a : α), a ∈ l₂✝ → p a}, List.pmap f l₁✝ H₁ ~ List.pmap f l₂✝ H₂
H₁ : ∀ (a : α), a ∈ x :: l₁✝ → p a
H₂ : ∀ (a : α), a ∈ x :: l₂✝ → p a
⊢ List.pmap f (x :: l₁✝) H₁ ~ List.pmap f (x :: l₂✝) H₂
simp [IH, Perm.cons]
no goals
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ : List α
x y : α
l✝ : List α
H₁ : ∀ (a : α), a ∈ y :: x :: l✝ → p a
H₂ : ∀ (a : α), a ∈ x :: y :: l✝ → p a
⊢ List.pmap f (y :: x :: l✝) H₁ ~ List.pmap f (x :: y :: l✝) H₂
simp [swap]
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
_p₁ : l₁✝ ~ l₂✝
p₂ : l₂✝ ~ l₃✝
IH₁ : ∀ {H₁ : ∀ (a : α), a ∈ l₁✝ → p a} {H₂ : ∀ (a : α), a ∈ l₂✝ → p a}, List.pmap f l₁✝ H₁ ~ List.pmap f l₂✝ H₂
IH₂ : ∀ {H₁ : ∀ (a : α), a ∈ l₂✝ → p a} {H₂ : ∀ (a : α), a ∈ l₃✝ → p a}, List.pmap f l₂✝ H₁ ~ List.pmap f l₃✝ H₂
H₁ : ∀ (a : α), a ∈ l₁✝ → p a
H₂ : ∀ (a : α), a ∈ l₃✝ → p a
⊢ ∀ (a : α), a ∈ l₂✝ → p a
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
_p₁ : l₁✝ ~ l₂✝
p₂ : l₂✝ ~ l₃✝
IH₁ : ∀ {H₁ : ∀ (a : α), a ∈ l₁✝ → p a} {H₂ : ∀ (a : α), a ∈ l₂✝ → p a}, List.pmap f l₁✝ H₁ ~ List.pmap f l₂✝ H₂
IH₂ : ∀ {H₁ : ∀ (a : α), a ∈ l₂✝ → p a} {H₂ : ∀ (a : α), a ∈ l₃✝ → p a}, List.pmap f l₂✝ H₁ ~ List.pmap f l₃✝ H₂
H₁ : ∀ (a : α), a ∈ l₁✝ → p a
H₂ : ∀ (a : α), a ∈ l₃✝ → p a
⊢ List.pmap f l₁✝ H₁ ~ List.pmap f l₃✝ H₂
refine' IH₁.trans IH₂
no goals
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
_p₁ : l₁✝ ~ l₂✝
p₂ : l₂✝ ~ l₃✝
IH₁ : ∀ {H₁ : ∀ (a : α), a ∈ l₁✝ → p a} {H₂ : ∀ (a : α), a ∈ l₂✝ → p a}, List.pmap f l₁✝ H₁ ~ List.pmap f l₂✝ H₂
IH₂ : ∀ {H₁ : ∀ (a : α), a ∈ l₂✝ → p a} {H₂ : ∀ (a : α), a ∈ l₃✝ → p a}, List.pmap f l₂✝ H₁ ~ List.pmap f l₃✝ H₂
H₁ : ∀ (a : α), a ∈ l₁✝ → p a
H₂ : ∀ (a : α), a ∈ l₃✝ → p a
⊢ ∀ (a : α), a ∈ l₂✝ → p a
exact fun a m => H₂ a (p₂.subset m)