[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
⊢ ∀ (a : α ⊕ β), ¬LiftRel r s a a
[PROOFSTEP]
rintro _ (⟨h⟩ | ⟨h⟩)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
a✝ : α
h : r a✝ a✝
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
b✝ : β
h : s b✝ b✝
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
⊢ ∀ (a b : α ⊕ β), LiftRel r s a b → LiftRel r s b a → a = b
[PROOFSTEP]
rintro _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hba⟩ | ⟨hba⟩)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
a✝ c✝ : α
hab : r a✝ c✝
hba : r c✝ a✝
⊢ inl a✝ = inl c✝
[PROOFSTEP]
rw [antisymm hab hba]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
b✝ d✝ : β
hab : s b✝ d✝
hba : s d✝ b✝
⊢ inr b✝ = inr d✝
[PROOFSTEP]
rw [antisymm hab hba]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsRefl β s
⊢ ∀ (a : α ⊕ β), Lex r s a a
[PROOFSTEP]
rintro (a | a)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsRefl β s
a : α
⊢ Lex r s (inl a) (inl a)
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsRefl β s
a : β
⊢ Lex r s (inr a) (inr a)
[PROOFSTEP]
exacts [Lex.inl (refl _), Lex.inr (refl _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
⊢ ∀ (a : α ⊕ β), ¬Lex r s a a
[PROOFSTEP]
rintro _ (⟨h⟩ | ⟨h⟩)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
a₁✝ : α
h : r a₁✝ a₁✝
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
b₁✝ : β
h : s b₁✝ b₁✝
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
⊢ ∀ (a b c : α ⊕ β), Lex r s a b → Lex r s b c → Lex r s a c
[PROOFSTEP]
rintro _ _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hbc⟩ | ⟨hbc⟩)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a₁✝ a₂✝¹ : α
hab : r a₁✝ a₂✝¹
a₂✝ : α
hbc : r a₂✝¹ a₂✝
⊢ Lex r s (inl a₁✝) (inl a₂✝)
case inl.sep
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
b✝ : β
⊢ Lex r s (inl a₁✝) (inr b✝)
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
b₁✝ b₂✝¹ : β
hab : s b₁✝ b₂✝¹
b₂✝ : β
hbc : s b₂✝¹ b₂✝
⊢ Lex r s (inr b₁✝) (inr b₂✝)
case sep.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a✝ : α
b✝ b₂✝ : β
hbc : s b✝ b₂✝
⊢ Lex r s (inl a✝) (inr b₂✝)
[PROOFSTEP]
exacts [.inl (_root_.trans hab hbc), .sep _ _, .inr (_root_.trans hab hbc), .sep _ _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
⊢ ∀ (a b : α ⊕ β), Lex r s a b → Lex r s b a → a = b
[PROOFSTEP]
rintro _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hba⟩ | ⟨hba⟩)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
hba : r a₂✝ a₁✝
⊢ inl a₁✝ = inl a₂✝
[PROOFSTEP]
rw [antisymm hab hba]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
b₁✝ b₂✝ : β
hab : s b₁✝ b₂✝
hba : s b₂✝ b₁✝
⊢ inr b₁✝ = inr b₂✝
[PROOFSTEP]
rw [antisymm hab hba]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a b : α ⊕ β
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
refine' ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, _⟩, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a b : α ⊕ β
hab : a < b
⊢ ¬b ≤ a
[PROOFSTEP]
rintro (⟨hba⟩ | ⟨hba⟩)
[GOAL]
case refine'_1.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a✝ c✝ : α
hba : a✝ ≤ c✝
hab : inl c✝ < inl a✝
⊢ False
[PROOFSTEP]
exact hba.not_lt (inl_lt_inl_iff.1 hab)
[GOAL]
case refine'_1.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
b✝ d✝ : β
hba : b✝ ≤ d✝
hab : inr d✝ < inr b✝
⊢ False
[PROOFSTEP]
exact hba.not_lt (inr_lt_inr_iff.1 hab)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a b : α ⊕ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b
[PROOFSTEP]
rintro ⟨⟨hab⟩ | ⟨hab⟩, hba⟩
[GOAL]
case refine'_2.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a✝ c✝ : α
hab : a✝ ≤ c✝
hba : ¬inl c✝ ≤ inl a✝
⊢ inl a✝ < inl c✝
[PROOFSTEP]
exact LiftRel.inl (hab.lt_of_not_le fun h => hba <| LiftRel.inl h)
[GOAL]
case refine'_2.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
b✝ d✝ : β
hab : b✝ ≤ d✝
hba : ¬inr d✝ ≤ inr b✝
⊢ inr b✝ < inr d✝
[PROOFSTEP]
exact LiftRel.inr (hab.lt_of_not_le fun h => hba <| LiftRel.inr h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
⊢ ∃ b, b < a
[PROOFSTEP]
obtain ⟨b | b, h⟩ := exists_lt (inl a : Sum α β)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : α
h : inl b < inl a
⊢ ∃ b, b < a
[PROOFSTEP]
exact ⟨b, inl_lt_inl_iff.1 h⟩
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
b : β
h : inr b < inl a
⊢ ∃ b, b < a
[PROOFSTEP]
exact (not_inr_lt_inl h).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
⊢ ∃ b, b < a
[PROOFSTEP]
obtain ⟨b | b, h⟩ := exists_lt (inr a : Sum α β)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ b, b < a
[PROOFSTEP]
exact (not_inl_lt_inr h).elim
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : β
h : inr b < inr a
⊢ ∃ b, b < a
[PROOFSTEP]
exact ⟨b, inr_lt_inr_iff.1 h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
⊢ ∃ b, a < b
[PROOFSTEP]
obtain ⟨b | b, h⟩ := exists_gt (inl a : Sum α β)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : α
h : inl a < inl b
⊢ ∃ b, a < b
[PROOFSTEP]
exact ⟨b, inl_lt_inl_iff.1 h⟩
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
b : β
h : inl a < inr b
⊢ ∃ b, a < b
[PROOFSTEP]
exact (not_inl_lt_inr h).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
⊢ ∃ b, a < b
[PROOFSTEP]
obtain ⟨b | b, h⟩ := exists_gt (inr a : Sum α β)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
b : α
h : inr a < inl b
⊢ ∃ b, a < b
[PROOFSTEP]
exact (not_inr_lt_inl h).elim
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : β
h : inr a < inr b
⊢ ∃ b, a < b
[PROOFSTEP]
exact ⟨b, inr_lt_inr_iff.1 h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
obtain ⟨c | c, ha, hb⟩ := @exists_between (Sum α β) _ _ _ _ (inl_lt_inl_iff.2 h)
[GOAL]
case intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : α
ha : inl a < inl c
hb : inl c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩
[GOAL]
case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
exact (not_inl_lt_inr ha).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
obtain ⟨c | c, ha, hb⟩ := @exists_between (Sum α β) _ _ _ _ (inr_lt_inr_iff.2 h)
[GOAL]
case intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : α
ha : inr a < inl c
hb : inl c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
exact (not_inl_lt_inr hb).elim
[GOAL]
case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : β
ha : inr a < inr c
hb : inr c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a b : _root_.Lex (α ⊕ β)
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
refine' ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, _⟩, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a b : _root_.Lex (α ⊕ β)
hab : a < b
⊢ ¬b ≤ a
[PROOFSTEP]
rintro (⟨hba⟩ | ⟨hba⟩ | ⟨b, a⟩)
[GOAL]
case refine'_1.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a₁✝ a₂✝ : α
hba : a₁✝ ≤ a₂✝
hab : inl a₂✝ < inl a₁✝
⊢ False
[PROOFSTEP]
exact hba.not_lt (inl_lt_inl_iff.1 hab)
[GOAL]
case refine'_1.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
b₁✝ b₂✝ : β
hba : b₁✝ ≤ b₂✝
hab : inr b₂✝ < inr b₁✝
⊢ False
[PROOFSTEP]
exact hba.not_lt (inr_lt_inr_iff.1 hab)
[GOAL]
case refine'_1.sep
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
b : α
a : β
hab : inr a < inl b
⊢ False
[PROOFSTEP]
exact not_inr_lt_inl hab
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a b : _root_.Lex (α ⊕ β)
⊢ a ≤ b ∧ ¬b ≤ a → a < b
[PROOFSTEP]
rintro ⟨⟨hab⟩ | ⟨hab⟩ | ⟨a, b⟩, hba⟩
[GOAL]
case refine'_2.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a₁✝ a₂✝ : α
hab : a₁✝ ≤ a₂✝
hba : ¬inl a₂✝ ≤ inl a₁✝
⊢ inl a₁✝ < inl a₂✝
[PROOFSTEP]
exact Lex.inl (hab.lt_of_not_le fun h => hba <| Lex.inl h)
[GOAL]
case refine'_2.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
b₁✝ b₂✝ : β
hab : b₁✝ ≤ b₂✝
hba : ¬inr b₂✝ ≤ inr b₁✝
⊢ inr b₁✝ < inr b₂✝
[PROOFSTEP]
exact Lex.inr (hab.lt_of_not_le fun h => hba <| Lex.inr h)
[GOAL]
case refine'_2.intro.sep
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b
[PROOFSTEP]
exact Lex.sep _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
⊢ ∀ (a : _root_.Lex (α ⊕ β)), ⊥ ≤ a
[PROOFSTEP]
rintro (a | b)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
a : α
⊢ ⊥ ≤ inl a
[PROOFSTEP]
exact Lex.inl bot_le
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
b : β
⊢ ⊥ ≤ inr b
[PROOFSTEP]
exact Lex.sep _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
⊢ ∀ (a : _root_.Lex (α ⊕ β)), a ≤ ⊤
[PROOFSTEP]
rintro (a | b)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
a : α
⊢ inl a ≤ ⊤
[PROOFSTEP]
exact Lex.sep _ _
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
b : β
⊢ inr b ≤ ⊤
[PROOFSTEP]
exact Lex.inr le_top
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a✝ : α✝
b✝ : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
a b : (α ⊕ β) ⊕ γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        a ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    a ≤ b
[PROOFSTEP]
rcases a with ((_ | _) | _)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b✝ : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
b : (α ⊕ β) ⊕ γ
val✝ : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inl (inl val✝) ≤ b
[PROOFSTEP]
rcases b with ((_ | _) | _)
[GOAL]
case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b✝ : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
b : (α ⊕ β) ⊕ γ
val✝ : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inl (inr val✝) ≤ b
[PROOFSTEP]
rcases b with ((_ | _) | _)
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b✝ : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
b : (α ⊕ β) ⊕ γ
val✝ : γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inr val✝ ≤ b
[PROOFSTEP]
rcases b with ((_ | _) | _)
[GOAL]
case inl.inl.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ val✝ : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝)) ↔
    inl (inl val✝¹) ≤ inl (inl val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inl.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : α
val✝ : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝)) ↔
    inl (inl val✝¹) ≤ inl (inr val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : α
val✝ : γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝) ↔
    inl (inl val✝¹) ≤ inr val✝
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inr.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : β
val✝ : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝)) ↔
    inl (inr val✝¹) ≤ inl (inl val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inr.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ val✝ : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝)) ↔
    inl (inr val✝¹) ≤ inl (inr val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : β
val✝ : γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝) ↔
    inl (inr val✝¹) ≤ inr val✝
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inr.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : γ
val✝ : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝¹) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝)) ↔
    inr val✝¹ ≤ inl (inl val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inr.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : γ
val✝ : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝¹) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝)) ↔
    inr val✝¹ ≤ inl (inr val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ val✝ : γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝¹) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝) ↔
    inr val✝¹ ≤ inr val✝
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a : α✝
b : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
⊢ ∀ {a b : (α ⊕ β)ᵒᵈ},
    ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          a ≤
        ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          b ↔
      a ≤ b
