-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_le_size [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).1.size ≤ m.1.size + 1

Proof state:
case isTrue
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝ : (m.contains k && (f (m.get? k)).isNone) = true
⊢ m.val.size - 1 ≤ m.val.size + 1

case isFalse.isTrue
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝¹ : ¬(m.contains k && (f (m.get? k)).isNone) = true
h✝ : m.contains k = false ∧ (f (m.get? k)).isSome = true
⊢ m.val.size + 1 ≤ m.val.size + 1

case isFalse.isFalse
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝¹ : ¬(m.contains k && (f (m.get? k)).isNone) = true
h✝ : ¬(m.contains k = false ∧ (f (m.get? k)).isSome = true)
⊢ m.val.size ≤ m.val.size + 1

Tactic:
all_goals omega

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).val.size ≤ m.val.size + 1

Tactic:
simp [size_alter, h]

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
⊢ (if (m.contains k && (f (m.get? k)).isNone) = true then m.val.size - 1
    else if m.contains k = false ∧ (f (m.get? k)).isSome = true then m.val.size + 1 else m.val.size) ≤
    m.val.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
⊢ (if (m.contains k && (f (m.get? k)).isNone) = true then m.val.size - 1
    else if m.contains k = false ∧ (f (m.get? k)).isSome = true then m.val.size + 1 else m.val.size) ≤
    m.val.size + 1

Tactic:
split <;> try split

Result:
case isTrue
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝ : (m.contains k && (f (m.get? k)).isNone) = true
⊢ m.val.size - 1 ≤ m.val.size + 1

case isFalse.isTrue
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝¹ : ¬(m.contains k && (f (m.get? k)).isNone) = true
h✝ : m.contains k = false ∧ (f (m.get? k)).isSome = true
⊢ m.val.size + 1 ≤ m.val.size + 1

case isFalse.isFalse
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝¹ : ¬(m.contains k && (f (m.get? k)).isNone) = true
h✝ : ¬(m.contains k = false ∧ (f (m.get? k)).isSome = true)
⊢ m.val.size ≤ m.val.size + 1

Proof state:
case isFalse.isFalse
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝¹ : ¬(m.contains k && (f (m.get? k)).isNone) = true
h✝ : ¬(m.contains k = false ∧ (f (m.get? k)).isSome = true)
⊢ m.val.size ≤ m.val.size + 1

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝ : ¬(m.contains k && (f (m.get? k)).isNone) = true
⊢ (if m.contains k = false ∧ (f (m.get? k)).isSome = true then m.val.size + 1 else m.val.size) ≤ m.val.size + 1

Tactic:
split

Result:
case isFalse.isTrue
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝¹ : ¬(m.contains k && (f (m.get? k)).isNone) = true
h✝ : m.contains k = false ∧ (f (m.get? k)).isSome = true
⊢ m.val.size + 1 ≤ m.val.size + 1

case isFalse.isFalse
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h✝¹ : ¬(m.contains k && (f (m.get? k)).isNone) = true
h✝ : ¬(m.contains k = false ∧ (f (m.get? k)).isSome = true)
⊢ m.val.size ≤ m.val.size + 1