-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem WF.out [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashable α] {m : Raw α β}
    (h : m.WF) : Raw.WFImp m

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i₁ : EquivBEq α
i₂ : LawfulHashable α
m : Raw α β
h : m.WF
⊢ WFImp m

Tactic:
induction h generalizing i₁ i₂

Result:
case wf
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
a✝¹ : 0 < m✝.buckets.size
a✝ : ∀ [inst : EquivBEq α] [inst : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp m✝

case empty₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
c✝ : Nat
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.empty c✝).val

case insert₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.insert ⟨m✝, h✝⟩ a✝¹ b✝).val

case containsThenInsert₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.containsThenInsert ⟨m✝, h✝⟩ a✝¹ b✝).snd.val

case containsThenInsertIfNew₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.containsThenInsertIfNew ⟨m✝, h✝⟩ a✝¹ b✝).snd.val

case erase₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.erase ⟨m✝, h✝⟩ a✝¹).val

case insertIfNew₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.insertIfNew ⟨m✝, h✝⟩ a✝¹ b✝).val

case getThenInsertIfNew?₀
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.getThenInsertIfNew? ⟨m✝, h✝⟩ a✝¹ b✝).snd.val

case filter₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
f✝ : (a : α) → β✝ a → Bool
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.filter f✝ ⟨m✝, h✝⟩).val

case constGetThenInsertIfNew?₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α fun x => β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.Const.getThenInsertIfNew? ⟨m✝, h✝⟩ a✝¹ b✝).snd.val

case modify₀
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
f✝ : β✝ a✝¹ → β✝ a✝¹
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.modify ⟨m✝, h✝⟩ a✝¹ f✝).val

case constModify₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α fun x => β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
f✝ : β✝ → β✝
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.Const.modify ⟨m✝, h✝⟩ a✝¹ f✝).val

case alter₀
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
f✝ : Option (β✝ a✝¹) → Option (β✝ a✝¹)
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.alter ⟨m✝, h✝⟩ a✝¹ f✝).val

case constAlter₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α fun x => β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
f✝ : Option β✝ → Option β✝
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.Const.alter ⟨m✝, h✝⟩ a✝¹ f✝).val

Proof state:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.getThenInsertIfNew? ⟨m✝, h✝⟩ a✝¹ b✝).snd.val

Tactic:
exact Raw₀.wfImp_getThenInsertIfNew? (by apply h)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α fun x => β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
f✝ : Option β✝ → Option β✝
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.Const.alter ⟨m✝, h✝⟩ a✝¹ f✝).val

Tactic:
exact Raw₀.Const.wfImp_alter (by apply h)

Result:
no goals

Proof state:
case insert₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.insert ⟨m✝, h✝⟩ a✝¹ b✝).val

Tactic:
next h => exact Raw₀.wfImp_insert (by apply h)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.insert ⟨m✝, h✝⟩ a✝¹ b✝).val

Tactic:
exact Raw₀.wfImp_insert (by apply h)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.erase ⟨m✝, h✝⟩ a✝¹).val

Tactic:
exact Raw₀.wfImp_erase (by apply h)

Result:
no goals

Proof state:
case constAlter₀
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
β✝ : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m✝ : Raw α fun x => β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
f✝ : Option β✝ → Option β✝
a✝ : m✝.WF
a_ih✝ : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.Const.alter ⟨m✝, h✝⟩ a✝¹ f✝).val

Tactic:
next h => exact Raw₀.Const.wfImp_alter (by apply h)

Result:
no goals