-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)}
    (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : Raw.WFImp (Const.alterₘ m a f).1 where
  buckets_hash_self := isHashSelf_alterₘ m h a f
  distinct := DistinctKeys.perm (toListModel_alterₘ h) h.distinct.constAlterKey
  size_eq

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ (alterₘ m a f).val.size = (toListModel (alterₘ m a f).val.buckets).length

Tactic:
rw [← Perm.length_eq (toListModel_alterₘ h).symm, alterₘ]

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ (if h : m.containsₘ a = true then
          let buckets' := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l;
          let size' := if containsₘ ⟨withComputedSize buckets', ⋯⟩ a = true then m.val.size else m.val.size - 1;
          ⟨{ size := size', buckets := buckets' }, ⋯⟩
        else
          match f none with
          | none => m
          | some b => (m.consₘ a b).expandIfNecessary).val.size =
    (Const.alterKey a f (toListModel m.val.buckets)).length

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
h₁ : m.containsₘ a = true
⊢ (let buckets' := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l;
        let size' := if containsₘ ⟨withComputedSize buckets', ⋯⟩ a = true then m.val.size else m.val.size - 1;
        ⟨{ size := size', buckets := buckets' }, ⋯⟩).val.size =
    (Const.alterKey a f (toListModel m.val.buckets)).length

Tactic:
rw [containsₘ_eq_containsKey h] at h₁

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
h₁ : containsKey a (toListModel m.val.buckets) = true
⊢ (let buckets' := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l;
        let size' := if containsₘ ⟨withComputedSize buckets', ⋯⟩ a = true then m.val.size else m.val.size - 1;
        ⟨{ size := size', buckets := buckets' }, ⋯⟩).val.size =
    (Const.alterKey a f (toListModel m.val.buckets)).length

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ (if h : m.containsₘ a = true then
          let buckets' := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l;
          let size' := if containsₘ ⟨withComputedSize buckets', ⋯⟩ a = true then m.val.size else m.val.size - 1;
          ⟨{ size := size', buckets := buckets' }, ⋯⟩
        else
          match f none with
          | none => m
          | some b => (m.consₘ a b).expandIfNecessary).val.size =
    (Const.alterKey a f (toListModel m.val.buckets)).length

Tactic:
split

Result:
case isTrue
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
h✝ : m.containsₘ a = true
⊢ (let buckets' := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l;
        let size' := if containsₘ ⟨withComputedSize buckets', ⋯⟩ a = true then m.val.size else m.val.size - 1;
        ⟨{ size := size', buckets := buckets' }, ⋯⟩).val.size =
    (Const.alterKey a f (toListModel m.val.buckets)).length

case isFalse
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
h✝ : ¬m.containsₘ a = true
⊢ (match f none with
        | none => m
        | some b => (m.consₘ a b).expandIfNecessary).val.size =
    (Const.alterKey a f (toListModel m.val.buckets)).length

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
⊢ (match f none with
        | none => m
        | some b => (m.consₘ a b).expandIfNecessary).val.size =
    (match f none with
      | none => eraseKey a (toListModel m.val.buckets)
      | some v => insertEntry a v (toListModel m.val.buckets)).length

Tactic:
split

Result:
case h_1
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
x✝ : Option β
heq✝ : f none = none
⊢ m.val.size =
    (match f none with
      | none => eraseKey a (toListModel m.val.buckets)
      | some v => insertEntry a v (toListModel m.val.buckets)).length

case h_2
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
x✝ : Option β
b✝ : β
heq✝ : f none = some b✝
⊢ (m.consₘ a b✝).expandIfNecessary.val.size =
    (match f none with
      | none => eraseKey a (toListModel m.val.buckets)
      | some v => insertEntry a v (toListModel m.val.buckets)).length