-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_insertₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} :
    Perm (toListModel (m.insertₘ a b).1.2) (insertEntry a b (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = false
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
rw [insertEntry_of_containsKey_eq_false h']

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = false
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ ⟨a, b⟩ :: toListModel m.val.buckets

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = false
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ ⟨a, b⟩ :: toListModel m.val.buckets

Tactic:
refine (Raw₀.toListModel_expandIfNecessary _).trans ?_

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = false
⊢ toListModel (m.consₘ a b).val.buckets ~ ⟨a, b⟩ :: toListModel m.val.buckets

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : ¬m.containsₘ a = true
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
rw [containsₘ_eq_containsKey h, Bool.not_eq_true] at h'

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = false
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = false
⊢ toListModel (m.consₘ a b).val.buckets ~ ⟨a, b⟩ :: toListModel m.val.buckets

Tactic:
exact toListModel_consₘ m h a b

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
rw [insertₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (if m.containsₘ a = true then m.replaceₘ a b else (m.consₘ a b).expandIfNecessary).val.buckets ~
    insertEntry a b (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (if m.containsₘ a = true then m.replaceₘ a b else (m.consₘ a b).expandIfNecessary).val.buckets ~
    insertEntry a b (toListModel m.val.buckets)

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : m.containsₘ a = true
⊢ toListModel (m.replaceₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬m.containsₘ a = true
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = true
⊢ toListModel (m.replaceₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
rw [insertEntry_of_containsKey h']

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = true
⊢ toListModel (m.replaceₘ a b).val.buckets ~ replaceEntry a b (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = true
⊢ toListModel (m.replaceₘ a b).val.buckets ~ replaceEntry a b (toListModel m.val.buckets)

Tactic:
exact toListModel_replaceₘ _ h _ _

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : m.containsₘ a = true
⊢ toListModel (m.replaceₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

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

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = true
⊢ toListModel (m.replaceₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : m.containsₘ a = true
⊢ toListModel (m.replaceₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
next h' =>
rw [containsₘ_eq_containsKey h] at h'
rw [insertEntry_of_containsKey h']
exact toListModel_replaceₘ _ h _ _

Result:
no goals

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬m.containsₘ a = true
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
next h' =>
rw [containsₘ_eq_containsKey h, Bool.not_eq_true] at h'
rw [insertEntry_of_containsKey_eq_false h']
refine (Raw₀.toListModel_expandIfNecessary _).trans ?_
exact toListModel_consₘ m h a b

Result:
no goals