-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_expandIfNecessary [BEq α] [Hashable α] [PartialEquivBEq α] (m : Raw₀ α β) :
    Perm (toListModel (expandIfNecessary m).1.2) (toListModel m.1.2)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
m : Raw₀ α β
⊢ toListModel
      (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.buckets ~
    toListModel m.val.buckets

Tactic:
split

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

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

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

Tactic:
dsimp

Result:
case isFalse
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
m : Raw₀ α β
h✝ : ¬Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size
⊢ toListModel (expand ⟨m.1.buckets, ⋯⟩).val ~ toListModel m.val.buckets

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
m : Raw₀ α β
h✝ : ¬Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size
⊢ toListModel (expand ⟨m.1.buckets, ⋯⟩).val ~ toListModel m.val.buckets

Tactic:
exact toListModel_expand

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
m : Raw₀ α β
⊢ toListModel
      (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.buckets ~
    toListModel m.val.buckets

Tactic:
dsimp

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
m : Raw₀ α β
⊢ toListModel
      (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.buckets ~
    toListModel m.val.buckets

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

Tactic:
exact Perm.refl _

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
m : Raw₀ α β
⊢ toListModel m.expandIfNecessary.val.buckets ~ toListModel m.val.buckets

Tactic:
rw [expandIfNecessary]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
m : Raw₀ α β
⊢ toListModel
      (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.buckets ~
    toListModel m.val.buckets