-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.isNum?_eq_some (ctx : Context) {p : Poly} {k : Nat} : p.isNum? = some k → p.denote ctx = k

Proof state:
case h_1
ctx : Context
k : Nat
p✝ : Poly
⊢ some 0 = some k → denote ctx [] = k

case h_2
ctx : Context
k : Nat
p✝ : Poly
k✝ : Nat
v✝ : Var
⊢ (bif v✝ == fixedVar then some k✝ else none) = some k → denote ctx [(k✝, v✝)] = k

case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k

Tactic:
next => intro h; injection h

Result:
case h_2
ctx : Context
k : Nat
p✝ : Poly
k✝ : Nat
v✝ : Var
⊢ (bif v✝ == fixedVar then some k✝ else none) = some k → denote ctx [(k✝, v✝)] = k

case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k

Proof state:
ctx : Context
p : Poly
k : Nat
⊢ (match p with
      | [] => some 0
      | [(k, v)] => bif v == fixedVar then some k else none
      | x => none) =
      some k →
    denote ctx p = k

Tactic:
split

Result:
case h_1
ctx : Context
k : Nat
p✝ : Poly
⊢ some 0 = some k → denote ctx [] = k

case h_2
ctx : Context
k : Nat
p✝ : Poly
k✝ : Nat
v✝ : Var
⊢ (bif v✝ == fixedVar then some k✝ else none) = some k → denote ctx [(k✝, v✝)] = k

case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k

Proof state:
case pos
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
a✝ : k = k✝
⊢ k = k✝

Tactic:
assumption

Result:
no goals

Proof state:
ctx : Context
k : Nat
p✝ : Poly
h : some 0 = some k
⊢ denote ctx [] = k

Tactic:
injection h

Result:
no goals

Proof state:
case h_2
ctx : Context
k : Nat
p✝ : Poly
k✝ : Nat
v✝ : Var
⊢ (bif v✝ == fixedVar then some k✝ else none) = some k → denote ctx [(k✝, v✝)] = k

case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k

Tactic:
next k v => by_cases h : v == fixedVar <;> simp [h]; intros; simp [Var.denote, eq_of_beq h]; assumption

Result:
case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k

Proof state:
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k

Tactic:
intros

Result:
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
a✝ : none = some k
⊢ denote ctx p = k

Proof state:
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
a✝ : none = some k
⊢ denote ctx p = k

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
⊢ k = k✝ → k * Var.denote ctx v = k✝

Tactic:
intros

Result:
case pos
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
a✝ : k = k✝
⊢ k * Var.denote ctx v = k✝

Proof state:
ctx : Context
k : Nat
p✝ : Poly
⊢ some 0 = some k → denote ctx [] = k

Tactic:
intro h

Result:
ctx : Context
k : Nat
p✝ : Poly
h : some 0 = some k
⊢ denote ctx [] = k

Proof state:
case pos
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
a✝ : k = k✝
⊢ k * Var.denote ctx v = k✝

Tactic:
simp [Var.denote, eq_of_beq h]

Result:
case pos
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
a✝ : k = k✝
⊢ k = k✝

Proof state:
ctx : Context
p : Poly
k : Nat
⊢ p.isNum? = some k → denote ctx p = k

Tactic:
simp [isNum?]

Result:
ctx : Context
p : Poly
k : Nat
⊢ (match p with
      | [] => some 0
      | [(k, v)] => bif v == fixedVar then some k else none
      | x => none) =
      some k →
    denote ctx p = k

Proof state:
case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k

Tactic:
next => intros; contradiction

Result:
no goals

Proof state:
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
⊢ (bif v == fixedVar then some k else none) = some k✝ → denote ctx [(k, v)] = k✝

Tactic:
by_cases h : v == fixedVar <;> simp [h]

Result:
case pos
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
⊢ k = k✝ → k * Var.denote ctx v = k✝