α : Type u_1
β : Type ?u.345110
γ : Type ?u.345113
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
⊢ s = s' → (∀ (x : α), x ∈ s → p x = p' x) → countp p s = countp p' s'
α : Type u_1
β : Type ?u.345110
γ : Type ?u.345113
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
hs : s = s'
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
hp : ∀ (x : α), x ∈ s → p x = p' x
⊢ countp p s = countp p' s'
revert hs hp
no goals
α : Type u_1
β : Type ?u.345110
γ : Type ?u.345113
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
⊢ s = s' → (∀ (x : α), x ∈ s → p x = p' x) → countp p s = countp p' s'
exact Quot.induction_on₂ s s'
  (fun l l' hs hp => by
    simp only [quot_mk_to_coe'', coe_eq_coe] at hs
    apply hs.countp_congr
    simpa using hp)
α : Type u_1
β : Type ?u.345110
γ : Type ?u.345113
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x = p' x
hs : l ~ l'
⊢ countp p (Quot.mk Setoid.r l) = countp p' (Quot.mk Setoid.r l')
α : Type u_1
β : Type ?u.345110
γ : Type ?u.345113
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hs : Quot.mk Setoid.r l = Quot.mk Setoid.r l'
hp : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x = p' x
⊢ countp p (Quot.mk Setoid.r l) = countp p' (Quot.mk Setoid.r l')
simp only [quot_mk_to_coe'', coe_eq_coe] at hs
α : Type u_1
β : Type ?u.345110
γ : Type ?u.345113
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x = p' x
hs : l ~ l'
⊢ ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)
α : Type u_1
β : Type ?u.345110
γ : Type ?u.345113
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x = p' x
hs : l ~ l'
⊢ countp p (Quot.mk Setoid.r l) = countp p' (Quot.mk Setoid.r l')
apply hs.countp_congr
no goals
α : Type u_1
β : Type ?u.345110
γ : Type ?u.345113
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x = p' x
hs : l ~ l'
⊢ ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)
simpa using hp