-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_expandIfNecessary [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β)
    (h : Raw.WFImp m.1) : Raw.WFImp (expandIfNecessary m).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ Raw.WFImp
    (if Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size then
        ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩
      else
        match expand ⟨m.1.buckets, ⋯⟩ with
        | ⟨buckets', h'⟩ => ⟨{ size := m.1.size, buckets := buckets' }, h'⟩).val

Tactic:
dsimp

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ Raw.WFImp
    (if Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size then
        ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩
      else ⟨{ size := m.1.size, buckets := (expand ⟨m.1.buckets, ⋯⟩).val }, ⋯⟩).val

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
size : Nat
buckets : Array (AssocList α β)
hm : 0 < { size := size, buckets := buckets }.buckets.size
h : Raw.WFImp ⟨{ size := size, buckets := buckets }, hm⟩.val
h✝ :
  ¬Std.DHashMap.Internal.numBucketsForCapacity✝ ⟨{ size := size, buckets := buckets }, hm⟩.1.size ≤
      ⟨{ size := size, buckets := buckets }, hm⟩.1.buckets.size
this : toListModel (expand ⟨buckets, hm⟩).val ~ toListModel ⟨buckets, hm⟩.val
⊢ Raw.WFImp
    ⟨{ size := ⟨{ size := size, buckets := buckets }, hm⟩.1.size,
          buckets := (expand ⟨⟨{ size := size, buckets := buckets }, hm⟩.1.buckets, ⋯⟩).val },
        ⋯⟩.val

Tactic:
dsimp at this

Result:
case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
size : Nat
buckets : Array (AssocList α β)
hm : 0 < { size := size, buckets := buckets }.buckets.size
h : Raw.WFImp ⟨{ size := size, buckets := buckets }, hm⟩.val
h✝ :
  ¬Std.DHashMap.Internal.numBucketsForCapacity✝ ⟨{ size := size, buckets := buckets }, hm⟩.1.size ≤
      ⟨{ size := size, buckets := buckets }, hm⟩.1.buckets.size
this : toListModel (expand ⟨buckets, hm⟩).val ~ toListModel buckets
⊢ Raw.WFImp
    ⟨{ size := ⟨{ size := size, buckets := buckets }, hm⟩.1.size,
          buckets := (expand ⟨⟨{ size := size, buckets := buckets }, hm⟩.1.buckets, ⋯⟩).val },
        ⋯⟩.val

Proof state:
case isFalse.refine_2
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
size : Nat
buckets : Array (AssocList α β)
hm : 0 < { size := size, buckets := buckets }.buckets.size
h : Raw.WFImp ⟨{ size := size, buckets := buckets }, hm⟩.val
h✝ :
  ¬Std.DHashMap.Internal.numBucketsForCapacity✝ ⟨{ size := size, buckets := buckets }, hm⟩.1.size ≤
      ⟨{ size := size, buckets := buckets }, hm⟩.1.buckets.size
this : toListModel (expand ⟨buckets, hm⟩).val ~ toListModel buckets
⊢ ⟨{ size := ⟨{ size := size, buckets := buckets }, hm⟩.1.size,
            buckets := (expand ⟨⟨{ size := size, buckets := buckets }, hm⟩.1.buckets, ⋯⟩).val },
          ⋯⟩.val.size =
    (toListModel
        ⟨{ size := ⟨{ size := size, buckets := buckets }, hm⟩.1.size,
                buckets := (expand ⟨⟨{ size := size, buckets := buckets }, hm⟩.1.buckets, ⋯⟩).val },
              ⋯⟩.val.buckets).length

Tactic:
refine h.size_eq.trans ?_

Result:
case isFalse.refine_2
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
size : Nat
buckets : Array (AssocList α β)
hm : 0 < { size := size, buckets := buckets }.buckets.size
h : Raw.WFImp ⟨{ size := size, buckets := buckets }, hm⟩.val
h✝ :
  ¬Std.DHashMap.Internal.numBucketsForCapacity✝ ⟨{ size := size, buckets := buckets }, hm⟩.1.size ≤
      ⟨{ size := size, buckets := buckets }, hm⟩.1.buckets.size
this : toListModel (expand ⟨buckets, hm⟩).val ~ toListModel buckets
⊢ (toListModel ⟨{ size := size, buckets := buckets }, hm⟩.val.buckets).length =
    (toListModel
        ⟨{ size := ⟨{ size := size, buckets := buckets }, hm⟩.1.size,
                buckets := (expand ⟨⟨{ size := size, buckets := buckets }, hm⟩.1.buckets, ⋯⟩).val },
              ⋯⟩.val.buckets).length

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ Raw.WFImp
    (if Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size then
        ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩
      else ⟨{ size := m.1.size, buckets := (expand ⟨m.1.buckets, ⋯⟩).val }, ⋯⟩).val

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
h✝ : Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size
⊢ Raw.WFImp ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩.val

case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
h✝ : ¬Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size
⊢ Raw.WFImp ⟨{ size := m.1.size, buckets := (expand ⟨m.1.buckets, ⋯⟩).val }, ⋯⟩.val

Proof state:
case isFalse.refine_1
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
size : Nat
buckets : Array (AssocList α β)
hm : 0 < { size := size, buckets := buckets }.buckets.size
h : Raw.WFImp ⟨{ size := size, buckets := buckets }, hm⟩.val
h✝ :
  ¬Std.DHashMap.Internal.numBucketsForCapacity✝ ⟨{ size := size, buckets := buckets }, hm⟩.1.size ≤
      ⟨{ size := size, buckets := buckets }, hm⟩.1.buckets.size
this : toListModel (expand ⟨buckets, hm⟩).val ~ toListModel buckets
⊢ IsHashSelf
    ⟨{ size := ⟨{ size := size, buckets := buckets }, hm⟩.1.size,
            buckets := (expand ⟨⟨{ size := size, buckets := buckets }, hm⟩.1.buckets, ⋯⟩).val },
          ⋯⟩.val.buckets

Tactic:
simpa using isHashSelf_expand

Result:
no goals

Proof state:
case isFalse.refine_3
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
size : Nat
buckets : Array (AssocList α β)
hm : 0 < { size := size, buckets := buckets }.buckets.size
h : Raw.WFImp ⟨{ size := size, buckets := buckets }, hm⟩.val
h✝ :
  ¬Std.DHashMap.Internal.numBucketsForCapacity✝ ⟨{ size := size, buckets := buckets }, hm⟩.1.size ≤
      ⟨{ size := size, buckets := buckets }, hm⟩.1.buckets.size
this : toListModel (expand ⟨buckets, hm⟩).val ~ toListModel buckets
⊢ DistinctKeys
    (toListModel
      ⟨{ size := ⟨{ size := size, buckets := buckets }, hm⟩.1.size,
              buckets := (expand ⟨⟨{ size := size, buckets := buckets }, hm⟩.1.buckets, ⋯⟩).val },
            ⋯⟩.val.buckets)

Tactic:
simpa using h.distinct.perm this

Result:
no goals

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
h✝ : Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size
⊢ Raw.WFImp ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩.val

Tactic:
exact h

Result:
no goals