-- Mathlib/Data/Multiset/Pi.lean
theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (β a)} :
    Nodup s → (∀ a ∈ s, Nodup (t a)) → Nodup (pi s t) :=
  Multiset.induction_on s (fun _ _ => nodup_singleton _)
    (by
      intro a s ih hs ht
      have has : a ∉ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : a ∉ s ∧ s.Nodup
⊢ s.Nodup

Tactic:
exact hs.2

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
⊢ ∀ a_1 ∈ t a, ∀ b ∈ t a, a_1 ≠ b → (Disjoint on fun b => Multiset.map (Pi.cons s a b) (s.pi t)) a_1 b

Tactic:
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

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
⊢ (∀ a_1 ∈ t a, (Multiset.map (Pi.cons s a a_1) (s.pi t)).Nodup) ∧
    Pairwise (Disjoint on fun b => Multiset.map (Pi.cons s a b) (s.pi t)) (t a)

Tactic:
refine
  ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
    ?_⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
⊢ Pairwise (Disjoint on fun b => Multiset.map (Pi.cons s a b) (s.pi t)) (t a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a : α) (s : Multiset α),
    (s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup) →
      (a ::ₘ s).Nodup → (∀ a_3 ∈ a ::ₘ s, (t a_3).Nodup) → ((a ::ₘ s).pi t).Nodup

Tactic:
intro a s ih hs ht

Result:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
⊢ ((a ::ₘ s).pi t).Nodup

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
⊢ ((a ::ₘ s).pi t).Nodup

Tactic:
simp only [pi_cons, nodup_bind]

Result:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
⊢ (∀ a_1 ∈ t a, (Multiset.map (Pi.cons s a a_1) (s.pi t)).Nodup) ∧
    Pairwise (Disjoint on fun b => Multiset.map (Pi.cons s a b) (s.pi t)) (t a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
⊢ Pairwise (Disjoint on fun b => Multiset.map (Pi.cons s a b) (s.pi t)) (t a)

Tactic:
refine (ht a <| mem_cons_self _ _).pairwise ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
⊢ ∀ a_1 ∈ t a, ∀ b ∈ t a, a_1 ≠ b → (Disjoint on fun b => Multiset.map (Pi.cons s a b) (s.pi t)) a_1 b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
⊢ ((a ::ₘ s).pi t).Nodup

Tactic:
have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2

Result:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
⊢ ((a ::ₘ s).pi t).Nodup

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ s.pi t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ s.pi t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
⊢ Pi.cons s a b₁ f a ⋯ = Pi.cons s a b₂ g a ⋯

Tactic:
rw [eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
⊢ s.Nodup

Tactic:
simp only [nodup_cons] at hs

Result:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : a ∉ s ∧ s.Nodup
⊢ s.Nodup

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
hs : a ∉ s ∧ s.Nodup
⊢ a ∉ s

Tactic:
exact hs.1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
⊢ a ∉ s

Tactic:
simp only [nodup_cons] at hs

Result:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
hs : a ∉ s ∧ s.Nodup
⊢ a ∉ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
hs : s.Nodup
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ s.pi t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ s.pi t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
this : Pi.cons s a b₁ f a ⋯ = Pi.cons s a b₂ g a ⋯
⊢ b₁ = b₂

Tactic:
rwa [Pi.cons_same, Pi.cons_same] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
⊢ ((a ::ₘ s).pi t).Nodup

Tactic:
have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1

Result:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup
has : a ∉ s
⊢ ((a ::ₘ s).pi t).Nodup