α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α),
    HEq a_1 a'_1 → HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a_1) (cons (a ::ₘ m) a' b' (cons m a b f) a'_1)
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f)) (cons (a ::ₘ m) a' b' (cons m a b f))
apply hfunext rfl
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α),
    a_1 = a'_1 → HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a_1) (cons (a ::ₘ m) a' b' (cons m a b f) a'_1)
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α),
    HEq a_1 a'_1 → HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a_1) (cons (a ::ₘ m) a' b' (cons m a b f) a'_1)
simp only [heq_iff_eq]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'') (cons (a ::ₘ m) a' b' (cons m a b f) a'')
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α),
    a_1 = a'_1 → HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a_1) (cons (a ::ₘ m) a' b' (cons m a b f) a'_1)
rintro a'' _ rfl
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'') (cons (a ::ₘ m) a' b' (cons m a b f) a'')
refine' hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => _
case inl
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

case inr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁) (cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂)
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)
rcases ne_or_eq a'' a with (h₁ | rfl)
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a : α
b : δ a
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
h₁ : a'' ≠ a
b' : δ a''
h : a ≠ a''
ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m
ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁) (cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂)

case inl.inr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

case inr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁) (cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂)
case inl
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

case inr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁) (cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂)
rcases eq_or_ne a'' a' with (rfl | h₂)
no goals
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a : α
b : δ a
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
h₁ : a'' ≠ a
b' : δ a''
h : a ≠ a''
ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m
ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁) (cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂)

case inl.inr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

case inr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁) (cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂)
all_goals simp [*, Pi.cons_same, Pi.cons_ne]
no goals
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ (a'' ∈ a ::ₘ a' ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)
rw [Multiset.cons_swap]
no goals
case inr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁) (cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂)
simp [*, Pi.cons_same, Pi.cons_ne]