-- 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 β → Option β} :
    (Const.alter m k f).1.size ≤ m.1.size + 1

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

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

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

Tactic:
all_goals omega

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option β → Option β
⊢ (if (m.contains k && (f (get? m k)).isNone) = true then m.val.size - 1
    else if m.contains k = false ∧ (f (get? m 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
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option β → Option β
h✝ : (m.contains k && (f (get? m k)).isNone) = true
⊢ m.val.size - 1 ≤ m.val.size + 1

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

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp [size_alter, h]

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

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

Tactic:
split

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

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