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

Tactic:
exact Raw₀.wfImp_empty

Result:
no goals

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

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

Result:
no goals

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

Tactic:
next h => exact Raw₀.wfImp_filter (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 α β✝
a✝ : 0 < m✝.buckets.size
h : ∀ [inst : EquivBEq α] [inst : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp m✝

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 α fun x => β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝
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 (Raw₀.containsThenInsertIfNew ⟨m✝, h✝⟩ a✝¹ b✝).snd.val

Tactic:
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 α
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 (Raw₀.Const.modify ⟨m✝, h✝⟩ a✝¹ f✝).val

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

Tactic:
apply h

Result:
no goals

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

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

Result:
no goals

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

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

Tactic:
apply h

Result:
no goals

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

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

Result:
no goals

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

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

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

Result:
no goals

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

Tactic:
next h => 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 α β✝
h✝ : 0 < m✝.buckets.size
a✝¹ : α
b✝ : β✝ a✝¹
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.insertIfNew ⟨m✝, h✝⟩ a✝¹ b✝).val

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

Result:
no goals

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

Tactic:
next h => exact Raw₀.Const.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✝¹ : α
b✝ : β✝
a✝ : m✝.WF
h : ∀ [i₁ : EquivBEq α] [i₂ : LawfulHashable α], WFImp m✝
i₁ : EquivBEq α
i₂ : LawfulHashable α
⊢ WFImp (Raw₀.Const.getThenInsertIfNew? ⟨m✝, h✝⟩ a✝¹ b✝).snd.val

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

Tactic:
apply h

Result:
no goals