[PROOFSTEP]
rintro (a | a) (b | b)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inl a ≤ inl b
[PROOFSTEP]
change inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a b : α
⊢ inl (↑toDual a) ≤ inl (↑toDual b) ↔ ↑toDual (inl a) ≤ ↑toDual (inl b)
[PROOFSTEP]
simp [toDual_le_toDual, inl_le_inl_iff]
[GOAL]
case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a : α
b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inl a ≤ inr b
[PROOFSTEP]
exact iff_of_false (@not_inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _) not_inr_le_inl
[GOAL]
case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a : β
b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inr a ≤ inl b
[PROOFSTEP]
exact iff_of_false (@not_inr_le_inl (OrderDual α) (OrderDual β) _ _ _ _) not_inl_le_inr
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inr a ≤ inr b
[PROOFSTEP]
change inr (toDual a) ≤ inr (toDual b) ↔ toDual (inr a) ≤ toDual (inr b)
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a b : β
⊢ inr (↑toDual a) ≤ inr (↑toDual b) ↔ ↑toDual (inr a) ≤ ↑toDual (inr b)
[PROOFSTEP]
simp [toDual_le_toDual, inr_le_inr_iff]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : (_root_.Lex (α ⊕ β))ᵒᵈ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        a ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    a ≤ b
[PROOFSTEP]
rcases a with (a | a)
[GOAL]
case inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
b : (_root_.Lex (α ⊕ β))ᵒᵈ
a : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inl a ≤ b
[PROOFSTEP]
rcases b with (b | b)
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
b : (_root_.Lex (α ⊕ β))ᵒᵈ
a : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inr a ≤ b
[PROOFSTEP]
rcases b with (b | b)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inl a ≤ inl b
case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a : α
b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inl a ≤ inr b
case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a : β
b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inr a ≤ inl b
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inr a ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : α
⊢ inr a ≤ inr b ↔ inl a ≤ inl b
[PROOFSTEP]
change toLex (inr <| toDual a) ≤ toLex (inr <| toDual b) ↔ toDual (toLex <| inl a) ≤ toDual (toLex <| inl b)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : α
⊢ ↑toLex (inr (↑toDual a)) ≤ ↑toLex (inr (↑toDual b)) ↔ ↑toDual (↑toLex (inl a)) ≤ ↑toDual (↑toLex (inl b))
[PROOFSTEP]
simp [toDual_le_toDual, Lex.inl_le_inl_iff, Lex.inr_le_inr_iff]
[GOAL]
case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a : α
b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inl a ≤ inr b
[PROOFSTEP]
exact iff_of_false (@Lex.not_inr_le_inl (OrderDual β) (OrderDual α) _ _ _ _) Lex.not_inr_le_inl
[GOAL]
case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a : β
b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inr a ≤ inl b
[PROOFSTEP]
exact iff_of_true (@Lex.inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _) (Lex.inl_le_inr _ _)
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inr a ≤ inr b
[PROOFSTEP]
change toLex (inl <| toDual a) ≤ toLex (inl <| toDual b) ↔ toDual (toLex <| inr a) ≤ toDual (toLex <| inr b)
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : β
⊢ ↑toLex (inl (↑toDual a)) ≤ ↑toLex (inl (↑toDual b)) ↔ ↑toDual (↑toLex (inr a)) ≤ ↑toDual (↑toLex (inr b))
[PROOFSTEP]
simp [toDual_le_toDual, Lex.inl_le_inl_iff, Lex.inr_le_inr_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
a b : WithBot α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) a ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) b ↔
    a ≤ b
