α : 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)
α : 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)
intro a s ih hs ht
α : 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)
α : 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)
have has : a ∉ s := by simp at hs; exact hs.1
α : 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)
α : 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)
have hs : Nodup s := by simp at hs; exact hs.2
α : 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)
α : 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)
simp
α : 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)
α : 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)
refine'
  ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
    _⟩
α : 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))
α : 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)
refine' (ht a <| mem_cons_self _ _).pairwise _
no goals
α : 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))
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
α : 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
α : 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
simp at hs
no goals
α : 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
exact hs.1
α : 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
α : 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
simp at hs
no goals
α : 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
exact hs.2
no goals
α : 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)
rw [eq]
no goals
α : 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₂
rwa [Pi.cons_same, Pi.cons_same] at this