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

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 - 1 ≤ m.val.size

Tactic:
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.val.size - 1 ≤
    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

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 - 1 ≤ m.val.size

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.val.size - 1 ≤ (m.alter k f).val.size

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)
⊢ m.val.size - 1 ≤
    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

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
⊢ m.val.size - 1 ≤ if m.contains k = false ∧ (f (m.get? k)).isSome = true then m.val.size + 1 else m.val.size

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 - 1 ≤ m.val.size

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 - 1 ≤ m.val.size

Tactic:
all_goals omega

Result:
no goals