no goals
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
h : WF m
⊢ m.size = Bucket.size m.buckets ∧ Bucket.WF m.buckets
induction h with
| mk h₁ h₂ => exact ⟨h₁, h₂⟩
| @empty' _ h => exact ⟨(Bucket.mk_size h).symm, .mk' h⟩
| insert _ ih => exact ⟨insert_size ih.1, insert_WF ih.2⟩
| erase _ ih => exact ⟨erase_size ih.1, erase_WF ih.2⟩
| modify _ ih => exact ⟨modify_size ih.1, modify_WF ih.2⟩
no goals
case mk
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m m✝ : Imp α β
h₁ : m✝.size = Bucket.size m✝.buckets
h₂ : Bucket.WF m✝.buckets
⊢ m✝.size = Bucket.size m✝.buckets ∧ Bucket.WF m✝.buckets
exact ⟨h₁, h₂⟩
no goals
case empty'
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
n✝ : Nat
h : 0 < n✝
⊢ (Imp.empty' n✝).size = Bucket.size (Imp.empty' n✝).buckets ∧ Bucket.WF (Imp.empty' n✝).buckets
exact ⟨(Bucket.mk_size h).symm, .mk' h⟩
no goals
case insert
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m m✝ : Imp α β
a✝¹ : α
b✝ : β
a✝ : WF m✝
ih : m✝.size = Bucket.size m✝.buckets ∧ Bucket.WF m✝.buckets
⊢ (Imp.insert m✝ a✝¹ b✝).size = Bucket.size (Imp.insert m✝ a✝¹ b✝).buckets ∧ Bucket.WF (Imp.insert m✝ a✝¹ b✝).buckets
exact ⟨insert_size ih.1, insert_WF ih.2⟩
no goals
case erase
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m m✝ : Imp α β
a✝¹ : α
a✝ : WF m✝
ih : m✝.size = Bucket.size m✝.buckets ∧ Bucket.WF m✝.buckets
⊢ (Imp.erase m✝ a✝¹).size = Bucket.size (Imp.erase m✝ a✝¹).buckets ∧ Bucket.WF (Imp.erase m✝ a✝¹).buckets
exact ⟨erase_size ih.1, erase_WF ih.2⟩
no goals
case modify
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m m✝ : Imp α β
a✝¹ : α
f✝ : α → β → β
a✝ : WF m✝
ih : m✝.size = Bucket.size m✝.buckets ∧ Bucket.WF m✝.buckets
⊢ (Imp.modify m✝ a✝¹ f✝).size = Bucket.size (Imp.modify m✝ a✝¹ f✝).buckets ∧ Bucket.WF (Imp.modify m✝ a✝¹ f✝).buckets
exact ⟨modify_size ih.1, modify_WF ih.2⟩