-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Mon.mul_denote (ctx : Context) (m₁ m₂ : Mon) : (m₁.mul m₂).denote ctx = m₁.denote ctx * m₂.denote ctx :=
  go hugeFuel m₁ m₂
where
  go (fuel : Nat) (m₁ m₂ : Mon) : (Mon.mul.go fuel m₁ m₂).denote ctx = m₁.denote ctx * m₂.denote ctx

Proof state:
ctx : Context
m₁✝¹ m₂✝¹ : Mon
n✝ : Nat
ih : ∀ (m₁ m₂ : Mon), denote ctx (mul.go n✝ m₁ m₂) = denote ctx m₁ * denote ctx m₂
m₁✝ m₂✝ : Mon
v₁ : Var
m₁ : List Var
v₂ : Var
m₂ : List Var
⊢ denote ctx
      (bif blt v₁ v₂ then v₁ :: mul.go n✝ m₁ (v₂ :: m₂)
      else bif blt v₂ v₁ then v₂ :: mul.go n✝ (v₁ :: m₁) m₂ else v₁ :: v₂ :: mul.go n✝ m₁ m₂) =
    Var.denote ctx v₁ * denote ctx m₁ * (Var.denote ctx v₂ * denote ctx m₂)

Tactic:
by_cases hlt : Nat.blt v₁ v₂ <;> simp! [hlt, Nat.mul_assoc, ih]

Result:
case neg
ctx : Context
m₁✝¹ m₂✝¹ : Mon
n✝ : Nat
ih : ∀ (m₁ m₂ : Mon), denote ctx (mul.go n✝ m₁ m₂) = denote ctx m₁ * denote ctx m₂
m₁✝ m₂✝ : Mon
v₁ : Var
m₁ : List Var
v₂ : Var
m₂ : List Var
hlt : ¬blt v₁ v₂ = true
⊢ denote ctx (bif blt v₂ v₁ then v₂ :: mul.go n✝ (v₁ :: m₁) m₂ else v₁ :: v₂ :: mul.go n✝ m₁ m₂) =
    Var.denote ctx v₁ * (denote ctx m₁ * (Var.denote ctx v₂ * denote ctx m₂))

Proof state:
ctx : Context
m₁✝ m₂✝ : Mon
fuel : Nat
m₁ m₂ : Mon
⊢ denote ctx (mul.go fuel m₁ m₂) = denote ctx m₁ * denote ctx m₂

Tactic:
induction fuel generalizing m₁ m₂ with
| zero => simp! [append_denote]
| succ _ ih =>
  simp!
  split <;> simp!
  next v₁ m₁ v₂ m₂ =>
    by_cases hlt : Nat.blt v₁ v₂ <;> simp! [hlt, Nat.mul_assoc, ih]
    by_cases hgt : Nat.blt v₂ v₁ <;> simp! [hgt, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, ih]

Result:
no goals

Proof state:
case succ
ctx : Context
m₁✝ m₂✝ : Mon
n✝ : Nat
ih : ∀ (m₁ m₂ : Mon), denote ctx (mul.go n✝ m₁ m₂) = denote ctx m₁ * denote ctx m₂
m₁ m₂ : Mon
⊢ denote ctx (mul.go (n✝ + 1) m₁ m₂) = denote ctx m₁ * denote ctx m₂

Tactic:
simp!

Result:
case succ
ctx : Context
m₁✝ m₂✝ : Mon
n✝ : Nat
ih : ∀ (m₁ m₂ : Mon), denote ctx (mul.go n✝ m₁ m₂) = denote ctx m₁ * denote ctx m₂
m₁ m₂ : Mon
⊢ denote ctx
      (match m₁, m₂ with
      | m₁, [] => m₁
      | [], m₁ => m₁
      | v₁ :: m₁, v₂ :: m₂ =>
        bif blt v₁ v₂ then v₁ :: mul.go n✝ m₁ (v₂ :: m₂)
        else bif blt v₂ v₁ then v₂ :: mul.go n✝ (v₁ :: m₁) m₂ else v₁ :: v₂ :: mul.go n✝ m₁ m₂) =
    denote ctx m₁ * denote ctx m₂