[PROOFSTEP]
rcases a with (a | _)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
b : WithBot α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) b ↔
    none ≤ b
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
b : WithBot α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝) ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) b ↔
    Option.some val✝ ≤ b
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ↔
    none ≤ none
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝) ↔
    none ≤ Option.some val✝
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝) ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ↔
    Option.some val✝ ≤ none
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝¹ val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝¹) ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝) ↔
    Option.some val✝¹ ≤ Option.some val✝
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ¬Option.some val✝ ≤ none
[PROOFSTEP]
exact not_coe_le_bot _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
a b : WithTop α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) a ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) b ↔ a ≤ b
[PROOFSTEP]
rcases a with (a | _)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
b : WithTop α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) b ↔ none ≤ b
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
b : WithTop α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝) ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) b ↔
    Option.some val✝ ≤ b
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ↔ none ≤ none
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝) ↔
    none ≤ Option.some val✝
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝) ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ↔
    Option.some val✝ ≤ none
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝¹ val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝¹) ≤
      ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝) ↔
    Option.some val✝¹ ≤ Option.some val✝
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ¬none ≤ Option.some val✝
[PROOFSTEP]
exact not_top_le_coe _


[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ count a (dedup (Quot.mk Setoid.r x✝)) = if a ∈ Quot.mk Setoid.r x✝ then 1 else 0
[PROOFSTEP]
simp only [quot_mk_to_coe'', coe_dedup, mem_coe, List.mem_dedup, coe_nodup, coe_count]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ List.count a (List.dedup x✝) = if a ∈ x✝ then 1 else 0
[PROOFSTEP]
apply List.count_dedup _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
⊢ dedup (bind (dedup m) f) = dedup (bind m f)
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ count x (dedup (bind (dedup m) f)) = count x (dedup (bind m f))
[PROOFSTEP]
simp_rw [count_dedup]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ (if x ∈ bind (dedup m) f then 1 else 0) = if x ∈ bind m f then 1 else 0
[PROOFSTEP]
refine if_congr ?_ rfl rfl
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ x ∈ bind (dedup m) f ↔ x ∈ bind m f
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
⊢ s ≤ dedup s ↔ Nodup s
[PROOFSTEP]
rw [le_dedup, and_iff_right le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Multiset α
⊢ dedup s = dedup t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t
[PROOFSTEP]
simp [Nodup.ext]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
⊢ dedup (map f (dedup s)) = dedup (map f s)
[PROOFSTEP]
simp [dedup_ext]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ dedup (n • s) = dedup s
[PROOFSTEP]
ext a
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
a : α
⊢ count a (dedup (n • s)) = count a (dedup s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
a : α
h : a ∈ s
⊢ count a (dedup (n • s)) = count a (dedup s)
[PROOFSTEP]
simp [h, h0]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
a : α
h : ¬a ∈ s
⊢ count a (dedup (n • s)) = count a (dedup s)
[PROOFSTEP]
simp [h, h0]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Multiset α
hno : Nodup s
⊢ s ≤ Multiset.dedup t ↔ s ≤ t
[PROOFSTEP]
simp [le_dedup, hno]
[GOAL]
α : Type u_1
s t : Multiset α
n : ℕ
h : Nodup s
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t
[PROOFSTEP]
classical
rw [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le]
simp [hn]
[GOAL]
α : Type u_1
s t : Multiset α
n : ℕ
h : Nodup s
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t
[PROOFSTEP]
rw [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le]
[GOAL]
α : Type u_1
s t : Multiset α
n : ℕ
h : Nodup s
hn : n ≠ 0
⊢ s ≤ Multiset.dedup t ↔ s ≤ Multiset.dedup (n • t)
[PROOFSTEP]
simp [hn]


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
h : a ∈ s
⊢ ↑card (ndinsert a s) = ↑card s
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ ↑card (ndinsert a s) = ↑card s + 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
⊢ dedup (a ::ₘ s) = ndinsert a (dedup s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
h : a ∈ s
⊢ dedup (a ::ₘ s) = ndinsert a (dedup s)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ dedup (a ::ₘ s) = ndinsert a (dedup s)
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∈ s
⊢ ndinsert a s ≤ t
[PROOFSTEP]
simp [h, l]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ ndinsert a s ≤ t
[PROOFSTEP]
rw [ndinsert_of_not_mem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_not_mem h, cons_erase m]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ s ≤ t
[PROOFSTEP]
exact l
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
⊢ ∀ (t : Multiset α) (eq : ndinsert a s = t),
    attach t =
      ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht : ndinsert a s = t
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
rw [ndinsert_of_mem h] at ht
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
subst ht
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
h : a ∈ s
ht : ndinsert a s = s
⊢ attach s =
    ndinsert { val := a, property := (_ : a ∈ s) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) (attach s))
[PROOFSTEP]
rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
rw [ndinsert_of_not_mem h] at ht
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : a ::ₘ s = t
h : ¬a ∈ s
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
subst ht
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
h : ¬a ∈ s
ht : ndinsert a s = a ::ₘ s
⊢ attach (a ::ₘ s) =
    ndinsert { val := a, property := (_ : a ∈ a ::ₘ s) }
      (map (fun p => { val := ↑p, property := (_ : ↑p ∈ a ::ₘ s) }) (attach s))
[PROOFSTEP]
simp [attach_cons, h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ Disjoint (ndinsert a s) t ↔ Disjoint (a ::ₘ s) t
[PROOFSTEP]
simp [Disjoint]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ Disjoint s (ndinsert a t) ↔ ¬a ∈ s ∧ Disjoint s t
[PROOFSTEP]
rw [disjoint_comm, disjoint_ndinsert_left]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t u : Multiset α
⊢ ndunion 0 t ≤ u ↔ 0 ⊆ u ∧ t ≤ u
[PROOFSTEP]
simp [zero_ndunion]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t u : Multiset α
x✝¹ : α
x✝ : Multiset α
h : ndunion x✝ t ≤ u ↔ x✝ ⊆ u ∧ t ≤ u
⊢ ndunion (x✝¹ ::ₘ x✝) t ≤ u ↔ x✝¹ ::ₘ x✝ ⊆ u ∧ t ≤ u
[PROOFSTEP]
simp only [cons_ndunion, mem_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h, and_assoc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
h : a ∈ t
⊢ ndinter (a ::ₘ s) t = a ::ₘ ndinter s t
[PROOFSTEP]
simp [ndinter, h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
h : ¬a ∈ t
⊢ ndinter (a ::ₘ s) t = ndinter s t
[PROOFSTEP]
simp [ndinter, h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
a : α
⊢ a ∈ ndinter s t ↔ a ∈ s ∧ a ∈ t
[PROOFSTEP]
simp [ndinter, mem_filter]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t u : Multiset α
⊢ s ≤ ndinter t u ↔ s ≤ t ∧ s ⊆ u
[PROOFSTEP]
simp [ndinter, le_filter, subset_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
⊢ ndinter s t = 0 ↔ Disjoint s t
[PROOFSTEP]
rw [← subset_zero]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
⊢ ndinter s t ⊆ 0 ↔ Disjoint s t
[PROOFSTEP]
simp [subset_iff, Disjoint]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Finite (α × β)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Finite (α × β)
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Finite (α × β)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Finite (α ⊕ β)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Finite (α ⊕ β)
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Finite (α ⊕ β)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
β : α → Type u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) × β a)
[PROOFSTEP]
letI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
β : α → Type u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this : Fintype α := Fintype.ofFinite α
⊢ Finite ((a : α) × β a)
[PROOFSTEP]
letI := fun a => Fintype.ofFinite (β a)
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
β : α → Type u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this✝ : Fintype α := Fintype.ofFinite α
this : (a : α) → Fintype (β a) := fun a => Fintype.ofFinite (β a)
⊢ Finite ((a : α) × β a)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ Finite (Set α)
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
val✝ : Fintype α
⊢ Finite (Set α)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : α → Sort u_5
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) → β a)
[PROOFSTEP]
haveI := Fintype.ofFinite (PLift α)
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : α → Sort u_5
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this : Fintype (PLift α)
⊢ Finite ((a : α) → β a)
[PROOFSTEP]
haveI := fun a => Fintype.ofFinite (PLift (β a))
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : α → Sort u_5
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this✝ : Fintype (PLift α)
this : (a : α) → Fintype (PLift (β a))
⊢ Finite ((a : α) → β a)
[PROOFSTEP]
exact Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a))) (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
n : ℕ
⊢ Finite (Vector α n)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
n : ℕ
this : Fintype α
⊢ Finite (Vector α n)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
⊢ Finite (α ↪ β)
[PROOFSTEP]
cases' isEmpty_or_nonempty (α ↪ β) with _ h
[GOAL]
case inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
h✝ : IsEmpty (α ↪ β)
⊢ Finite (α ↪ β)
[PROOFSTEP]
apply Finite.of_subsingleton
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)
[PROOFSTEP]
refine' h.elim fun f => _
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
⊢ Finite (α ↪ β)
[PROOFSTEP]
haveI : Finite α := Finite.of_injective _ f.injective
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
this : Finite α
⊢ Finite (α ↪ β)
[PROOFSTEP]
exact Finite.of_injective _ FunLike.coe_injective
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
e₁ e₂ : α ≃ β
h : Equiv.toEmbedding e₁ = Equiv.toEmbedding e₂
⊢ ∀ (x : α), ↑e₁ x = ↑e₂ x
[PROOFSTEP]
convert FunLike.congr_fun h using 0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
⊢ Finite (Sym α n)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
this : Fintype α
⊢ Finite (Sym α n)
[PROOFSTEP]
infer_instance


[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ antidiagonal (Quotient.mk (isSetoid α) l) ↔ x.fst + x.snd = Quotient.mk (isSetoid α) l
[PROOFSTEP]
dsimp only [quot_mk_to_coe, antidiagonal_coe]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ ↑(revzip (powersetAux l)) ↔ x.fst + x.snd = ↑l
[PROOFSTEP]
refine' ⟨fun h => revzip_powersetAux h, fun h ↦ _⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
⊢ x ∈ ↑(revzip (powersetAux l))
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
this : DecidableEq α
⊢ x ∈ ↑(revzip (powersetAux l))
[PROOFSTEP]
simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, ge_iff_le, mem_coe, List.mem_map, mem_powersetAux]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
this : DecidableEq α
⊢ ∃ a, a ≤ x.fst + x.snd ∧ (a, x.fst + x.snd - a) = x
[PROOFSTEP]
cases' x with x₁ x₂
[GOAL]
case mk
α : Type u_1
β : Type u_2
s : Multiset α
l : List α
this : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).fst + (x₁, x₂).snd = ↑l
⊢ ∃ a, a ≤ (x₁, x₂).fst + (x₁, x₂).snd ∧ (a, (x₁, x₂).fst + (x₁, x₂).snd - a) = (x₁, x₂)
[PROOFSTEP]
exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
l : List α
this : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).fst + (x₁, x₂).snd = ↑l
⊢ (x₁, (x₁, x₂).fst + (x₁, x₂).snd - x₁) = (x₁, x₂)
[PROOFSTEP]
rw [add_tsub_cancel_left x₁ x₂]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
l : List α
⊢ map Prod.fst (antidiagonal (Quotient.mk (isSetoid α) l)) = powerset (Quotient.mk (isSetoid α) l)
[PROOFSTEP]
simp [powersetAux']
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
l : List α
⊢ map Prod.snd (antidiagonal (Quotient.mk (isSetoid α) l)) = powerset (Quotient.mk (isSetoid α) l)
[PROOFSTEP]
simp [powersetAux']
[GOAL]
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ antidiagonal (a ::ₘ Quotient.mk (isSetoid α) l) =
    map (Prod.map id (cons a)) (antidiagonal (Quotient.mk (isSetoid α) l)) +
      map (Prod.map (cons a) id) (antidiagonal (Quotient.mk (isSetoid α) l))
[PROOFSTEP]
simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe, coe_map, antidiagonal_coe',
  coe_add]
[GOAL]
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ zip (powersetAux' l ++ List.map (cons a) (powersetAux' l))
      (reverse (List.map (cons a) (powersetAux' l)) ++ reverse (powersetAux' l)) ~
    List.map (fun x => Prod.map id (cons a) x) (zip (powersetAux' l) (reverse (powersetAux' l))) ++
      List.map (fun x => Prod.map (cons a) id x) (zip (powersetAux' l) (reverse (powersetAux' l)))
