-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α]
    (m : Raw₀ α (fun _ => β)) (h : Raw.WFImp m.1) (a : α) (f : Option β → Option β) :
  IsHashSelf (Const.alterₘ m a f).1.buckets

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 β
⊢ IsHashSelf (alterₘ m a f).val.buckets

Tactic:
dsimp only [alterₘ, withComputedSize]

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 β
⊢ IsHashSelf
    (if h : m.containsₘ a = true then
          ⟨{
              size :=
                if
                    containsₘ
                        ⟨{ size := computeSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l),
                            buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l },
                          ⋯⟩
                        a =
                      true then
                  m.val.size
                else m.val.size - 1,
              buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l },
            ⋯⟩
        else
          match f none with
          | none => m
          | some b => (m.consₘ a b).expandIfNecessary).val.buckets

Proof state:
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 β
hc : ¬m.containsₘ a = true
x✝ : Option β
heq✝ : f none = none
⊢ IsHashSelf m.val.buckets

Tactic:
exact h.buckets_hash_self

Result:
no goals

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 β
hc : ¬m.containsₘ a = true
⊢ IsHashSelf
    (match f none with
        | none => m
        | some b => (m.consₘ a b).expandIfNecessary).val.buckets

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 β
hc : ¬m.containsₘ a = true
x✝ : Option β
heq✝ : f none = none
⊢ IsHashSelf m.val.buckets

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 β
hc : ¬m.containsₘ a = true
x✝ : Option β
b✝ : β
heq✝ : f none = some b✝
⊢ IsHashSelf (m.consₘ a b✝).expandIfNecessary.val.buckets

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 β
⊢ IsHashSelf
    (if h : m.containsₘ a = true then
          ⟨{
              size :=
                if
                    containsₘ
                        ⟨{ size := computeSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l),
                            buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l },
                          ⋯⟩
                        a =
                      true then
                  m.val.size
                else m.val.size - 1,
              buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l },
            ⋯⟩
        else
          match f none with
          | none => m
          | some b => (m.consₘ a b).expandIfNecessary).val.buckets

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
⊢ IsHashSelf
    ⟨{
            size :=
              if
                  containsₘ
                      ⟨{ size := computeSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l),
                          buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l },
                        ⋯⟩
                      a =
                    true then
                m.val.size
              else m.val.size - 1,
            buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l },
          ⋯⟩.val.buckets

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
⊢ IsHashSelf
    (match f none with
        | none => m
        | some b => (m.consₘ a b).expandIfNecessary).val.buckets

Proof state:
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 β
hc : ¬m.containsₘ a = true
x✝ : Option β
b✝ : β
heq✝ : f none = some b✝
⊢ m.containsₘ a = false

Tactic:
exact Bool.not_eq_true _ ▸ hc

Result:
no goals

Proof state:
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
⊢ IsHashSelf
    ⟨{
            size :=
              if
                  containsₘ
                      ⟨{ size := computeSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l),
                          buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l },
                        ⋯⟩
                      a =
                    true then
                m.val.size
              else m.val.size - 1,
            buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l },
          ⋯⟩.val.buckets

Tactic:
exact isHashSelf_updateBucket_alter h

Result:
no goals

Proof state:
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 β
hc : ¬m.containsₘ a = true
x✝ : Option β
b✝ : β
heq✝ : f none = some b✝
⊢ IsHashSelf (m.consₘ a b✝).expandIfNecessary.val.buckets

Tactic:
refine (wfImp_expandIfNecessary _ (wfImp_consₘ _ h _ _ ?_)).buckets_hash_self

Result:
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 β
hc : ¬m.containsₘ a = true
x✝ : Option β
b✝ : β
heq✝ : f none = some b✝
⊢ m.containsₘ a = false