-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.mapVal {α β γ} {f : α → β → γ} [BEq α] [Hashable α]
    {m : Imp α β} (H : WF m) : WF (mapVal f m)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (j : AssocList α β),
    j ∈ m.buckets.val.toList → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.mapVal f j).toList

Tactic:
simp only [AssocList.toList_mapVal, List.pairwise_map]

Result:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (j : AssocList α β),
    j ∈ m.buckets.val.toList → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) j.toList

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

Tactic:
simp only [Array.toList_map, List.forall_mem_map]

Result:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (j : AssocList α β),
    j ∈ m.buckets.val.toList → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.mapVal f j).toList

Proof state:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
i : Nat
h✝ : i < ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val.size
h : i < m.buckets.val.size
⊢ ∀ (a : α × β), a ∈ m.buckets.val[i].toList → ((hash a.fst).toUSize % USize.ofNat m.buckets.val.size).toNat = i

Tactic:
intro a m

Result:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Imp α β
H : m✝.WF
h₁ : m✝.size = m✝.buckets.size
h₂ : m✝.buckets.WF
i : Nat
h✝ : i < ⟨Array.map (AssocList.mapVal f) m✝.buckets.val, ⋯⟩.val.size
h : i < m✝.buckets.val.size
a : α × β
m : a ∈ m✝.buckets.val[i].toList
⊢ ((hash a.fst).toUSize % USize.ofNat m✝.buckets.val.size).toNat = i

Proof state:
case refine_1.e_a.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
l : AssocList α β
⊢ l.toList.length = ((fun x => x.toList.length) ∘ AssocList.mapVal f) l

Tactic:
simp

Result:
no goals

Proof state:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Imp α β
H : m✝.WF
h₁ : m✝.size = m✝.buckets.size
h₂ : m✝.buckets.WF
i : Nat
h✝ : i < ⟨Array.map (AssocList.mapVal f) m✝.buckets.val, ⋯⟩.val.size
h : i < m✝.buckets.val.size
a : α × β
m : a ∈ m✝.buckets.val[i].toList
⊢ ((hash a.fst).toUSize % USize.ofNat m✝.buckets.val.size).toNat = i

Tactic:
apply h₂.2 _ _ _ m

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ m.buckets.size = Buckets.size ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩ ∧
    Buckets.WF ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩

Tactic:
refine ⟨?_, ?_, fun i h => ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ m.buckets.size = Buckets.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 : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α γ),
    bucket ∈ ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val.toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) bucket.toList

case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
i : Nat
h : i < ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val.size
⊢ AssocList.All
    (fun k x => ((hash k).toUSize % USize.ofNat ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val.size).toNat = i)
    ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val[i]

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (j : AssocList α β),
    j ∈ m.buckets.val.toList → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) j.toList

Tactic:
exact fun _ => h₂.1 _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ (Imp.mapVal f m).WF

Tactic:
simp only [Imp.mapVal, h₁, Buckets.mapVal, WF_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ m.buckets.size = Buckets.size ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩ ∧
    Buckets.WF ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ (List.map (fun x => x.toList.length) m.buckets.val.toList).sum =
    (List.map ((fun x => x.toList.length) ∘ AssocList.mapVal f) m.buckets.val.toList).sum

Tactic:
congr

Result:
case refine_1.e_a.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ (fun x => x.toList.length) = (fun x => x.toList.length) ∘ AssocList.mapVal f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
⊢ (Imp.mapVal f m).WF

Tactic:
have ⟨h₁, h₂⟩ := H.out

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ (Imp.mapVal f m).WF

Proof state:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
i : Nat
h : i < ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val.size
⊢ AssocList.All
    (fun k x => ((hash k).toUSize % USize.ofNat ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val.size).toNat = i)
    ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val[i]

Tactic:
simp only [Array.size_map, AssocList.All, Array.getElem_map, AssocList.toList_mapVal,
  List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h ⊢

Result:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
i : Nat
h✝ : i < ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩.val.size
h : i < m.buckets.val.size
⊢ ∀ (a : α × β), a ∈ m.buckets.val[i].toList → ((hash a.fst).toUSize % USize.ofNat m.buckets.val.size).toNat = i