[PROOFSTEP]
rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
[GOAL]
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ zip (powersetAux' l) (reverse (List.map (cons a) (powersetAux' l))) ++
      zip (List.map (cons a) (powersetAux' l)) (reverse (powersetAux' l)) =
    zip (List.map id (powersetAux' l)) (List.map (cons a) (reverse (powersetAux' l))) ++
      zip (List.map (cons a) (powersetAux' l)) (List.map id (reverse (powersetAux' l)))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ powersetAux' l = List.map id (powersetAux' l)
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (List.map (cons a) (powersetAux' l)) = List.map (cons a) (reverse (powersetAux' l))
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
[PROOFSTEP]
simp
[GOAL]
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (List.map (cons a) (powersetAux' l)) = List.map (cons a) (reverse (powersetAux' l))
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
[PROOFSTEP]
rw [map_reverse]
[GOAL]
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ length (powersetAux' l) = length (reverse (List.map (cons a) (powersetAux' l)))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
⊢ antidiagonal s = map (fun t => (s - t, t)) (powerset s)
[PROOFSTEP]
induction' s using Multiset.induction_on with a s hs
[GOAL]
case empty
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ antidiagonal 0 = map (fun t => (0 - t, t)) (powerset 0)
[PROOFSTEP]
simp only [antidiagonal_zero, powerset_zero, zero_tsub, map_singleton]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
⊢ antidiagonal (a ::ₘ s) = map (fun t => (a ::ₘ s - t, t)) (powerset (a ::ₘ s))
[PROOFSTEP]
simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_mk, id.def, sub_cons,
  erase_cons_head]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