Proof state:
case neg
ctx : Context
m₁✝¹ m₂✝¹ : Mon
n✝ : Nat
ih : ∀ (m₁ m₂ : Mon), denote ctx (mul.go n✝ m₁ m₂) = denote ctx m₁ * denote ctx m₂
m₁✝ m₂✝ : Mon
v₁ : Var
m₁ : List Var
v₂ : Var
m₂ : List Var
hlt : ¬blt v₁ v₂ = true
⊢ denote ctx (bif blt v₂ v₁ then v₂ :: mul.go n✝ (v₁ :: m₁) m₂ else v₁ :: v₂ :: mul.go n✝ m₁ m₂) =
    Var.denote ctx v₁ * (denote ctx m₁ * (Var.denote ctx v₂ * denote ctx m₂))

Tactic:
by_cases hgt : Nat.blt v₂ v₁ <;> simp! [hgt, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, ih]

Result:
no goals

Proof state:
case succ
ctx : Context
m₁✝ m₂✝ : Mon
n✝ : Nat
ih : ∀ (m₁ m₂ : Mon), denote ctx (mul.go n✝ m₁ m₂) = denote ctx m₁ * denote ctx m₂
m₁ m₂ : Mon
⊢ denote ctx
      (match m₁, m₂ with
      | m₁, [] => m₁
      | [], m₁ => m₁
      | v₁ :: m₁, v₂ :: m₂ =>
        bif blt v₁ v₂ then v₁ :: mul.go n✝ m₁ (v₂ :: m₂)
        else bif blt v₂ v₁ then v₂ :: mul.go n✝ (v₁ :: m₁) m₂ else v₁ :: v₂ :: mul.go n✝ m₁ m₂) =
    denote ctx m₁ * denote ctx m₂

Tactic:
split <;> simp!

Result:
case succ.h_3
ctx : Context
m₁ m₂ : Mon
n✝ : Nat
ih : ∀ (m₁ m₂ : Mon), denote ctx (mul.go n✝ m₁ m₂) = denote ctx m₁ * denote ctx m₂
m₁✝¹ m₂✝¹ : Mon
v₁✝ : Var
m₁✝ : List Var
v₂✝ : Var
m₂✝ : List Var
⊢ denote ctx
      (bif blt v₁✝ v₂✝ then v₁✝ :: mul.go n✝ m₁✝ (v₂✝ :: m₂✝)
      else bif blt v₂✝ v₁✝ then v₂✝ :: mul.go n✝ (v₁✝ :: m₁✝) m₂✝ else v₁✝ :: v₂✝ :: mul.go n✝ m₁✝ m₂✝) =
    Var.denote ctx v₁✝ * denote ctx m₁✝ * (Var.denote ctx v₂✝ * denote ctx m₂✝)

Proof state:
case zero
ctx : Context
m₁✝ m₂✝ m₁ m₂ : Mon
⊢ denote ctx (mul.go 0 m₁ m₂) = denote ctx m₁ * denote ctx m₂

Tactic:
simp! [append_denote]

Result:
no goals

Proof state:
case succ.h_3
ctx : Context
m₁ m₂ : Mon
n✝ : Nat
ih : ∀ (m₁ m₂ : Mon), denote ctx (mul.go n✝ m₁ m₂) = denote ctx m₁ * denote ctx m₂
m₁✝¹ m₂✝¹ : Mon
v₁✝ : Var
m₁✝ : List Var
v₂✝ : Var
m₂✝ : List Var
⊢ denote ctx
      (bif blt v₁✝ v₂✝ then v₁✝ :: mul.go n✝ m₁✝ (v₂✝ :: m₂✝)
      else bif blt v₂✝ v₁✝ then v₂✝ :: mul.go n✝ (v₁✝ :: m₁✝) m₂✝ else v₁✝ :: v₂✝ :: mul.go n✝ m₁✝ m₂✝) =
    Var.denote ctx v₁✝ * denote ctx m₁✝ * (Var.denote ctx v₂✝ * denote ctx m₂✝)

Tactic:
next v₁ m₁ v₂ m₂ =>
  by_cases hlt : Nat.blt v₁ v₂ <;> simp! [hlt, Nat.mul_assoc, ih]
  by_cases hgt : Nat.blt v₂ v₁ <;> simp! [hgt, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, ih]

Result:
no goals