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

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
x✝ : Option (β a)
b✝ : β a
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

Tactic:
rw [heq, size_expandIfNecessary, consₘ, length_insertEntry, if_neg h₁, h.size_eq]

Result:
no goals

Proof state:
case h_1
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
x✝ : Option (β a)
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

Tactic:
next heq =>
rw [heq, h.size_eq, length_eraseKey, if_neg h₁]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
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✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
x✝ : Option (β a)
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✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
x✝ : Option (β a)
b✝ : β a
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

Proof state:
case h_2
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
x✝ : Option (β a)
b✝ : β a
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

Tactic:
next heq =>
rw [heq, size_expandIfNecessary, consₘ, length_insertEntry, if_neg h₁, h.size_eq]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
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 (getValueCast? a (toListModel m.val.buckets)) with
      | none => eraseKey a (toListModel m.val.buckets)
      | some v => insertEntry a v (toListModel m.val.buckets)).length

Tactic:
rw [getValueCast?_eq_none <| Bool.not_eq_true _ ▸ h₁]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
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

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : containsKey a (toListModel m.val.buckets) = true
⊢ (if containsₘ ⟨withComputedSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l), ⋯⟩ a = true then
      (toListModel m.val.buckets).length
    else (toListModel m.val.buckets).length - 1) =
    if (f (some (getValueCast a (toListModel m.val.buckets) h₁))).isSome = true then (toListModel m.val.buckets).length
    else (toListModel m.val.buckets).length - 1

Tactic:
rw [containsₘ_eq_containsKey (by apply wfImp_updateBucket_alter h)]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : containsKey a (toListModel m.val.buckets) = true
⊢ (if
        containsKey a
            (toListModel
              ⟨withComputedSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l), ⋯⟩.val.buckets) =
          true then
      (toListModel m.val.buckets).length
    else (toListModel m.val.buckets).length - 1) =
    if (f (some (getValueCast a (toListModel m.val.buckets) h₁))).isSome = true then (toListModel m.val.buckets).length
    else (toListModel m.val.buckets).length - 1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : containsKey a (toListModel m.val.buckets) = true
⊢ (if containsKey a (toListModel (updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l)) = true then
      (toListModel m.val.buckets).length
    else (toListModel m.val.buckets).length - 1) =
    if (f (some (getValueCast a (toListModel m.val.buckets) h₁))).isSome = true then (toListModel m.val.buckets).length
    else (toListModel m.val.buckets).length - 1

Tactic:
simp only [containsKey_of_perm <| toListModel_updateBucket_alter h]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : containsKey a (toListModel m.val.buckets) = true
⊢ (if containsKey a (alterKey a f (toListModel m.val.buckets)) = true then (toListModel m.val.buckets).length
    else (toListModel m.val.buckets).length - 1) =
    if (f (some (getValueCast a (toListModel m.val.buckets) h₁))).isSome = true then (toListModel m.val.buckets).length
    else (toListModel m.val.buckets).length - 1

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

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

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h₁ : ¬containsKey a (toListModel m.val.buckets) = true
⊢ (match f none with
        | none => m
        | some b => (m.consₘ a b).expandIfNecessary).val.size =
    (alterKey a f (toListModel m.val.buckets)).length