⊢ map (fun x => (s - x, a ::ₘ x)) (powerset s) + map (fun x => (a ::ₘ (s - x), x)) (powerset s) =
    map (fun x => (a ::ₘ s - x, x)) (powerset s) + map (fun x => (s - x, a ::ₘ x)) (powerset s)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
⊢ map (fun x => (a ::ₘ (s - x), x)) (powerset s) + map (fun x => (s - x, a ::ₘ x)) (powerset s) =
    map (fun x => (a ::ₘ s - x, x)) (powerset s) + map (fun x => (s - x, a ::ₘ x)) (powerset s)
[PROOFSTEP]
congr 1
[GOAL]
case cons.e_a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
⊢ map (fun x => (a ::ₘ (s - x), x)) (powerset s) = map (fun x => (a ::ₘ s - x, x)) (powerset s)
[PROOFSTEP]
refine' Multiset.map_congr rfl fun x hx ↦ _
[GOAL]
case cons.e_a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
x : Multiset α
hx : x ∈ powerset s
⊢ (a ::ₘ (s - x), x) = (a ::ₘ s - x, x)
[PROOFSTEP]
rw [cons_sub_of_le _ (mem_powerset.mp hx)]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
⊢ ↑card (antidiagonal s) = 2 ^ ↑card s
[PROOFSTEP]
have := card_powerset s
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
this : ↑card (powerset s) = 2 ^ ↑card s
⊢ ↑card (antidiagonal s) = 2 ^ ↑card s
[PROOFSTEP]
rwa [← antidiagonal_map_fst, card_map] at this
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ prod (map (fun a => f a + g a) 0) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal 0))
[PROOFSTEP]
simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s)) →
      prod (map (fun a => f a + g a) (a ::ₘ s)) =
        sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal (a ::ₘ s)))
