[GOAL]
α : 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))
[PROOFSTEP]
apply hfunext rfl
[GOAL]
α : 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)
[PROOFSTEP]
simp only [heq_iff_eq]
[GOAL]
α : 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)
[PROOFSTEP]
rintro a'' _ rfl
[GOAL]
α : 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'')
[PROOFSTEP]
refine' hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => _
[GOAL]
α : 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)
[PROOFSTEP]
rw [Multiset.cons_swap]
[GOAL]
α : 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₂)
[PROOFSTEP]
rcases ne_or_eq a'' a with (h₁ | rfl)
[GOAL]
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₂)
[PROOFSTEP]
rcases eq_or_ne a'' a' with (rfl | h₂)
[GOAL]
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₂)
[PROOFSTEP]
all_goals simp [*, Pi.cons_same, Pi.cons_ne]
[GOAL]
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₂)
[PROOFSTEP]
simp [*, Pi.cons_same, Pi.cons_ne]
[GOAL]
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₂)
[PROOFSTEP]
simp [*, Pi.cons_same, Pi.cons_ne]
[GOAL]
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₂)
[PROOFSTEP]
simp [*, Pi.cons_same, Pi.cons_ne]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
⊢ (Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) = f
[PROOFSTEP]
ext a' h'
[GOAL]
case h.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'
[PROOFSTEP]
by_cases h : a' = a
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : a' = a
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a' : α
f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1
h' : a' ∈ a' ::ₘ m
⊢ Pi.cons m a' (f a' (_ : a' ∈ a' ::ₘ m)) (fun a'_1 ha' => f a'_1 (_ : a'_1 ∈ a' ::ₘ m)) a' h' = f a' h'
[PROOFSTEP]
rw [Pi.cons_same]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'
[PROOFSTEP]
rw [Pi.cons_ne _ h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ f₁ a' h' = cons s a b f₁ a' this
[PROOFSTEP]
rw [Pi.cons_ne this ne.symm]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₁ a' this = cons s a b f₂ a' this
[PROOFSTEP]
rw [eq]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₂ a' this = f₂ a' h'
[PROOFSTEP]
rw [Pi.cons_ne this ne.symm]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a a' : α) (m : Multiset α) (b : Multiset ((a : α) → a ∈ m → β a)),
    HEq (bind (t a) fun b_1 => map (Pi.cons (a' ::ₘ m) a b_1) (bind (t a') fun b_2 => map (Pi.cons m a' b_2) b))
      (bind (t a') fun b_1 => map (Pi.cons (a ::ₘ m) a' b_1) (bind (t a) fun b_2 => map (Pi.cons m a b_2) b))
[PROOFSTEP]
intro a a' m n
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
⊢ HEq (bind (t a) fun b => map (Pi.cons (a' ::ₘ m) a b) (bind (t a') fun b => map (Pi.cons m a' b) n))
    (bind (t a') fun b => map (Pi.cons (a ::ₘ m) a' b) (bind (t a) fun b => map (Pi.cons m a b) n))
[PROOFSTEP]
by_cases eq : a = a'
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : a = a'
⊢ HEq (bind (t a) fun b => map (Pi.cons (a' ::ₘ m) a b) (bind (t a') fun b => map (Pi.cons m a' b) n))
    (bind (t a') fun b => map (Pi.cons (a ::ₘ m) a' b) (bind (t a) fun b => map (Pi.cons m a b) n))
[PROOFSTEP]
subst eq
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
⊢ HEq (bind (t a) fun b => map (Pi.cons (a ::ₘ m) a b) (bind (t a) fun b => map (Pi.cons m a b) n))
    (bind (t a) fun b => map (Pi.cons (a ::ₘ m) a b) (bind (t a) fun b => map (Pi.cons m a b) n))
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ HEq (bind (t a) fun b => map (Pi.cons (a' ::ₘ m) a b) (bind (t a') fun b => map (Pi.cons m a' b) n))
    (bind (t a') fun b => map (Pi.cons (a ::ₘ m) a' b) (bind (t a) fun b => map (Pi.cons m a b) n))
[PROOFSTEP]
simp [map_bind, bind_bind (t a') (t a)]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ HEq (bind (t a) fun b => bind (t a') fun a_1 => map (fun x => Pi.cons (a' ::ₘ m) a b (Pi.cons m a' a_1 x)) n)
    (bind (t a) fun b => bind (t a') fun a_1 => map (fun x => Pi.cons (a ::ₘ m) a' a_1 (Pi.cons m a b x)) n)
[PROOFSTEP]
apply bind_hcongr
[GOAL]
case neg.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
[PROOFSTEP]
rw [cons_swap a a']
[GOAL]
case neg.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ∀ (a_1 : β a),
    a_1 ∈ t a →
      HEq (bind (t a') fun a_3 => map (fun x => Pi.cons (a' ::ₘ m) a a_1 (Pi.cons m a' a_3 x)) n)
        (bind (t a') fun a_3 => map (fun x => Pi.cons (a ::ₘ m) a' a_3 (Pi.cons m a a_1 x)) n)
[PROOFSTEP]
intro b _
[GOAL]
case neg.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝ : b ∈ t a
⊢ HEq (bind (t a') fun a_1 => map (fun x => Pi.cons (a' ::ₘ m) a b (Pi.cons m a' a_1 x)) n)
    (bind (t a') fun a_1 => map (fun x => Pi.cons (a ::ₘ m) a' a_1 (Pi.cons m a b x)) n)
[PROOFSTEP]
apply bind_hcongr
[GOAL]
case neg.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝ : b ∈ t a
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
[PROOFSTEP]
rw [cons_swap a a']
[GOAL]
case neg.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝ : b ∈ t a
⊢ ∀ (a_1 : β a'),
    a_1 ∈ t a' →
      HEq (map (fun x => Pi.cons (a' ::ₘ m) a b (Pi.cons m a' a_1 x)) n)
        (map (fun x => Pi.cons (a ::ₘ m) a' a_1 (Pi.cons m a b x)) n)
[PROOFSTEP]
intro b' _
[GOAL]
case neg.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ HEq (map (fun x => Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' x)) n)
    (map (fun x => Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b x)) n)
[PROOFSTEP]
apply map_hcongr
[GOAL]
case neg.hf.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
[PROOFSTEP]
rw [cons_swap a a']
[GOAL]
case neg.hf.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ∀ (a_1 : (a : α) → a ∈ m → β a),
    a_1 ∈ n → HEq (Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' a_1)) (Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b a_1))
[PROOFSTEP]
intro f _
[GOAL]
case neg.hf.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝² : b ∈ t a
b' : β a'
a✝¹ : b' ∈ t a'
f : (a : α) → a ∈ m → β a
a✝ : f ∈ n
⊢ HEq (Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f)) (Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f))
[PROOFSTEP]
exact Pi.cons_swap eq
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ↑card (pi 0 t) = prod (map (fun a => ↑card (t a)) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ↑card (pi s t) = prod (map (fun a => ↑card (t a)) s) →
      ↑card (pi (a ::ₘ s) t) = prod (map (fun a => ↑card (t a)) (a ::ₘ s))
[PROOFSTEP]
simp (config := { contextual := true }) [mul_comm]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)) →
      Nodup (a ::ₘ s) → (∀ (a_3 : α), a_3 ∈ a ::ₘ s → Nodup (t a_3)) → Nodup (pi (a ::ₘ s) t)
[PROOFSTEP]
intro a s ih hs ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
⊢ Nodup (pi (a ::ₘ s) t)
[PROOFSTEP]
have has : a ∉ s := by simp at hs ; exact hs.1
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
⊢ ¬a ∈ s
[PROOFSTEP]
simp at hs 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
hs : ¬a ∈ s ∧ Nodup s
⊢ ¬a ∈ s
[PROOFSTEP]
exact hs.1
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
⊢ Nodup (pi (a ::ₘ s) t)
[PROOFSTEP]
have hs : Nodup s := by simp at hs ; exact hs.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
⊢ Nodup s
[PROOFSTEP]
simp at hs 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
hs : ¬a ∈ s ∧ Nodup s
⊢ Nodup s
[PROOFSTEP]
exact hs.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs✝ : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
hs : Nodup s
⊢ Nodup (pi (a ::ₘ s) t)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs✝ : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
hs : Nodup s
⊢ (∀ (a_1 : β a), a_1 ∈ t a → Nodup (Multiset.map (Pi.cons s a a_1) (pi s t))) ∧
    Pairwise (fun a_1 b => Disjoint (Multiset.map (Pi.cons s a a_1) (pi s t)) (Multiset.map (Pi.cons s a b) (pi s t)))
      (t a)
[PROOFSTEP]
refine' ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has), _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs✝ : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
hs : Nodup s
⊢ Pairwise (fun a_1 b => Disjoint (Multiset.map (Pi.cons s a a_1) (pi s t)) (Multiset.map (Pi.cons s a b) (pi s t)))
    (t a)
[PROOFSTEP]
refine' (ht a <| mem_cons_self _ _).pairwise _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs✝ : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
hs : Nodup s
⊢ ∀ (a_1 : β a),
    a_1 ∈ t a →
      ∀ (b : β a),
        b ∈ t a → a_1 ≠ b → Disjoint (Multiset.map (Pi.cons s a a_1) (pi s t)) (Multiset.map (Pi.cons s a b) (pi s t))
[PROOFSTEP]
exact fun b₁ _ b₂ _ neb =>
  disjoint_map_map.2 fun f _ g _ eq =>
    have : Pi.cons s a b₁ f a (mem_cons_self _ _) = Pi.cons s a b₂ g a (mem_cons_self _ _) := by rw [eq]
    neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs✝ : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
hs : Nodup s
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ pi s t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ pi s t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
⊢ Pi.cons s a b₁ f a (_ : a ∈ a ::ₘ s) = Pi.cons s a b₂ g a (_ : a ∈ a ::ₘ s)
[PROOFSTEP]
rw [eq]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : Nodup s → (∀ (a : α), a ∈ s → Nodup (t a)) → Nodup (pi s t)
hs✝ : Nodup (a ::ₘ s)
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Nodup (t a_1)
has : ¬a ∈ s
hs : Nodup s
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ pi s t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ pi s t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
this : Pi.cons s a b₁ f a (_ : a ∈ a ::ₘ s) = Pi.cons s a b₂ g a (_ : a ∈ a ::ₘ s)
⊢ b₁ = b₂
[PROOFSTEP]
rwa [Pi.cons_same, Pi.cons_same] at this 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
[PROOFSTEP]
intro f
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m → β a
⊢ f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
[PROOFSTEP]
induction' m using Multiset.induction_on with a m ih
[GOAL]
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m → β a
f : (a : α) → a ∈ 0 → β a
⊢ f ∈ pi 0 t ↔ ∀ (a : α) (h : a ∈ 0), f a h ∈ t a
[PROOFSTEP]
have : f = Pi.empty β := funext (fun _ => funext fun h => (not_mem_zero _ h).elim)
[GOAL]
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m → β a
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
⊢ f ∈ pi 0 t ↔ ∀ (a : α) (h : a ∈ 0), f a h ∈ t a
[PROOFSTEP]
simp only [this, pi_zero, mem_singleton, true_iff]
[GOAL]
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m → β a
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
⊢ ∀ (a : α) (h : a ∈ 0), Pi.empty β a h ∈ t a
[PROOFSTEP]
intro _ h
[GOAL]
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m → β a
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
a✝ : α
h : a✝ ∈ 0
⊢ Pi.empty β a✝ h ∈ t a✝
[PROOFSTEP]
exact (not_mem_zero _ h).elim
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ f ∈ pi (a ::ₘ m) t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
[PROOFSTEP]
simp_rw [pi_cons, mem_bind, mem_map, ih]
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) ↔
    ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
[PROOFSTEP]
constructor
[GOAL]
case cons.mp
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) →
    ∀ (a_2 : α) (h : a_2 ∈ a ::ₘ m), f a_2 h ∈ t a_2
[PROOFSTEP]
rintro ⟨b, hb, f', hf', rfl⟩ a' ha'
[GOAL]
case cons.mp.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
⊢ Pi.cons m a b f' a' ha' ∈ t a'
[PROOFSTEP]
by_cases h : a' = a
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m✝ → β a
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
b : β a'
hb : b ∈ t a'
ha' : a' ∈ a' ::ₘ m
⊢ Pi.cons m a' b f' a' ha' ∈ t a'
[PROOFSTEP]
rwa [Pi.cons_same]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'
[PROOFSTEP]
rw [Pi.cons_ne _ h]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f' a' (_ : a' ∈ m) ∈ t a'
[PROOFSTEP]
apply hf'
[GOAL]
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1) →
    ∃ a_2, a_2 ∈ t a ∧ ∃ a_3, (∀ (a : α) (h : a ∈ m), a_3 a h ∈ t a) ∧ Pi.cons m a a_2 a_3 = f
[PROOFSTEP]
intro hf
[GOAL]
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ ∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f
[PROOFSTEP]
refine' ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), _⟩
[GOAL]
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m✝ : Multiset α
t : (a : α) → Multiset (β a)
f✝ : (a : α) → a ∈ m✝ → β a
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ (Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) fun a_1 ha => f a_1 (_ : a_1 ∈ a ::ₘ m)) = f
[PROOFSTEP]
rw [pi.cons_eta]
