-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean
theorem hashesTo_cons [BEq α] [Hashable α] {i : Nat} {size : Nat} {l : List ((a : α) × β a)} {k : α}
    {v : β k} (h : (h' : 0 < size) → (mkIdx size h' (hash k)).1.toNat = i) :
    HashesTo l i size → HashesTo (⟨k, v⟩ :: l) i size

Proof state:
case inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
x✝ : HashesTo l i size
ih : ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ l → (mkIdx size h (hash p.fst)).val.toNat = i
h' : 0 < size
⊢ (mkIdx size h' (hash ⟨k, v⟩.fst)).val.toNat = i

Tactic:
exact h h'

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
x✝ : HashesTo l i size
ih : ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ l → (mkIdx size h (hash p.fst)).val.toNat = i
h' : 0 < size
k' : (a : α) × β a
hk : k' = ⟨k, v⟩ ∨ k' ∈ l
⊢ (mkIdx size h' (hash k'.fst)).val.toNat = i

Tactic:
rcases hk with (rfl|hk)

Result:
case inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
x✝ : HashesTo l i size
ih : ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ l → (mkIdx size h (hash p.fst)).val.toNat = i
h' : 0 < size
⊢ (mkIdx size h' (hash ⟨k, v⟩.fst)).val.toNat = i

case inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
x✝ : HashesTo l i size
ih : ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ l → (mkIdx size h (hash p.fst)).val.toNat = i
h' : 0 < size
k' : (a : α) × β a
hk : k' ∈ l
⊢ (mkIdx size h' (hash k'.fst)).val.toNat = i

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
⊢ HashesTo l i size → HashesTo (⟨k, v⟩ :: l) i size

Tactic:
refine fun ⟨ih⟩ => ⟨fun h' k' hk => ?_⟩

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
x✝ : HashesTo l i size
ih : ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ l → (mkIdx size h (hash p.fst)).val.toNat = i
h' : 0 < size
k' : (a : α) × β a
hk : k' ∈ ⟨k, v⟩ :: l
⊢ (mkIdx size h' (hash k'.fst)).val.toNat = i

Proof state:
case inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
x✝ : HashesTo l i size
ih : ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ l → (mkIdx size h (hash p.fst)).val.toNat = i
h' : 0 < size
k' : (a : α) × β a
hk : k' ∈ l
⊢ (mkIdx size h' (hash k'.fst)).val.toNat = i

Tactic:
exact ih h' _ hk

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
x✝ : HashesTo l i size
ih : ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ l → (mkIdx size h (hash p.fst)).val.toNat = i
h' : 0 < size
k' : (a : α) × β a
hk : k' ∈ ⟨k, v⟩ :: l
⊢ (mkIdx size h' (hash k'.fst)).val.toNat = i

Tactic:
simp only [List.mem_cons] at hk

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
l : List ((a : α) × β a)
k : α
v : β k
h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i
x✝ : HashesTo l i size
ih : ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ l → (mkIdx size h (hash p.fst)).val.toNat = i
h' : 0 < size
k' : (a : α) × β a
hk : k' = ⟨k, v⟩ ∨ k' ∈ l
⊢ (mkIdx size h' (hash k'.fst)).val.toNat = i