[PROOFSTEP]
intro a s ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s✝ : Multiset α
f g : α → β
a : α
s : Multiset α
ih : prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
⊢ prod (map (fun a => f a + g a) (a ::ₘ s)) =
    sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal (a ::ₘ s)))
[PROOFSTEP]
simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a), mul_left_comm (g a),
  sum_map_add, antidiagonal_cons, Prod_map, id_eq, map_add, map_map, Function.comp_apply, mul_assoc, sum_add]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s✝ : Multiset α
f g : α → β
a : α
s : Multiset α
ih : prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
⊢ sum (map (fun i => prod (map f i.fst) * (f a * prod (map g i.snd))) (antidiagonal s)) +
      sum (map (fun i => prod (map f i.fst) * (g a * prod (map g i.snd))) (antidiagonal s)) =
    sum (map (fun x => prod (map f x.fst) * (g a * prod (map g x.snd))) (antidiagonal s)) +
      sum (map (fun i => prod (map f i.fst) * (f a * prod (map g i.snd))) (antidiagonal s))
[PROOFSTEP]
exact add_comm _ _


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
⊢ s = a ::ₘ a ::ₘ t
[PROOFSTEP]
rwa [cons_add, cons_add, zero_add] at s_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a : α
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ Nodup (Quot.mk Setoid.r _l) ↔ ∀ (a : α), count a (Quot.mk Setoid.r _l) ≤ 1
[PROOFSTEP]
simp only [quot_mk_to_coe'', coe_nodup, mem_coe, coe_count]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a : α
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ List.Nodup _l ↔ ∀ (a : α), List.count a _l ≤ 1
[PROOFSTEP]
apply List.nodup_iff_count_le_one
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
⊢ count a s = if a ∈ s then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
h : a ∈ s
⊢ count a s = 1
[PROOFSTEP]
exact count_eq_one_of_mem d h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
h : ¬a ∈ s
⊢ count a s = 0
[PROOFSTEP]
exact count_eq_zero_of_not_mem h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t : Multiset α
a : α
d₁ : Nodup s
d₂ : Nodup t
⊢ Nodup (s + t) ↔ Disjoint s t
[PROOFSTEP]
simp [nodup_add, d₁, d₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : Nodup l
⊢ a ∈ Multiset.erase l b ↔ a ≠ b ∧ a ∈ l
[PROOFSTEP]
rw [d.erase_eq_filter b, mem_filter, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t✝ : Multiset α
a : α
t : Multiset β
l₁ : List α
l₂ : List β
d₁ : Nodup (Quotient.mk (isSetoid α) l₁)
d₂ : Nodup (Quotient.mk (isSetoid β) l₂)
⊢ Nodup (Quotient.mk (isSetoid α) l₁ ×ˢ Quotient.mk (isSetoid β) l₂)
[PROOFSTEP]
simp [List.Nodup.product d₁ d₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t✝ : Multiset α
a : α
σ : α → Type u_4
t : (a : α) → Multiset (σ a)
l₁ : List α
⊢ Nodup (Quot.mk Setoid.r l₁) → (∀ (a : α), Nodup (t a)) → Nodup (Multiset.sigma (Quot.mk Setoid.r l₁) t)
[PROOFSTEP]
choose f hf using fun a => Quotient.exists_rep (t a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t✝ : Multiset α
a : α
σ : α → Type u_4
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), Quotient.mk (isSetoid (σ a)) (f a) = t a
⊢ Nodup (Quot.mk Setoid.r l₁) → (∀ (a : α), Nodup (t a)) → Nodup (Multiset.sigma (Quot.mk Setoid.r l₁) t)
[PROOFSTEP]
simpa [← funext hf] using List.Nodup.sigma
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
s t : Multiset α
x✝ : Nodup s ∧ Nodup t
h₁ : Nodup s
h₂ : Nodup t
a : α
⊢ count a (s ∪ t) ≤ 1
[PROOFSTEP]
rw [count_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
s t : Multiset α
x✝ : Nodup s ∧ Nodup t
h₁ : Nodup s
h₂ : Nodup t
a : α
⊢ max (count a s) (count a t) ≤ 1
[PROOFSTEP]
exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
s : Multiset α
t : α → Multiset β
h₁ : ∀ (a : α), ∃ l, t a = ↑l
t' : α → List β
h' : ∀ (x : α), t x = ↑(t' x)
this : t = fun a => ↑(t' a)
hd : Symmetric fun a b => List.Disjoint (t' a) (t' b)
⊢ ∀ (a : List α),
    Nodup (bind (Quot.mk Setoid.r a) t) ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk Setoid.r a → Nodup (t a_1)) ∧
        Pairwise (fun a b => Disjoint (t a) (t b)) (Quot.mk Setoid.r a)
[PROOFSTEP]
simp [this, List.nodup_bind, pairwise_coe_iff_pairwise hd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ False
[PROOFSTEP]
refine' count_eq_zero.1 _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ count a (s - t) = 0
[PROOFSTEP]
rw [count_sub a s t, tsub_eq_zero_iff_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t
[PROOFSTEP]
exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
x : β
⊢ x ∈ t ↔ x ∈ map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
[PROOFSTEP]
simp only [mem_map, true_and_iff, Subtype.exists, eq_comm, mem_attach]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
x : β
⊢ x ∈ t ↔ ∃ a h, x = i a (_ : ↑{ val := a, property := (_ : a ∈ s) } ∈ s)
[PROOFSTEP]
exact ⟨i_surj _, fun ⟨y, hy⟩ => hy.snd.symm ▸ hi _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
this : t = map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
⊢ map f s = pmap (fun x x_1 => f x) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
[PROOFSTEP]
rw [pmap_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
this : t = map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
⊢ pmap (fun x x_1 => f x) s (_ : ∀ (x : α), x ∈ s → x ∈ s) = map (fun x => f ↑x) (attach s)
[PROOFSTEP]
rw [pmap_eq_map_attach]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
this : t = map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
⊢ map (fun x => f ↑x) (attach s) = map g t
[PROOFSTEP]
rw [this, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
this : t = map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
⊢ map (fun x => f ↑x) (attach s) = map (g ∘ fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
[PROOFSTEP]
exact map_congr rfl fun x _ => h _ _


[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]