no goals
ctx : Context
m₁✝ m₂✝ : Mon
fuel : Nat
m₁ m₂ : Mon
⊢ denote ctx (mul.go fuel m₁ m₂) = denote ctx m₁ * denote ctx m₂
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]
no goals
case zero
ctx : Context
m₁✝ m₂✝ m₁ m₂ : Mon
⊢ denote ctx (mul.go zero m₁ m₂) = denote ctx m₁ * denote ctx m₂
simp! [append_denote]
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₂
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 (succ n✝) m₁ m₂) = denote ctx m₁ * denote ctx m₂
simp!
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₂✝)
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₂
split <;> simp!
no goals
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₂✝)
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]
case inr
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₂))
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₂)
by_cases hlt : Nat.blt v₁ v₂ <;> simp! [hlt, Nat.mul_assoc, ih]
no goals
case inr
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₂))
by_cases hgt : Nat.blt v₂ v₁ <;> simp! [hgt, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, ih]