-- 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 α
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₀.containsThenInsert ⟨m✝, h✝⟩ a✝¹ b✝).snd.val

Tactic:
exact Raw₀.wfImp_containsThenInsert (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✝ : β✝ → β✝
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp ⟨m✝, h✝⟩.val

Tactic:
apply h

Result:
no goals

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✝¹ : α
f✝ : Option (β✝ a✝¹) → Option (β✝ a✝¹)
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp ⟨m✝, h✝⟩.val

Tactic:
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 ⟨m✝, h✝⟩.val

Tactic:
apply h

Result:
no goals

Proof state:
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

Tactic:
next h => exact Raw₀.wfImp_alter (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 ⟨m✝, h✝⟩.val

Tactic:
apply h

Result:
no goals

Proof state:
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

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

Result:
no goals

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✝¹ : α
f✝ : Option (β✝ a✝¹) → Option (β✝ a✝¹)
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.alter ⟨m✝, h✝⟩ a✝¹ f✝).val

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

Result:
no goals

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✝¹ : α
f✝ : β✝ a✝¹ → β✝ a✝¹
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.modify ⟨m✝, h✝⟩ a✝¹ f✝).val

Tactic:
exact Raw₀.wfImp_modify (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 ⟨m✝, h✝⟩.val

Tactic:
apply h

Result:
no goals

Proof state:
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

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

Result:
no goals