α : 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
α : 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
intro f
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

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
α : 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
induction' m using Multiset.induction_on with a m ih
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
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
simp_rw [pi_cons, mem_bind, mem_map, ih]
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

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
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
constructor
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
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
have : f = Pi.empty β := funext (fun _ => funext fun h => (not_mem_zero _ h).elim)
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
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
simp only [this, pi_zero, mem_singleton, true_iff]
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✝
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
intro _ h
no goals
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✝
exact (not_mem_zero _ h).elim
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'
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
rintro ⟨b, hb, f', hf', rfl⟩ a' ha'
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'

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'
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'
by_cases h : a' = a
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'
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'
subst h
no goals
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'
rwa [Pi.cons_same]
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'
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'
rw [Pi.cons_ne _ h]
no goals
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'
apply hf'
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
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
intro hf
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
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
refine' ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), _⟩
no goals
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
rw [pi.cons_eta]