α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ WF (Imp.mapVal f m)
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
⊢ WF (Imp.mapVal f m)
have ⟨h₁, h₂⟩ := H.out
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ Bucket.size m.buckets =
      Bucket.size
        { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) } ∧
    Bucket.WF
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
        property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ WF (Imp.mapVal f m)
simp [Imp.mapVal, Bucket.mapVal, WF_iff, h₁]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ Bucket.size m.buckets =
    Bucket.size
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
        property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α γ),
    bucket ∈
        { val := Array.map (AssocList.mapVal f) m.buckets.val,
              property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val.data →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)

case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
i : Nat
h :
  i <
    Array.size
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val
⊢ AssocList.All
    (fun k x =>
      USize.toNat
          (UInt64.toUSize (hash k) %
            Array.size
              { val := Array.map (AssocList.mapVal f) m.buckets.val,
                  property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val) =
        i)
    { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val[i]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ Bucket.size m.buckets =
      Bucket.size
        { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) } ∧
    Bucket.WF
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
        property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }
refine ⟨?_, ?_, fun i h => ?_⟩
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) m.buckets.val.data) =
    Nat.sum (List.map ((fun x => List.length (AssocList.toList x)) ∘ AssocList.mapVal f) m.buckets.val.data)
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ Bucket.size m.buckets =
    Bucket.size
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
        property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }
simp [Bucket.size]
case refine_1.e_l.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ (fun x => List.length (AssocList.toList x)) = (fun x => List.length (AssocList.toList x)) ∘ AssocList.mapVal f
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) m.buckets.val.data) =
    Nat.sum (List.map ((fun x => List.length (AssocList.toList x)) ∘ AssocList.mapVal f) m.buckets.val.data)
congr
case refine_1.e_l.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
l : AssocList α β
⊢ List.length (AssocList.toList l) = ((fun x => List.length (AssocList.toList x)) ∘ AssocList.mapVal f) l
case refine_1.e_l.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ (fun x => List.length (AssocList.toList x)) = (fun x => List.length (AssocList.toList x)) ∘ AssocList.mapVal f
funext l
no goals
case refine_1.e_l.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
l : AssocList α β
⊢ List.length (AssocList.toList l) = ((fun x => List.length (AssocList.toList x)) ∘ AssocList.mapVal f) l
simp
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (j : AssocList α β),
    j ∈ m.buckets.val.data →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList (AssocList.mapVal f j))
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α γ),
    bucket ∈
        { val := Array.map (AssocList.mapVal f) m.buckets.val,
              property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val.data →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
simp only [Array.map_data, List.forall_mem_map_iff]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (j : AssocList α β),
    j ∈ m.buckets.val.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList j)
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (j : AssocList α β),
    j ∈ m.buckets.val.data →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList (AssocList.mapVal f j))
simp [List.pairwise_map]
no goals
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (j : AssocList α β),
    j ∈ m.buckets.val.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList j)
exact fun _ => h₂.1 _
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
i : Nat
h✝ :
  i <
    Array.size
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val
h : i < Array.size m.buckets.val
⊢ ∀ (a : α × γ) (x : α × β),
    x ∈ AssocList.toList m.buckets.val[i] →
      (x.fst, f x.fst x.snd) = a → USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) = i
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
i : Nat
h :
  i <
    Array.size
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val
⊢ AssocList.All
    (fun k x =>
      USize.toNat
          (UInt64.toUSize (hash k) %
            Array.size
              { val := Array.map (AssocList.mapVal f) m.buckets.val,
                  property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val) =
        i)
    { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val[i]
simp [AssocList.All] at h ⊢
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
i : Nat
h✝ :
  i <
    Array.size
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val
h : i < Array.size m.buckets.val
x : α × β
hx : x ∈ AssocList.toList m.buckets.val[i]
⊢ USize.toNat (UInt64.toUSize (hash (x.fst, f x.fst x.snd).fst) % Array.size m.buckets.val) = i
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
i : Nat
h✝ :
  i <
    Array.size
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val
h : i < Array.size m.buckets.val
⊢ ∀ (a : α × γ) (x : α × β),
    x ∈ AssocList.toList m.buckets.val[i] →
      (x.fst, f x.fst x.snd) = a → USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) = i
rintro a x hx rfl
no goals
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : WF m
h₁ : m.size = Bucket.size m.buckets
h₂ : Bucket.WF m.buckets
i : Nat
h✝ :
  i <
    Array.size
      { val := Array.map (AssocList.mapVal f) m.buckets.val,
          property := (_ : 0 < Array.size (Array.map (AssocList.mapVal f) m.buckets.val)) }.val
h : i < Array.size m.buckets.val
x : α × β
hx : x ∈ AssocList.toList m.buckets.val[i]
⊢ USize.toNat (UInt64.toUSize (hash (x.fst, f x.fst x.snd).fst) % Array.size m.buckets.val) = i
apply h₂.2 _ _ x hx